Computer-Aided Studies of All Possible Shortest Single Axioms for the Equivalential Calculus

ABSTRACT

It has been known since 1939 that for a for­ mula to be a single axiom for the equivalential calculus its length must be at least II, and that single axioms of this length exist. Also, a single axiom of length II must have the two-property. There are 630 formulas with the two-property and of length II. With computer assistance, the authors have shown that 612 of these 630 formulas are not single axioms. The main object of this paper is to outline the methods used to obtain these results. This paper logically precedes a recent paper of L. Wos which announces computer-assisted proofs that a further 5 of the 630 formulas are not single axioms, and should serve as an introduction to the method of schemata mentioned in that paper.

I. THE EQUIVALENTIAL CALCULUS, CONDENSED DETACHMENT, AND THE TWO-PROPERTY

We consider formulas built up from variables p, q, r, ... and a single binary connective E, and written in Polish notation. The "length" of such a formula is the number of ·occurrences in it of E's and variables. Such a formula is called an "equiva­ lential tautology" if it holds in the logical matrix

i.e. if this matrix satisfies it. For example, Epp and EEpqEqp are equivalential tautologies, but Epq and EEpqEpp are not. The matrix (I) is essentially the truth table for material equivalence (p7q)&(q+p) (in Polish notation: KCpqCqp ).

A set S of equivalential tautologies is called a "deductive axiomatization" of the equivalential calculus EC if every equivalential tautology is derivable by the rules of substitution and modus ponens from the formulas in S; if S has just one element x then x is called a "single axiom" for EC. It is known (Kalman, 1983, Theorem I) that a for­ mula is derivable from formulas S by substitution and modus ponens if and only if it is a substitu­ tion instance of a formula derivable from the formulas S by condensed detachment. Here condensed detachment is the rule which, when applied to two formulas x=Euv and y having no variables in common,

J.A. Kalman and J.G. Peterson Department of Mathematics and Statistics University of Auckland, New Zealand

produces the formula w if u and y are unifiable and w=o(v) for some most general unifier a of u and y; w is then unique to within variance (i.e. a formula w' may be produced by applying conden­ sed detachment to x and y if and only if w' is a variant of w), and it is customary to write w=Dxy ; if x and y have variables in common, and y' is a variant of y having no variables in common with x, then Dxy is defined if and only if Dxy' is defined, and if Dxy' is defined we set Dxy=Dxy' . Thus, if S is a deductive axiomatization of EC, and T is a set of equivalential tautologies such that every formula in S is a substitution instance of a formula derivable by condensed detachment from the formulas in T, then Twill be a deductive axiomatization of EC; in particular, if x is a single axiom for EC, and x is derivable by conden­ sed detachment from the equivalential tautology y, then y will be a single axiom for EC. It is known (cf. (i:.ukasiewicz, 1939, §8)) that a shortest single axiom x for EC has length II, and has the "two-property" (Belnap, 1976) that every variable which occurs in x occurs exactly twice in x; also, EEpqEErqEpr is known to be a shortest single axiom for EC (~ukasiewicz, 1939). It is easily seen that there are 630 formulas of length II with the two­ property. However not all of these 630 formulas are single axioms for EC; for instance, the formu­ la EEpqEEqrEpr is not a single axiom for EC. The main object of this paper is to discuss how compu­ ters may be used to help show that formulas such as EEpqEEqrEpr are not single axioms for EC.

2. THEOREM-GENERATING PROGRAM TG

We illustrate in §§3 and 6 how a theorem­ generating program TG, which was originally developed as a tool for showing that particular formulas are derivable from others by condensed detachment, was used to show syntactically that particular formulas are not so derivable.

Given a finite set S of formulas, the program TG generates the set Th(S) of all formulas which may be derived by condensed detachment from the formulas in S. In general, Th(S) is infinite; if Th(S) is finite, then S is not a deductive axioma­ tization of EC. We illustrate in §3 how this may be exploited to show syntactically that 286 of the 630 formulas are not single axioms for EC. In these 286 cases, using minimal instead of arbitra­ ry substitutions enables us to reduce an infinite set of derivable formulas to a finite set.

Although TG is not an interactive program, the user can specify changes, to take place during a run, in certain parameters which control the length of retained formulas and how formulas are selected to be used in subsequent condensed detachments. During each run, statistics of how many condensed detachments have failed and how many have produced formulas which were too long to retain are regu­ larly produced. At the end of each run, a list of all the derived formulas, sorted by length and lex­ icographically for formulas of the same length, is printed out. With these aids, the user can some­ times discover syntactic properties possessed by each of the formulas in a particular set Th(S). We illustrate in §6 how this can be exploited to show syntactically that II of the 630 formulas are not single axioms for EC.

3 . FIRST SYNTACTIC METHOD: FINITENESS

Consider for example the question whether the formula x = EEEpqErpEqr is a single axiom for EC. When the formula x is given as input to the program TG, the formulas Dxx=y=EEEpqpq and Dyx=z=Epp are generated; the program also determines that Dxz=z, Dzx=x , Dzy=y, and Dzz=z, and that all other combi­ nations Dst with s, t € {x ,y,z } are undefined. Since in particular the known single axiom EEpqEErqEpr for EC is not a substitution instance of any of x, y, or z, it follows that x cannot be a single axiom for EC.

In general we may say that a formula x is "of finite type Fn" if (to within variance) the set Th({x }) of formulas generated by x is a finite set with n elements; thus EEEpqErpEqr is of finite type F3. Using TG, we easily find that 286 of the 630 formulas are of finite type Fn for some n =I, 2, 3, 4, 5, 7, 8; since a very large nu~ber of unifi­ cations is involved, computer assistance is invaluable here. It is possible that more than 286 of the 630 formulas are of finite type.

4. MATRIX-TESTING PROGRAM MT

In showing that particular formulas are not single axioms for EC, it is useful to have avail­ able a program MT which, given a logical matrix such as (I) and a particular formula such as EEpqEqp, determines whether or not the matrix satisfies the formula. More generally, given a partially completed matrix M and a finite set S of formulas, MT can search for all ways (if any) of comp l eting M so that it satisfies all the formulas in S; in particular, if M is the void matrix of a given size, MT will search for all matrices of that size which satisfy all the formulas in S.

The purpose of the program MT is similar to that of the interactive program TESTER written by Nuel D. Belnap, Jr. at the University of Pittsburgh and now in us·e by logicians at a number of univer­ sities in the United States, Britain and Australia.

5. SEMANTIC METHOD: LOGICAL MATRICES

A logical matrix M is said to be "normal" if it has the property that whenever a, b € M are such that a and Eab are designated, it follows that b is designated. For example,

is a normal logical matrix; (2) is essentially the truth table for material implication. The matrix (I) is also normal. It is known that a formula x is not a single axiom for EC if and only if there exists a normal logical matrix M, possibly of in­ finite size, such that x holds in M but some equivalential tautology (e.g. some single axiom for EC) does not hold in M. For example, easy calcula­ tions show that the formula EEpqEEqrEpr holds in the matrix (2), but the formula EEpqEErqEpr does not; it follows that EEpqEEqrEpr is not a single axiom for EC.

With the help of a collection of 14 logical matrices, the authors have shown that, of the 630 - 286 = 344 formulas remaining for considera­ tion after eliminating 286 formulas of finite type, 315 are not single axioms for EC. Of the 14 matrices, one (the matrix (2)) is of size 2, 7 are of size 3, 3 are of size 4, 2 are of size 8, and one is of size 10.

The program MT is very useful for checking these results, but has not been of great use in finding the matrices: the 6 matrices of sizes 4, 8, and 10 were in fact all found by hand. There are 4 16 matrices of size 4, and a straightforward search to find which of these satisfy a given for­ mula of length II with the two-property would be far beyond the capacity of MT running on existing computers .

6. SECOND SYNTACTIC METHOD:

FORM OF GENERATED FORMULAS

Of the 344 - 315 = 29 formulas now remaining for consideration, Peterson showed how II could be rejected as single axioms for EC by syntactic argu­ ments based on the form of the formulas generated when these formulas are given as input to the program TG.

Consider for example the question whether the formula x=EpEEEpqEqrr is a single axiom for EC. Examination of the output when x is given as input to the program TG reveals that, apart from the original formula x, all the formulas generated are of the form

where y is x or a formula of the form (3) in which the variables s and t do not occur. In fact, it is easily seen that Dxx=EEExsEstt, and that if z is a formula of the form (3) in which the variables so and to do not occur then (i) Dxz=EEEzsoEsototo,

(ii) Dzx is undefined (since EEysEst and x are not unifiable), and (iii) if Z1=EEEylslEsltltl then

Dzz1 is undefined (since EEysEst and z1 are not unifiable). Since the known single axiom EEpqEErqEpr is not a substitution instance of x or of any of the formulas (3), it follows that xis not a single axiom for EC.

Peterson observed that similar arguments also apply to a further 10 of the 29 formulas not re­ jected by the methods of §§3 and 5. The method of schemata used by the Argonne Automated Reasoning Group in studying EC (cf. (Wos, 1982, p.l3)) also involves studying the possible forms of generated formulas, but in situations more complex than that illustrated above.

7. THE REMAINING 18 FORMULAS

There are proofs in the literature (~ukasie­ wicz, 1939; Peterson, 1976; Kalman, 1978) that II of the remaining 18 formulas are single axioms for EC, but after allowing for these there still re­ main 7 .formulas whose status the present authors were unable to settle. Recently, the Automated Reasoning Group at the Argonne National Laboratory has announced that 2 of these 7 formulas are single axioms for EC and the remaining 5 are not (cf. (Wos, 1982, p.l4)). Proofs that 4 of these formulas are not single axioms for EC are given in (Wos, Winker, Veroff, Smith and Henschen, 1983).

8. CONCLUSION

With the help of the relatively straightfor­ ward programs TG and MT, we succeeded in classifying almost 99% of the 630 formulas with respect to the status of being a single axiom for EC, i.e. in isolating about 1% of these formulas whose status seems the most difficult to deter­ mine. Moreover, it appears likely that the methoas of finiteness (§3) and matrix-testing (§5) de­ scribed in this paper, or essentially equivalent methods, would be employed in any study of all the possible shortest single axioms for EC, and the method of examining the form of generated formulas (§6) is closely related to the method of schemata employed by the Argonne Automated Reasoning Group in completing the classification of the 630 for­ mulas. Our programs probably did not have the capacity to carry the task of classifying these formulas to final completion (cf. (Wos, 1982, P· 7)).

We believe that mechanical theorem-proving using unification-based inference rules such as condensed detachment and resolution, and the study of Hilbert-type sentential calculi like the equi­ valential calculus, are two subjects which have much to offer each other. The theorem-provers can be genuinely useful tools in studying the calculi, and the calculi provide a promising field of application for the theorem-provers (cf. (Kalman, 1982, §6)). In such mechanical studies of other calculi, the methods illustrated in this paper should find further applications.