UDC 51.01:164

MATHEMATICS

S. Yu. MASLOV

APPLICATION OF THE INVERSE METHOD FOR ESTABLISHING DERIVABILITY TO THE THEORY OF DECIDABLE FRAGMENTS OF THE CLASSICAL PREDICATE CALCULUS

(Presented by Academician P. S. Novikov on 6 III 1966)

1. Recently the possibilities of automating proof processes have been intensively studied. Numerous works have appeared both in the field of the theory of logical inference (see, for example, \((^{1-7})\)) and in the field of constructing algorithms and machine programs for searching for a derivation. In \((^7)\) a new method is proposed for establishing the derivability of formulas of the classical predicate calculus, called the inverse method. This method is convenient for constructing machine algorithms and programs for searching for logical inference (it makes it possible, by purposefully relying on the specific features of the formulas being tested, to restrict the enumeration arising under the direct application of Herbrand’s theorem, and to obtain derivations that do not contain superfluous applications of quantifier rules). In addition to its practical aspect, the inverse method has properties that make it a convenient apparatus for the theoretical consideration of questions of derivability, for establishing decidable classes of formulas and classes of reduction. Proofs of decidability for almost all decidable classes available in the literature are covered by a single scheme; at the same time it becomes possible to extend known classes and to obtain new decidable classes. The purpose of the present communication is to demonstrate the possibilities of the inverse method as an apparatus of the theory of derivability. We shall use the terminology of \((^7)\)*.

2. Let \(F\) be a closed formula of the form \(P(D_1 \& \ldots \& D_\delta)\), where \(P\) is a prefix and \(D_1,\ldots,D_\delta\) are simple disjunctions. We shall say that an \(F\)-set \(H\) is favorable with respect to the \(F\)-sets \(H^0,\ldots,H^s\) if \(H\) can be obtained by rules A and B, regarding \(H^0,\ldots,H^s\) as favorable. We shall say that an \(F\)-set \(\{(i_1,\ldots,i_{h_1}, i_{h_1+1},\ldots,i_{h_2}), S\}\) is decomposable into the sets \(\{(i_1,\ldots,i_{h_1}), S_1\}\) and \(\{(i_{h_1+1},\ldots,i_{h_2}), S_2\}\), if, whatever the realizations \(R_1\) of the bundle \(S_1\) and \(R_2\) of the bundle \(S_2\) may be, having in their composition common variables (with the exception of variables occupying positions corresponding to external universal quantifiers), by assigning \(R_2\) to the right of \(R_1\), we obtain a realization of the \(F\), \(h_2\)-bundle \(S\). Inductively on \(l\) the relation “the set \(H\) is decomposable into the sets \(H_1,\ldots,H_l\)” is defined. The following lemma is easily obtained (cf. item 4 of \((^7)\)).

Lemma. Let \(H\) be decomposable into \(H_1,\ldots,H_l\). For any \(F\)-sets \(H^1,\ldots,H^s\), the empty set is favorable with respect to \(H, H^1,\ldots,H^s\) if and only if it is favorable with respect to each group
\(H_i, H^1,\ldots,H^s\) \((i=1,2,\ldots,l)\).

* In \((^7)\), on p. 17, the expression in square brackets occurring in condition b) of the definition of an \(F\)-list should be read as follows:

\[ [\forall j'(j' < j \supset a_{i,j'} = a_{i',j'}) \& (a_{i,j} \ne a_{i',j})]. \]

On p. 20 the prefix of formula (6) should be read as follows:

\[ \forall x_1 \ldots \forall x_\varphi \exists x_{\varphi+1} \ldots \exists x_\psi \forall x_{\psi+1} \ldots \forall x_\xi . \]

Thus, in the process of constructing favorable sets when a decomposable set is obtained, we can branch the process into several processes, each of which is simpler than the unbranched one.

3. Let us denote the classical first-order predicate calculus by \(C\), and the same calculus with function symbols by \(C'\). In this article we consider only such formulas of the calculus \(C'\) that: 1) the bound variables of the formula are distinct from the free ones and from one another; 2) among the propositional connectives, only \(\&\), \(\vee\), and \(\neg\) occur in the formula, and negation may stand only before elementary formulas. (It is obvious that for every formula of the calculus \(C'\) one can construct an equivalent one having the indicated properties.)

Let \(F\) be a formula and let \(G\) be some elementary subformula of it. The \(F\)-prefix of the formula \(G\) will mean the quantifier prefix obtained in the following way: the formula \(F\) is read from left to right, and, one after another, those quantifier complexes are written down which bind variables occurring in \(G\). The literature contains numerous examples of decidable classes that are singled out from the class of all prenex formulas by conditions restricting the form of the prefix of the formula and the form of the elementary subformulas of the formula. Often a simple reformulation of the description of such a decidable class in terms of admissible \(F\)-prefixes reveals possibilities for extending this class.

A well-known example of this kind is the generalization, contained in \((^1)\), IV (p. 247), of the monadic fragment of the calculus \(C\), which comprises the class of such formulas of the calculus \(C\) that all nonempty \(F\)-prefixes have length \(1\). Another example is the decidable class of formulas of the calculus \(C\) all of whose nonempty \(F\)-prefixes end with a universal quantifier (this class is substantially broader than class IX cited in \((^1)\) on p. 248). Moreover, the class \(K\) described below is decidable; it is at the same time a generalization of the two classes just mentioned, as well as of the Gödel classes (classes VI and VII from \((^1)\)), the Skolem class (class VIII from \((^1)\)), and Friedman’s classes \((^4)\). We shall say that a formula \(F\) of the calculus \(C\) belongs to \(K\)* if it is possible to indicate quantifier complexes \(\exists x_1, \ldots, \exists x_k\), not lying within the scope of any universal quantifier, such that in \(F\), apart from empty \(F\)-prefixes, only \(F\)-prefixes of length \(1\), \(F\)-prefixes ending with a universal quantifier, and the \(F\)-prefix

\[ \exists x_1 \ldots \exists x_k \]

may occur.

Theorem. The class of arbitrary disjunctions of formulas from \(K\) is decidable with respect to derivability.

We outline the proof. Let \(F\) be a formula from \(K\). Without loss of generality, one may assume that \(F\) has the form

\[ \bigvee_{i=1}^{m} F_i, \]

where: 1) \(F_i \in K\); 2)

\[ F_i=\exists x_1^i \ldots x_{k_i}^i P_i\ \&\ \bigwedge_{j=1}^{\delta_i} D_{i,j}, \]

where \(x_1^i,\ldots,x_{k_i}^i\) are the distinguished variables from the definition of the class \(K\), \(P_i\) is the quantifier prefix, and \(D_{i,j}\) are simple disjunctions. Let \(G\) be an elementary formula, its predicate symbol occurs in \(F\), all variables entering into \(G\) enter into \(F\), and the \(F\)-prefix of \(G\) belongs to one of the types listed in the definition of the class \(K\). If some one of the formulas \(D_{i,j}\) does not contain \(G\), then replace it by the formula

\[ (D_{i,j}\vee G)\ \&\ (D_{i,j}\vee \neg G). \]

As a result of a finite number of steps of this type, in which all elementary formulas satisfying the conditions imposed on \(G\) figure as \(G\), we obtain—

* This same class is decidable also in the calculus \(C'\). Moreover, by the inverse method (extending it in the natural way to the calculus \(C'\)) one can prove the decidability of the class of such formulas \(F\) of the calculus \(C'\) that in each \(F\)-prefix all quantifiers, except perhaps the last, are universal quantifiers. In this connection let us note that the decidability of the class of formulas of the form \(\exists x\,M\), where \(M\) is a quantifier-free formula of the calculus \(C'\), was obtained by V. P. Orevkov \((^3)\) (also by means of the inverse method).

some formula \(F'\). We shall call such a process saturation, and the formulas obtained as a result of this process saturated. Suppose also that for any \(j\) \(\left(2 \leq j \leq \max_{1\leq i\leq m}\{k_i\}\right)\) there is a formula \(F_{j'}\) such that \(k_{j'}=j\) (if there is no such formula, it can be added fictitiously and saturation can be applied).

We now apply to \(F'\) the inverse method (extended, as indicated in § 5 of (7), to the case of disjunctions of preliminary formulas) *. Let \((i,(\alpha_1,\ldots,\alpha_{k_i},\ldots,\alpha_{n_i}))\) be a member of the \(F'\)-list **. By the content of this member we shall mean the set of those numbers from the list \(\alpha_1,\ldots,\alpha_{k_i}\) that are distinct from the numbers of free variables. We shall call this member general if its content has \(k_i\) elements. We shall make use of one characteristic device: instead of arbitrary \(F'\)-lists we shall consider \(F'\)-lists of a special kind, but such as ensure a complete enumeration of the required substitutions. In our case it is convenient to allow \(F'\)-lists in which, before any nongeneral member whose content has more than one element, there stands a general member with the same content.

If \(F'\) is derivable, then in one step of applying rule B one can justify the favorability of a set decomposable into some free \(H_1\) and some one-member \(H_2\) not containing \(F'\)-chains. Carrying out induction on the number of applications of rule B and using the lemma, we obtain that, in order to justify the favorability of the empty set, it is sufficient to justify the favorability of only a finite number of sets, i.e., in a finite number of steps we shall be convinced of the derivability of \(F'\) or of its nonderivability.

1. We indicate two generalizations of the theorem just given. We shall say that a formula \(F\) of the calculus \(C\) belongs to \(K'\) if all quantifier complexes from \(F\) can be divided into groups \(\Gamma_1,\ldots,\Gamma_l\) such that: 1) there are no \(F\)-prefixes in which complexes from different groups occur; 2) in each group \(\Gamma_i\) one can indicate complexes \(\exists x^i_1,\ldots,\exists x^i_{k_i}\) such that the scope of any complex of the form \(\forall y\) embracing \(\exists x^i_{k_i}\) embraces all complexes from \(\Gamma_i\); 3) any nonempty \(F\)-prefix either has length 1, or ends with a universal quantifier, or has the form \(\exists x^i_1\ldots \exists x^i_{k_i}\), where \(1\leq i\leq l\). The class \(K'\) is decidable with respect to derivability.

In (3) decidability with respect to derivability was established for the class of all formulas of the calculus \(C\) of the form

\[ \exists x_1x_2\forall y_1\ldots y_s\exists x_3M, \tag{1} \]

where \(M\) is quantifier-free and \(\exists x_3\) occurs only in the (1)-prefixes \(\exists x_3\) and \(\exists x_1\exists x_3\). We shall say that a formula \(F\) of the calculus \(C\) belongs to the class \(K''\) if \(F\) has the form

\[ P_1QxP_2\exists x'M, \tag{2} \]

where \(P_1\) and \(P_2\) are quantifier prefixes, \(Q\) is a quantifier, \(M\) is a quantifier-free formula, \(\exists x'\) occurs only in the (2)-prefixes \(\exists x'\) and \(Qx\exists x'\), and the formula

\[ P_1QxP_2S_{xx'}M \]

belongs to \(K'\). The class \(K''\) is decidable with respect to derivability.

For the proof, a not limiting generality assumption is introduced: (3) contains complexes \(\exists x_1\) and \(\exists x_2\) (where \(x_1\) or \(x_2\) may coincide with \(x\)) such that among the (3)-prefixes there is \(\exists x_1\exists x_2\). (If such complexes are not found, we can add them fictitiously and apply saturation.) In our case it is convenient to allow (2)-lists possessing

* True, in (7) the inverse method was described for closed formulas, while here we have in mind the trivial modification of the method for the case of nonclosed formulas.
** Here \(n_i\) is the length of the prefix of the formula \(F_i\).

with the special property: before any \(n\)-tuple\(^*\) \(I\), in which unequal numbers\({}^{**}\) stand in the positions corresponding to the variables \(x\) and \(x'\) (denote them by \(\alpha\) and \(\beta\), respectively), there occurs: a) an \(n\)-tuple differing from \(I\) in that \(\alpha\) stands in the last position instead of the number \(\beta\); b) an \(n\)-tuple in which \(\alpha\) and \(\beta\) stand in the positions corresponding to \(x_1\) and \(x_2\).

If we now consider saturated formulas of the form (2), then every application of rule B to closed sets in which the \(n\)-tuple corresponding to the last term is inessential can be replaced by an application of rule B by which a favorable set of length 1 or 2 is obtained; the \(n\)-tuples corresponding to the members of this set are essential, and among the other dependencies there is only the equality of two certain elements. Such a favorable set is easily modeled by a closed one, and the question of whether the initial formula is derivable reduces to the problem of derivability using only essential \(n\)-tuples (or, what is the same thing, to the problem of derivability for the class \(K'\)).

Analogously one can prove that the class of arbitrary disjunctions of formulas from the class \(K''\) is decidable with respect to derivability. We note that only for convenience of formulation did we define \(K''\) as a class of prenex formulas. It is not difficult to redefine the class \(K''\) so that it is formally an extension of the class \(K'\).

1. In conclusion let us indicate the proofs of decidability, by means of the inverse method, for certain classes of formulas of the classical predicate calculus known in the literature. Let us first dwell on Church’s list \(({}^{1})\), § 46\({}^{***}\). Cases III, IV, VI, VII, VIII, IX, XII, and XIII simply satisfy the conditions of our theorem. The decidability of classes I and II by means of saturation is established trivially. A formula of class V′ (and analogously of class XI′) is derivable if and only if there is at least one closed set. The more general classes V and XI reduce respectively to V′ and XI′ with the aid of our lemma. Class XIV is easily reduced to class I by modeling the closed sets arising from elementary formulas with predicate variables \(g_1, \ldots, g_N\), by closed sets containing no variables \(c_1, \ldots, c_l\) at all. The decidable classes from \(({}^{3,4,8})\) have already been indicated as covered by the inverse method. To these we shall also add the classes \(L\) and \(L^*\) from \(({}^{6})\), which are contained in \(K''\). Let us also mention the class of formulas of the form (6) from \(({}^{7})\), decidable by virtue of the finiteness of the number of possible favorable sets. The last class that we shall consider in this connection is Krom’s decidable class \(({}^{5})\). The proof of decidability of this class by the inverse method is easily achieved by saturation. At the same time it becomes clear that conditions (2) \((({}^{5}), p. 1306)\) can be weakened by replacing them with the requirement that there be no closed sets for noncoinciding elementary formulas.

Thus, for only a few classes known to the author (the class \(X\) from \(({}^{1})\), containing a finite number of formulas, and the classes \(M\) and \(M^*\) from \(({}^{6})\)) do the proofs of decidability require, in addition to the indicated techniques, the introduction of additional considerations.

Leningrad Branch
of the V. A. Steklov Mathematical Institute
Academy of Sciences of the USSR

Received
3 III 1966

REFERENCES

\({}^{1}\) A. Church, Introduction to Mathematical Logic, 1, Moscow (1960).
\({}^{2}\) M. Davis, Symp. in Appl. Math. Proceedings, 15, 1963, p. 45.
\({}^{3}\) B. S. Dreben, Proc. Harvard Symp. of Dig. Comp. and Their Appl., 1962, p. 32.
\({}^{4}\) J. Friedman, J. Assoc. Comput. Machinery, 10, 1, 1 (1963).
\({}^{5}\) M. R. Krom, Pacif. J. Math., 14, 4, 1305 (1964).
\({}^{6}\) Hao Wang, Proc. Symp. Math. Theory of Machines, 1964, p. 23.
\({}^{7}\) S. Yu. Maslov, DAN, 159, No. 1 (1964).
\({}^{8}\) V. P. Orevkov, II Symp. on Cybernetics (Abstracts), 1965, p. 176.

\(^*\) By \(n\) is denoted the length of the prefix of formula (2).

\({}^{**}\) Such an \(n\)-tuple will below be called inessential.

\({}^{***}\) We have in mind that before testing a formula for derivability one should reveal all connections of the propositional calculus that can be revealed without removing quantifiers. Only after this do we begin to test the derivability of each of the resulting formulas in the predicate calculus. In Church’s terminology this means the use of theorem 465.