Leon Gumański

DEFINITION 3.1. (i ≤ k)

That is to say, the symbol ‘’ stands for the set of (all and only) those atomic expressions which are in at least one of the successive (starting with stage 1) subtableaux of a certain tableau T. Hence the set is the set of all atomic expressions present in the tableau T. If i=1, then and is the set of atomic expressions of a subtableau of stage 1.

CONVENTION 3.1. For every ik one is allowed to say accordingly that occurs (is) at stage i.

DEFINITION 3.2. When a subtableau is on the g–th branch of the anterior subtableau we shall say that the set is on the g–th branch of and the set is anterior to .

Sometimes it will be convenient to speak about the set of (all and only) atomic expressions which can be found in at least one of the subtableaux (0 d r–n, confront Graph G).

DEFINITION 3.3.

and for some d and every g ≤ n: is on the g–th branch of .

Graphically: (if i=1, instead of there is t).

	• • •
	• • •

ASSUMPTION 3.1. Each of the sets Q₁, Q₂,…,Q_q (q=1+n+…+n^k–1) in any k–stage tableau–construction of t is ordered according to the same principle.

DEFINITION 3.4. When is anterior to we shall say that the set is anterior to as well as is anterior to and to .

Let us return for a while to the tableau–construction represented in Tab. 4. The comparison of the set with the set and discloses an essential regularity:

OBSERVATION 3.3. The sets Q_f, Q_g (f,gq) differ at most in the shape of the y–variables in analogous places and if a y–variable has been introduced by virtue of the rule F(a) (or F(Ea)) in a certain place p in Q_f, then a y–variable has also been introduced by virtue of the same rule in place p in Q_g.

CONVENTION 3.2. One is allowed to say that occurs (is) at stage i.

DEFINITION 3.5. If there exists such an atomic expression v that , we give expression to this fact saying that there is a closing pair in    .

For instance, the pair {+fy₂,fy₂} in the subtableau No 2 in Tab. 1 is a closing pair.

CONVENTION 3.3. In what follows in this section (3) the signs “u”, “w” stand for any not identical atomic expressions.

DEFINITION 3.6. A pair of atomic expressions {+u,w} such that both u and w begin with the same predicate variable F will be termed “distinguished”.

DEFINITION 3.7. In case a distinguished pair {+u,w} occurs in the d–th subtableau of a tableau–construction of t but in the same subtableau such substi­tutions by F(Ea) are admissible that would yield a closing pair {+v,v} in place of {+u,w} (both pairs originate from the same pair of (not separate) atomic expressions being present in the matrix of t), then the pair {+u,w} is called a one–stage pair.

Consider for instance the following tableau:

True	False
gy1(–fy2fy1) gy1 –fy2fy1 –fy2­ fy1 the end of stage 1	(x1) (x2) (Ex3) – [gx1(–fx2fx3)] (x2) (Ex3) – [gy1(–fx2fx3)] (Ex3) – [gy1(–fy2fx3)] – [gy1(–fy2fy1)] fy2	x1/y1 x2/y2 x3/y1

The pair {+fy₁,fy₂} is a one–stage pair because the substitution x₃/y₂ is also permissible at stage 1 and would give us a closing pair {+fy₂,fy₂} instead of the pair {+fy₁,fy₂}.

DEFINITION 3.8. When a distinguished pair is not a one–stage pair but at stage i+1 such substitutions by F(Ea) are performable that would produce u instead of w or +w instead of +u in the subtableau to which is anterior (hence either or would hold good), then the pair {+u,w} is a two–stage pair.

In other words, if there is a two–stage pair , then it is possible to obtain at the next stage a closing pair or . The pair {+fy₂, fy₁} in the subtableau No 1 of Tab. 1 may serve as a concrete example of a two–stage pair (the substitution x₁/y₂ is not permissible before stage 2).

DEFINITION 3.9. Any pair of atomic expressions which is either a one–stage or a two–stage pair will be called “subclosing”.

LEMMA 3.1. If the expression t has a closed k–stage tableau–construction (a proof), then in every not closed subtableau of stage 1 of the construction there exists at least one subclosing pair of atomic expressions.

PROOF. The rightness of this lemma is again visible from the homogeneous tableaux of the construction. Namely, if t has a proof, all tableaux of the construction are closed, among others all the homogeneous tableaux, too. However, when a homogeneous tableau T_j is closed, the closure is achieved due to a closing pair {+v,v}. If the pair is not in (i. e. the subtableau of T_j which belongs to stage 1, jn), then there remain two cases only: either both members of {+v,v} occur at the same stage i or one member of the pair occurs at stage i and the other one at stage i+sk. In the first case, according to Definition 3.7 there is a one stage pair in . In the second case, after Definition 3.8 there is a two–stage pair in . Hence by Definition 3.9 there is a subclosing pair in for every jn.

We are now in position to complement our previous negative criterion NC1 of provability by a second criterion:

NC2 If in some not closed subtableau of stage 1 of a k–stage tableau–constru­ction of t no subclosing pair of atomic expressions exists, then no proof of t is possible.

PROOF. NC2 follows from Lemma 3.1 by conversion.

OBSERVATION 3.4. It is worth noting that when a certain tableau–con­stru­ction of t consists of no more than one tableau (i. e. n=1), then the graph G (p. 9) reduces to

t						...

and the implication in Lemma 3.1 can be strengthen to equivalence. In other words, the condition of provability in Lemma 3.1 becomes not only necessary, but also sufficient.

COROLLARY 3.4. An economic proof of t in which the rule FC is inappli­cable has at most 2 stages.

PROOF. According to Remark 2.7 the sole tableau of the proof is homo­ge­neous and by Lemma 3.1 there must be in a subclosing pair which can be trans­for­med into a closing pair either at stage 1 or at stage 2.

THEOREM 3.1. The set of expressions provable without rule FC is decidable.

PROOF. By Corollary 3.4 use the test described in section 4.

It may be well to add incidentally that it can be recognized immediately at stage 1 whether the rule FC is applicable at all in a proof of t.

When a tableau–construction of t consists of more than one tableau, the necessary condition of provability indicated in Lemma 3.1 turns out not to be sufficient in general. For it often happens that although the condition is fulfilled no proof of t exists, since it is impossible to find such admissible substitutions by F(Ea) which would transform subclosing pairs into closing ones in each tableau of the construction (substitutions suitable for closure of one tableau may be inappropriate for another tableau). None the less if the condition is not fulfilled, the expression t is unprovable.

At any rate the problem remains still open how to recognize whether the expression t can be proved when stage 1 of a tableau–construction of t embraces more than one subtableau (n>1).

4. Provability. Test for any given number k
When trying to solve the problem of provability it is important to realize and to keep in mind first of all that we do have an effective method to determine whether a tableau–construction of t can be closed at stage k (k=1,2,3,…). Namely, in view of the fact that only one rule F(Ea) allows a choice of substituted y–varia­bles (if there are more than one free variable in the expression transformed), we can for a start check up all admissible substitutions a/b when applying rule F(Ea) at stage 1 of the construction. The number of trials (possible substitutions) is always finite because there is a finite number of free individual variables in the expression to be transformed. If by no means the construction can be closed at stage 1, then for each manner of substituting at stage 1 we can try out all the possible substitutions by F(Ea) at stage 2 taking into account that transformations need not start from the first quantifier (cf. Tab. 2). When this does not result in discovery of a proof either, then for each manner of substituting by F(Ea) at stage 1 and 2 we can put to test all the possible substitutions by F(Ea) at stage 3 and this procedure can be conti­nued up to stage k. When in the course of this procedure a proof of t has already been found at stage i, we know how many stages an economic proof of t demands. If i<k, the proof may be extended up to stage k for it is always permissible to continue transformations even on closed tableaux (cf. Remark 2.1). Hence in this case a k–stage proof of t also exists, although it is not an economic proof. However, when all the trials do not result in a discovery of a proof, it is evident that a k–stage proof of t is impossible.

Then an important problem arises whether it would be expedient to continue the procedure and how long. To put it another way, the question is if it is possible to indicate such a number k which is the limit of purposeful quest for a proof of t. So when the limit is attained and no proof is found, further efforts are useless because t is unprovable.

5. Three types of prefix
Now we shall take advantage of a distinction between the shapes the prefix of t may have.

I. The prefix of t comprises only universal quantifiers, i. e. t has the form:

(a₁)(a₂)…(a_m)w
where the matrix w contains no other individual variables than a₁,a₂…,a_m. When building a tableau–construction of t, F(a) is the only applicable rule for quanti­fiers in this case and at stage 1 one obtains n subtableaux in which the atomic expre­ssions belonging to the sets are constructed of m different y–va­ria­bles and some predicate variables.

LEMMA 5.1. If a set does not embrace any closing pair (so the subtableau is not closed), then every k–stage tableau–construction of t is not closed either.

PROOF. This is visible from the k–stage homogeneous tableau T of which is the first subtableau (i. e. the subtableau which belongs to stage 1). Namely, the y–variables in the elements of the set are entirely different from those of ⁴. That is why no atomic expression can make a closing pair with an atomic expression of the set . Besides if in certain places the y–variables are different (identical) in the elements of, then the y–variables in the elements of are also different (identical) in analogous places. Hence, as the first subtableau of T is not closed, the whole tableau T cannot be closed either.

And so we conclude:

THEOREM 5.1. Provability of t can be effectively checked up by means of a one–stage tableau–construction of t. The expression t is universally valid if and only if the one–stage tableau–construction is closed.

PROOF.  from Lemma 5.1 by conversion; ← obvious.

II. The prefix of t is composed of nothing but existential quantifiers, i. e. t is of the form:

(Ea₁)(Ea₂)…(Ea_m)w.
In this case the sole applicable rule for quantifiers is F(Ea). It demands to introduce a y–variable while eliminating the first quantifier. The same y–variable, being the only free individual variable in expressions transformed, has to be substituted for all x–variables at every stage of the tableau–construction of t. For that reason it should be immediately evident that the atomic expressions of stage 1 of any homogeneous tableau T of the construction must be repeated at every stage of T. In other words: . But this testifies that T is closed if and only if for every j,e₁n: the set contains a closing pair of atomic expressions. And so we arrive at the conclusion:

THEOREM 5.2. A one–stage tableau–construction of t suffices, in this case, for verifying whether t is a theorem of the calculus. We are confronted with a positive result of the verification if and only if the construction is closed.

III. In the light of what has been ascertained so far it is enough to confine further discussion only to expressions with a prefix containing both existential and universal quantifiers. Thus let t be an expression of this sort. In other words, t has the form:
( )( )…( )w
where the parantheses “( )” represent a quantifier, no matter which one.

At first we have to analyse the sets of atomic expressions one may find in a k–stage tableau–construction of t.

The sets if are not identical, may differ in various respects some of which are essential for the possibility of proving the expression t. In order to elucidate this point certain new notions seem to be indispensable.

DEFINITION 5.1. By “the degree of the set X of atomic expressions” we shall mean the number of distinct individual variables the expressions of the set X are built of.

For instance, the set {+fy₁y₁,+fy₁y₂,gy₂y₁} is of degree 2. The sets may differ in their degree.

DEFINITION 5.2. Sets X₁, X₂ of atomic expressions are of the same kind if and only if X₁ comes into being from X₂ as an effect of simultaneously substituting certain variables for some (or all) individual variables occurring in the elements of X₂ and at the same time X₂ comes into being from X₁ as a result of reverse substitutions (substitutions b/a are reverse of the substitutions a/b).

EXAMPLES. The following sets X₁, X₂ are of the same kind:

X₁ = {fyy₁}, X₂ = {fyy₁},

X₁ = {fy, hyy₁}, X₂ = {fy₂, hy₂y₁},

X₁ = {gy₁y₂, +gy₂y₁, gy₁y₁}, X₂ = {gy₂y₁, +gy₁y₂, gy₂y₂}.
On the contrary, the set X₁ is not of the same kind as X₂ in the next cases:

X₁ = {fy₁y₂}, X₂ = {hy₁y₂},

X₁ = {fy₁y₂}, X₂ = {+fy₁y₂},

X₁ = {fy₁, hy₁y₂}, X₂ = {fy₁, hy₁y₂, gy₃},

X₁ = {hy₁y₂, +hy₁y₂}, X₂ = {hy₁y₁, +hy₁y₁}.

REMARK 5.1. It is visible that identical sets are of the same kind. We take that empty sets are of the same kind although we shall not take advantage of them. Sets of the same kind may differ only in the shape of individual variables in their elements. Not equivalent sets (not having the same number of elements) as well as sets not having the same degree are always of a different kind. When comparing sets it should be remembered that atomic expressions u, +u have to be treated as distinct.

The sets may be different in their kind.

DEFINITION 5.3. The kind of a set X of atomic expressions is an equi­valence class (abstraction class) generated by X with respect to the relation of being of the same kind.

DEFINITION 5.4. Sets X₁, X₂ of atomic expressions are up to degree h of the same kind if and only if 1⁰ both sets X₁, X₂ are at least of degree h and 2⁰ for every subset Y₁  X₁ of a degree not higher than h there is a subset Y₂  X₂ of the same kind as Y₁ and conversely: for every subset Y₂  X₂ of degree not higher than h there is a subset Y₁  X₁ of the same kind as Y₂.

For instance, the sets X₁={fy₁y₂,+hy₁}, X₂={+fy₁y₂,fy₂y₁,+hy₃} are only to degree 1 of the same kind though the set X₁ is of degree 2 whereas X₂ is of degree 3.

REMARK 5.2. If the sets X₁, X₂ are up to degree h of the same kind, it is not excluded that they are also up to degree higher than h of the same kind. And so the sets:
X₁={+fy₁y₂,fy₂y₁,+hy₃}

X₂={+fy₃y₁,fy₁y₃,+hy₂}
are of the same kind up to degree 1, 2 and 3.
DEFINITION 5.5. A set X₁ of atomic expressions is a generic extension of degree h of a set X₂ if and only if 1⁰ for every subset Y₂  X₂ there is a subset Y₁  X₁ of the same kind as Y₂ and besides 2⁰ there is a subset Y₃  X₁ of degree h but of a kind different than all the subsets of X₂. In such cases we shall also say that X₁ is a generic extension of X₂ over Y₃.

For instance, the set {fy₂y₁,+fy₁y₂,hy₁} is a generic extension of degree 1 (over the set {hy₁}) and of degree 2 (over the set {fy₂y₁,+fy₁y₂,hy₁}) of the set {fy₁y₂,+fy₂y₁}.

In our further considerations we shall take it for granted that:

ASSUMPTION 5.1. There are m₁ existential and m₂ universal quantifiers in the expression t. Moreover m₁+m₂=m.

ASSUMPTION 5.2. The expression t has a proof P with the minimum length coefficient k (Cf. Definition 2.4). If there are more economic proofs of t, P is freely chosen from among them. Let the graph G (p. 9) be the graph of the proof P and T be whichever tableau of P.

Just as we have discerned one–stage and two stage subclosing pairs (of atomic expressions) we shall distinguish one–stage closing pairs from two–stage ones.

DEFINITION 5.6. If in tableau T both +v and v are elements of the set , then {+v,v} is a one–stage closing pair and when one of the expressions +v, v (called “first member”) belongs to and the other one (called “second member”) to then {+v,v} is a two–stage closing pair.

For example, the pair {+fy₂,fy₂} in Tab. 1 is a one–stage closing pair in subtableau No 2 whereas the pair {+fy₂,fy₂} is a two–stage closing pair in the tableau consisting of the subtableau No 1 and No 11.

OBSERVATION 5.1. It is plain that the set is of a degree not higher than m (Cf. Assumption 5.1) for it embraces (all and only) the atomic expressions that come into being at stage i by transformation of at most m quantifiers of t. Hence the subset of is also of a degree not higher than m. Besides, the set X (Y) to which belong all the members of one–stage and all the second members of two–stage closing pairs present in is also of a degree not higher than m. Moreover, no atomic expressions that belongs to (or ) can be built of more than m y–variables.

COROLLARY 5.1. If the set includes a closing pair, then the pair is of a degree not higher than m.

REMARK 5.3. For that reason we shall confine ourselves to analyzing different sets of atomic expressions of degree hm that can be found in tableau T. Nevertheless, in order to avoid misunderstanding it may be well to add at once that the set is liable to be of a degree higher than m but only its subsets of degree hm can be utilized for creating closing pairs (in if both members of a closing pair belong to or in if the first member belongs to and the second members to ).

We have characterized any tableau in the graph G by means of a sequence . At present we shall determine similarily a tableau T⁺ correlated with the given tableau T. Namely:

DEFINITION 5.7. T⁺ is correlated with T if and only if 1⁰ the following sets occur in turn in the tableau T⁺ (i+s<k, s>0):

and besides

2⁰ two conditions are fulfilled at the same time:

1. 
   ,
   
2. 
   if the set is on the g–th branch (g  n) of (in T), then is on the g–th branch of (in T⁺).
   

If T is homogeneous, T⁺ overlaps T.

Accordingly, we define for T⁺_­: