![]() Leon Gumański
ASSUMPTION 3.1. Each of the sets Q1, Q2,…,Qq (q=1+n+…+nk–1) in any k–stage tableau–construction of t is ordered according to the same principle. DEFINITION 3.4. When Let us return for a while to the tableau–construction represented in Tab. 4. The comparison of the set OBSERVATION 3.3. The sets Qf, Qg (f,gq) 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 Qf, then a y–variable has also been introduced by virtue of the same rule in place p in Qg. CONVENTION 3.2. One is allowed to say that DEFINITION 3.5. If there exists such an atomic expression v that For instance, the pair {+fy2,fy2} 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 substitutions 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:
The pair {+fy1,fy2} is a one–stage pair because the substitution x3/y2 is also permissible at stage 1 and would give us a closing pair {+fy2,fy2} instead of the pair {+fy1,fy2}. DEFINITION 3.8. When a distinguished pair In other words, if there is a two–stage pair 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 Tj is closed, the closure is achieved due to a closing pair {+v,v}. If the pair is not in 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–construction 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–construction of t consists of no more than one tableau (i. e. n=1), then the graph G (p. 9) reduces to
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 inapplicable has at most 2 stages. PROOF. According to Remark 2.7 the sole tableau of the proof is homogeneous and by Lemma 3.1 there must be in 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–variables (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 continued 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: (a1)(a2)…(am)w where the matrix w contains no other individual variables than a1,a2…,am. When building a tableau–construction of t, F(a) is the only applicable rule for quantifiers in this case and at stage 1 one obtains n subtableaux in which the atomic expressions belonging to the sets ![]() LEMMA 5.1. If a set PROOF. This is visible from the k–stage homogeneous tableau T of which 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: (Ea1)(Ea2)…(Eam)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: ![]() ![]() 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 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 {+fy1y1,+fy1y2,gy2y1} is of degree 2. The sets DEFINITION 5.2. Sets X1, X2 of atomic expressions are of the same kind if and only if X1 comes into being from X2 as an effect of simultaneously substituting certain variables for some (or all) individual variables occurring in the elements of X2 and at the same time X2 comes into being from X1 as a result of reverse substitutions (substitutions b/a are reverse of the substitutions a/b). EXAMPLES. The following sets X1, X2 are of the same kind:
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 DEFINITION 5.3. The kind of a set X of atomic expressions is an equivalence class (abstraction class) generated by X with respect to the relation of being of the same kind. DEFINITION 5.4. Sets X1, X2 of atomic expressions are up to degree h of the same kind if and only if 10 both sets X1, X2 are at least of degree h and 20 for every subset Y1 X1 of a degree not higher than h there is a subset Y2 X2 of the same kind as Y1 and conversely: for every subset Y2 X2 of degree not higher than h there is a subset Y1 X1 of the same kind as Y2. For instance, the sets X1={fy1y2,+hy1}, X2={+fy1y2,fy2y1,+hy3} are only to degree 1 of the same kind though the set X1 is of degree 2 whereas X2 is of degree 3. REMARK 5.2. If the sets X1, X2 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:
For instance, the set {fy2y1,+fy1y2,hy1} is a generic extension of degree 1 (over the set {hy1}) and of degree 2 (over the set {fy2y1,+fy1y2,hy1}) of the set {fy1y2,+fy2y1}. In our further considerations we shall take it for granted that: ASSUMPTION 5.1. There are m1 existential and m2 universal quantifiers in the expression t. Moreover m1+m2=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 For example, the pair {+fy2,fy2} in Tab. 1 is a one–stage closing pair in subtableau No 2 whereas the pair {+fy2,fy2} 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 COROLLARY 5.1. If the set REMARK 5.3. For that reason we shall confine ourselves to analyzing different sets of atomic expressions of degree hm that can be found in tableau T. Nevertheless, in order to avoid misunderstanding it may be well to add at once that the set We have characterized any tableau in the graph G by means of a sequence DEFINITION 5.7. T+ is correlated with T if and only if 10 the following sets occur in turn in the tableau T+ (i+s<k, s>0):
and besides 20 two conditions are fulfilled at the same time:
If T is homogeneous, T+ overlaps T. Accordingly, we define for T+: Yüklə 0,58 Mb. Dostları ilə paylaş: |