## Leon Gumański
- Bu səhifədəki naviqasiya:
- 1. Introduction and preliminaries
- 2. Semantic tableaux
K1, K2 are sets of expressions (may be empty) here and the y–variable b in F(a) should always be “new” (i. e. such that it does not yet occur in the tableau) whereas the y–variable b in F(Ea) can be “new” if and only if no y–variables are present in the tableau yet, so if there are some y–variables, b should be (freely) chosen from among them^{3}.
Besides the As a point of departure for further analyses let us take by way of a paradigm example the proof of the expression W mentioned above. Tab. 1
Analysing Tab. 1 it is easy to notice that the method of semantic tableaux makes it possible to dissolve compound expressions into ever smaller ones and to obtain finally some atomic expressions. The example shows that it is sometimes necessary to apply a rule (reduction schema) to the same quantifier more than once. DEFINITION 2.2. If all the quantifiers of DEFINITION 2.3. In case a tableau–construction C of DEFINITION 2.4. When all the tableaux of a construction are closed, we say that the whole construction is i–stage proof of t, then P is an economic (k–stage) proof of t. In that case we shall say that the number k is the minimum length coefficient of the proof of t.
EXAMPLE 2.1. For instance, Tab. 1 is a specimen of 2–stage tableau–construction, which comprises four 2–stage tableaux because the initial common part splits into two subtableaux at stage 1 and then each subtableau of stage 1 splits again into two other ones. As all the four tableaux are closed, the whole 2–stage tableau–construction is a proof. OBSERVATION 2.1. Splitting of a tableau is a result of an application of rule LEMMA 2.1. If a PROOF. According to definition 2.2 all appropriate rules for truth–functors have to be applied at each stage. Then if rule LEMMA 2.2. The number of tableaux in a construction depends on the fact how many times the rule PROOF. There are ASSUMPTION 2.1 We assume that the order of transformations by DEFINITION 2.5. When a subtableau
we shall say that At the same time we take for granted that: ASSUMPTION 2.2. For every EXAMPLE 2.2. In Tab. 1 the subtableau No 1 of stage 1 is anterior to the subtableaux No 11 and No 12 of stage 2 and the subtableau No 11 is on the first branch of the subtableau No 1 whereas the subtableau No 12 is on the second branch of the subtableau No 1. The transformations of stage 2 are in accordance with Assumption 2.1 and 2.2. REMARK 2.1. Observe in Tab. 1 that the subtableau No 2 is already closed at stage 1. However, it should be born in mind that further transformations – although useless – are admissible even on closed tableaux. Just to stress this possibility suitable rules have been applied at stage 2 in the subtableau No 21 and No 22 as well. This explains why our definition of “ REMARK 2.2. It is clear that it would be futile to use after a certain stage of a tableau–construction only rules for truth–functors because it would not result in creating new expressions different from those that exist already in the tableau–construction. Hence appropriate rules for quantifiers should be utilized at every stage. However, as a matter of fact in some cases it may turn out that in order to achieve a proof of Anyhow, it might be well to mention that in some economic proofs it is necessary to reduce universal quantifiers that appear at the beginning of Tab. 2
Tab. 3
REMARK 2.3. It is worth noting that a tableau can sometimes be closed on account of a compound fully open expression
If Yüklə 0,58 Mb. Dostları ilə paylaş: |