Leon Gumański

T:

where (ik) is the set of all atomic expressions occurring in that subtableau of T which belongs to stage i of the construction.

CONVENTION 2.3. We shall sometimes say that occurs (is) at stage i.

Of special interest are those tableaux that can be characterized by the following sequence:

DEFINITION 2.7. Tableaux of this kind will be called “homogeneous”. They consist of subtableaux such that is the j–th subtableau of stage 1 and for all i (2ik): (of stage i) is on the j–th branch of Tableaux that are not homogeneous are heterogeneous.

For illustrative purposes let us return to Tab. 1 for a while. As we have already alluded the whole construction there comprises four 2–stage tableaux. Two of them are homogeneous, namely the first one consisting of the subtableau No 1 and No 11, then the last one embracing the subtableau No 2 and No 22.

REMARK 2.7. If in a k–stage tableau–construction there is only one tableau (n=1), it must be homogeneous for it is characterized by the sequence (j=1, e_i=i):

Tab. 3 may serve again as an example here.
3. Provability

Some conditions and negative criterions
Now, let us consider another 2–stage tableau construction:

Tab. 4

True				False
				(Ex1) (x2) [fx1–(gx2hx1)] (x2) [fy1–(gx2hy1)] fy1–(gy2hy1)
1 the end of stage 1		2 gy2hy1 gy2 hy1		1 fy1		2 –(gy2hy1)
				(x2) [fy2–(gx2hy2)] fy2–(gy3hy2)		(x2) [fy1–(gx2hy1)] fy1–(gy3hy1)
11	12 gy3hy2 gy3 hy2	21	22 gy3hy1 gy3 hy1	11 fy2	12 –(gy3hy2)	21 fy1	22 –(gy3hy1)
the end of stage 2

Again there are four tableaux in this construction. In order to compare the sets of atomic expressions in them it may be expedient to employ the following arrangement (as in the foregoing the sign plus means that the expression is in the left column):

Tableau	Stage 1	Stage 2	Type
No 1 + No 11			homogeneous
No 1 + No 12			heterogeneous
No 2 + No 21			heterogeneous
No 2 + No 22			homogeneous

It appears that in every column of a homogeneous tableau the succeeding atomic expressions begin with the same predicate variables at both stages. It is left to the reader to check up that the same regularity will hold good at the next stages. A similar regularity can be also found in the sole tableau of Tab. 3. This is a result of assumptions 2.1, 2.2, 2.3 and 2.4.

OBSERVATION 3.1. In atomic expressions of a homogeneous tableau a predicate variable F occurs in a column of stage i (i>1) if and only if the variable F is present in the same column of stage 1.

COROLLARY 3.1. For every k: if at stage 1 of a k–stage homogeneous tableau T there is no predicate variable which can be found in both columns at the beginning of atomic expressions, then the tableau is not closed.

PROOF. The corollary is a consequence of Observation 3.1 and the clo­sure rule.

Hence we have already a negative criterion of existence of a proof of the expression t:

NC1 If in a k–stage tableau–construction of t there is a homogeneous tableau T which fulfils the condition formulated in the antecedent of the foregoing Corollary 3.1, then the construction is not closed and no proof of t is possible.

What this amounts to is the statement that in certain cases the problem of decision can be solved negatively by means of one–stage tableau–construction. We shall later see that there are more cases in which a one–stage tableau–con­stru­ction turns out to be sufficient.

From our negative criterion NC1 we conclude by conversion that:

COROLLARY 3.2. If t is provable, every homogeneous tableau T of a tableau–construction of t is such that a predicate variable F commences an atomic expre­ssion in both columns of stage 1 of T.

However the fact remains that:

OBSERVATION 3.2. For each subtableau (jn) of stage 1 of the con­stru­ction there is a homogeneous tableau T_j of which is the first subtableau.

COROLLARY 3.3. For each subtableau of stage 1 there must be such a predicate variable F_j that is present in atomic expressions in both columns of .

Corollary 3.3 indicates a necessary condition of provability of t but not a sufficient one because the presence of F_j in both columns of does not testify that by suitable substitutions of y–variables for x–variables (by virtue of the rules for quantifiers) the closure of all tableaux of the construction can be achieved after k stages (for some k).

Now, let us introduce some new symbols and terms relative to the sets of atomic expressions in a k–stage tableau construction of t.