MATHEMATICS

S. Yu. MASLOV

AN INVERSE METHOD FOR ESTABLISHING DERIVABILITY IN THE CLASSICAL PREDICATE CALCULUS

(Presented by Academician P. S. Novikov on 14 V 1964)

The term “predicate calculus” below means the narrow classical predicate calculus; the terms “derivation” and “derivable formula” refer to this calculus. We take the object variables of the language of the predicate calculus to be \(x_1, x_2,\ldots\); the letters \(i, j, h, q, r, n\) and lowercase Greek letters (possibly with subscripts or primes) are used as metavariables for positive integers. The expressions \(D_i\) and \(D_{i,j}\) denote formulas of the form \((E_1 \vee \cdots \vee E_\varepsilon)\), where \(E_r\) is an elementary formula or the negation of an elementary formula \((r=1,2,\ldots,\varepsilon)\).

1. Let \(F\) be a closed formula of the form

\[ Q_1x_1 \ldots Q_nx_n \, (D_1 \& \ldots \& D_\delta), \tag{1} \]

where \(Q_1,\ldots,Q_n\) are quantifiers. Let

\[ (\alpha_{1,1},\ldots,\alpha_{1,n}),\ldots,(\alpha_{q,1},\ldots,\alpha_{q,n}) \tag{2} \]

be a list of \(n\)-term systems of numbers (abbreviated: \(n\)-ss).

(2) is called a resolvent of the formula \(F\), or an \(F\)-list, if:

a) all members of the list are distinct;

b) \(\forall ij\{(i \leq q \& j \leq n \& Q_j \text{ is the universal quantifier}) \supset [[\forall i'j'\,(i' < i \supset \neg \alpha_{i,j} \ne \alpha_{i',j'}) \& \forall j'(j' < j \supset \neg \alpha_{i,j} \ne \alpha_{i,j'})] \vee \exists i'(i' < i \& \forall j'(j' \leq j \supset \alpha_{i',j'}=\alpha_{i,j'}))]\};\)

c) \(\forall ii'j\{[\forall j'(j' < j \supset \alpha_{i',j'}=\alpha_{i,j'}) \& (\alpha_{i'j}\ne \alpha_{i,j})] \supset Q_j \text{ is the existential quantifier}\}.\)

An \(F\)-list (2) is called complete if every formula of the form*

\[ \left( \left. S^{x_1,\ldots,x_n}_{x_{\alpha_{1,1}},\ldots,x_{\alpha_{1,n}}} D_{i_1} \vee \cdots \vee S^{x_1,\ldots,x_n}_{x_{\alpha_{q,1}},\ldots,x_{\alpha_{q,n}}} D_{i_q} \right) \quad (i_1 \leq \delta,\ldots,i_q \leq \delta) \tag{3} \]

is derivable. A complete \(F\)-list is called irreducible if none of its proper sublists is complete.

From Herbrand’s theorem\({}^{2}\) it follows that the formula \(F\) is derivable if and only if a complete \(F\)-list can be constructed. In many works a method of searching for a derivation is considered that is based on fixing one or another way—common to all formulas—of generating resolvents, in which each subsequent resolvent includes the preceding one, and on checking their completeness. Under any such generation method that ensures a proof of derivability for every derivable formula, it usually turns out, for concrete formulas, that the generated resolvents contain superfluous members. At the Leningrad seminar on mathematical logic in 1962, N. A. Shanin proposed a method for searching for derivations of formulas of the predicate calculus by introducing metavariables. For formulas of the form (1), according to this method, instead of lists of the form (2), analogous lists of variables for natural numbers are generated, and one seeks a substitution of variables under which an irreducible list of the form (2) is obtained. The idea of the metavariable method served as the starting point for the author’s considerations. Below a method is described which makes it possible, by expediently relying on

* \(S\) is the operation of substituting lower variables for upper ones; see \({}^{1}\).

specific features of the formulas being tested, and to organize economically, for each derivable formula \(F\), the construction of an irreducible \(F\)-list. The search for such an \(F\)-list is carried out by discovering the manner of formation of its last terms, then the manner of formation of the terms preceding the last ones, etc. (In connection with this, the proposed method is called the inverse method)*.

1. Let \(F\) be a formula of the form (1). Denote by \(M\) the number of universal quantifiers in \(F\), and, for each \(i\), denote by \(K_i\) the number of existential quantifiers preceding in (1) the \(i\)-th universal quantifier \((i = 1, \ldots, M)\). Introduce \(2^{K_i}-1\) signs
   \(f^i_{j_1,\ldots,j_\nu}\), where \(\nu \leq K_i\) and \(j_1 < \cdots < j_\nu \leq K_i\) \((i=1,\ldots,M)\). For each \(h\), an \(F,h\)-atom will mean any pair \((\alpha,\beta)\) such that \(\alpha \leq n,\ \beta \leq h\). Define inductively the notions of an \(F,h\)-chain and an \(F\)-chain: 1) all \(F,h\)-atoms are \(F,h\)-chains, and all positive integers are \(F\)-chains; 2) if \(T_1,\ldots,T_\nu\) are \(F,h\)-chains (\(F\)-chains), then the expression
   \(f^i_{j_1,\ldots,j_\nu}(T_1,\ldots,T_\nu)\) is an \(F,h\)-chain (respectively, an \(F\)-chain). An \(F,h\)-bundle will mean any list of expressions of the form \(A \asymp T\), where \(A\) is an \(F,h\)-atom and \(T\) is an \(F,h\)-term. Let
   \(i', j_1,\ldots,j_\nu\) be the numbers, in the list of quantifiers \(Q_1,\ldots,Q_n\), of the \(i\)-th universal quantifier and of the \(j_1\)-st, \(\ldots\), \(j_\nu\)-th existential quantifiers. We say that on an \(F\)-list \(P\) the relation
   \(\alpha \asymp f^i_{j_1,\ldots,j_\nu}(\alpha_1,\ldots,\alpha_\nu)\) is satisfied if in \(P\) there is an \(n\)-tuple in which the \(i'\)-th number is equal to \(\alpha\), and the \(j_1'\)-th, \(\ldots\), \(j_\nu'\)-th numbers are equal to \(\alpha_1,\ldots,\alpha_\nu\), respectively. We shall say that on \(P\) the relation
   \(\alpha \asymp f^i_{j_1,\ldots,j_\nu}(T_1,\ldots,T_\nu)\), where \(T_1,\ldots,T_\nu\) are \(F\)-chains, is satisfied if there exist numbers \(\alpha_1,\ldots,\alpha_\nu\) such that on \(P\) the relations
   \(\alpha \asymp f^i_{j_1,\ldots,j_\nu}(\alpha_1,\ldots,\alpha_\nu)\),
   \(\alpha_1 \asymp T_1,\ldots,\alpha_\nu \asymp T_\nu\) are satisfied.

Let \(R\) be an \(F\)-list some of whose terms are marked. If \((\alpha,\beta)\) is an \(F,h\)-atom, where \(h\) is the number of terms marked in \(R\), then the \(\alpha\)-th number of the \(\beta\)-th marked \(n\)-tuple is called the number conjugate with \((\alpha,\beta)\). We shall call \(R\) a realization of the \(F,h\)-bundle \(S\) if, replacing each atom occurring in \(S\) by the number conjugate with that atom, we obtain relations satisfied on \(R\). A bundle is called correct if its realization can be constructed. For any \(h,h', i_1,\ldots,i_h\) such that
\(h \leq h'\) and \(i_1 < \cdots < i_h \leq h'\), an \(F,h\)-bundle \(S\) is called a subbundle of the \(F,h'\)-bundle \(S'\) by the characteristic \((i_1,\ldots,i_h)\) if, whatever realization of the bundle \(S'\) is taken, by leaving marked in it only the \(i_1\)-st, \(\ldots\), \(i_h\)-th of the marked terms, we obtain a realization of the bundle \(S\). An \(F,(h+1)\)-bundle \(S'\) is called an extension of the \(F,h\)-bundle \(S\) if to any realization \(R\) of the bundle \(S\), whose last term is marked, one may add on the right one or several \(n\)-tuples so that there is obtained an \(F\)-list in which the last term and the terms marked in \(R\) are marked, and a realization of the bundle \(S'\) is obtained. It is not difficult to give purely syntactic definitions of the concept “correct bundle” and of the relations: “\(S\) is a subbundle of \(S'\) by the characteristic \(\Xi\),” “\(S'\) is an extension of \(S\),” which show the algorithmic solvability of these concepts.

1. Let \(F\) be a formula of the form (1). An \(F\)-set will mean any pair \(\{C,S\}\), where \(C\) is a list of positive integers not exceeding \(\delta\) (the number of terms of this list will be called the length of the \(F\)-set), \(S\) is a correct \(F,h\)-bundle, and \(h\) is the length of the \(F\)-set**. An \(F\)-set \(\{C,S\}\) will be called a subset (a subset with a common end) of an \(F\)-set \(\{C',S'\}\) if one can construct numbers \(i_1,\ldots,i_h\) such that:

* Another method of economical search for a proof is presented in a recent paper of Davis \((^3)\). Below, in item 4, the advantages of the inverse method are noted.

** The case is not excluded in which \(C\) and \(S\) are empty lists. The pair \(\{\, ,\,\}\) will be called the empty set.

1) \(i_1 < \ldots < i_h \le h'\) (respectively \(i_1 < \ldots < i_h = h'\)), where \(h\) is the length of the set \(\{C,S\}\), \(h'\) is the length of the set \(\{C',S'\}\); 2) \(C\) consists of the \(i_1\)-st, \(\ldots\), \(i_h\)-th numbers of the list \(C'\); 3) \(S\) is a sublinkage of \(S'\) with characteristic \((i_1,\ldots,i_h)\). A subset \(H'\) of an \(F\)-set \(H\) is called proper if \(H\) is not a subset of \(H'\). An \(F\)-set \(\{(i_1,\ldots,i_q), S\}\) will be called closed if, for any realization \(R\) of the linkage \(S\), the formula (3) is derivable, where \((\alpha_{1,1},\ldots,\alpha_{1,n}),\ldots,(\alpha_{q,1},\ldots,\alpha_{q,n})\) is the list of marked terms of \(R\).

Let us define, by the following generating rules, the notion of a favorable \(F\)-set:

A. If \(H\) is a closed \(F\)-set and no proper subset of it is closed, then \(H\) is a favorable \(F\)-set.

B. Let \(H_1,\ldots,H_\delta\) be favorable \(F\)-sets and let \(H\) be the \(F\)-set \(\{(i_1,\ldots,i_h), S\}\), possessing the following property: one can construct an extension \(S'\) of the linkage \(S\) such that \(H_1,\ldots,H_\delta\) are respectively subsets with common end of the sets \(\{(i_1,\ldots,i_h,1), S'\},\ldots,\{(i_1,\ldots,i_h,\delta), S'\}\). If no proper subset of \(H\) has the same property, then \(H\) is a favorable \(F\)-set.

Theorem. Whatever the formula \(F\) of the form (1) may be, \(F\) is derivable if and only if the empty set is a favorable \(F\)-set.

The proposed method for establishing derivability of the formula \(F\) consists in the following: by rules A and B, favorable \(F\)-sets are constructed successively until the empty set is obtained (after which it is easy to construct an irreducible \(F\)-list and a derivation of the formula \(F\)).

Example. Let us verify the derivability of the formula

\[ \exists x_1 \forall x_2 \exists x_3 \exists x_4 \forall x_5 (\neg Fx_1x_2x_3 \vee Fx_2x_3x_5)\ \&\ (Gx_1x_2x_4 \vee \neg Gx_2x_4x_5 \vee \neg Fx_1x_2x_4). \tag{4} \]

The closed sets are:

\[ \{(1,1),\ ((2,1) \simeq (1,2),\ (3,1) \simeq (2,2),\ (5,1) \simeq (3,2),\ (3,1) \simeq f^1_1(2,1))\}, \tag{a} \]

\[ \{(1,2),\ ((2,1) \simeq (1,2),\ (3,1) \simeq (2,2),\ (5,1) \simeq (4,2),\ (3,1) \simeq f^1_1(2,1))\}, \tag{b} \]

\[ \{(2,2),\ ((2,1) \simeq (1,2),\ (4,1) \simeq (2,2),\ (5,1) \simeq (4,2),\ (4,1) \simeq f^1_1(2,1))\}. \tag{c} \]

From (a) and (b), by rule B, we obtain

\[ \{(1),\ ((3,1) \simeq f^1_1(2,1))\}. \tag{d} \]

From (d) and (c) we obtain

\[ \{(2),\ ((4,1) \simeq f^1_1(2,1))\}. \tag{e} \]

From (d) and (e) we obtain the empty set. Therefore, (4) is derivable. Its irreducible resolvent is the list:

\[ (1,2,3,4,5),\quad (2,6,7,8,9),\quad (1,2,6,6,10),\quad (6,11,12,13,14), \]

\[ (2,6,11,10,15),\quad (6,11,15,15,16),\quad (2,6,10,10,17). \]

4. Let us note one feature of the inverse method which constitutes its principal advantage over the known methods of searching for a derivation. In constructing favorable \(F\)-sets, the obtaining of each new set, generally speaking, simplifies the problem of establishing the derivability of \(F\). In a number of cases, when considering a derivable formula \(F\), having established the favorability of some \(F\)-set, we obtain the possibility of proving the derivability of \(F\) by indicating one or several formulas \(F_1,\ldots,F_\varepsilon\), each of which is derived more simply than \(F\), and a scheme according to which the derivations of these formulas are rearranged into the required derivation. Sometimes, by means of such a reduction, the derivability of \(F\) can be justified even when its derivation is too large to survey. Without dwelling on the various possibilities of such use of the inverse method, we shall indicate the simplest one.

Let \(F\) be a formula of the form (1). An \(F\)-set \(\{C,S\}\) is called free if \(S\) is the empty list. From the favorability of a free \(F\)-set \(\{C,S\}\) it follows that \(C\) is a list without repetitions. If the \(F\)-set \(\{(1,\ldots,\delta'),S\}\),

where \(\delta' \leqslant \delta\), is a free favorable \(F\)-set, then \(F\) is derivable if and only if the formulas \(F_1,\ldots,F_{\delta'}\) are derivable, where

\[ F_i = Q_1x_1\ldots Q_nx_n(D_1\&\ldots\&D_{i-1}\&D_{i+1}\&\ldots\&D_\delta) \quad (i=1,\ldots,\delta')^* . \]

1. Let \(F\) be a formula of the form

\[ \bigvee_{i=1}^{r} Q_{i,1}x_1\ldots Q_{i,n_i}x_{n_i} \left(\bigwedge_{j=1}^{\delta_i} D_{i,j}\right), \tag{5} \]

where \(Q_{1,1},\ldots,Q_{r,n_r}\) are quantifiers. All the definitions of §§ 2–4 and the results of §§ 3 and 4 are not difficult to generalize to this case. We shall indicate only what type of objects the \(F\)-lists, \(F,h\)-atoms, and \(F\)-sets are in this case:
1) an \(F\)-list is a list of pairs \((\rho,P)\), where \(\rho \leqslant r\) and \(P\) is an \(n_\rho\)-tuple of positive integers;
2) an \(F,h\)-atom is a triple of numbers \((\alpha,\beta,\gamma)\), where \(\alpha \leqslant n_\gamma\), \(\beta \leqslant h\), \(\gamma \leqslant r\);
3) an \(F\)-set is a pair \(\{C,S\}\), where \(C\) is a list of pairs \((\mu,\nu)\) (here \(\mu \leqslant r\), \(\nu \leqslant \delta_\mu\)) and for each atom \((\alpha,\beta,\gamma)\) from \(S\), in the \(\beta\)-th term \((\mu,\nu)\) of the list \(C\), \(\mu=\gamma\). By a further complication of the notions it is not difficult to cover by the inverse method also formulas that are disjunctions of formulas of the form

\[ Q_1x_1\ldots Q_nx_n \left(\bigvee_{i=1}^{\mu}\bigwedge_{j=1}^{\delta_i} D_{i,j}\right). \]

Remark. The transfer of the inverse method to the case of the classical predicate calculus with constant functional symbols does not present fundamental difficulties.

1. In constructing all possible favorable \(F\)-sets, a situation may arise in which the empty set has not yet been constructed, but either no new application of rule Б is possible, or every application of rule Б gives rise to an \(F\)-set having, as its subset, some \(F\)-set already constructed. In this case \(F\) is not derivable. Other cases are also possible when, in a finite number of steps, it becomes clear that the empty set is not contained among the favorable \(F\)-sets. For some solvable classes (in particular, for all the solvable classes of formulas of the form (1) listed in (¹)) these considerations lead to a decision algorithm for determining the favorability of the empty set.

Let us note that in the case when \(F\) has the form (5) and all quantifier prefixes in (5) have the form
\(\forall x_1\ldots \forall x_\varphi \exists x_{\varphi+1}\ldots \exists x_\psi \forall x_{\psi+1}\ldots \forall x_\xi\), then, whatever the favorable \(F\)-set \(\{C,S'\}\) may be, \(S'\) does not contain functional symbols. Hence it is not difficult to obtain that formulas of the form:

\[ \forall x_1\ldots \forall x_\varphi \exists x_{\varphi+1}\ldots \exists x_\varphi \ldots \forall x_{\psi+1}\forall x_\xi \left(\bigvee_{i=1}^{\mu}\bigwedge_{j=1}^{\delta_i} D_{i,j}\right) \quad (\delta_1 \leqslant 2,\ldots,\delta_\mu \leqslant 2) \tag{6} \]

and, consequently, arbitrary disjunctions of formulas of the form (6), constitute a solvable class.

The author expresses his gratitude to the head of the Leningrad seminar on mathematical logic, N. I. Shanin, and also to the participants of the seminar, with whom he had useful conversations.

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

Received
12 V 1964

CITED LITERATURE

¹ A. Church, Introduction to Mathematical Logic, 1, Moscow, 1960.
² J. Herbrand, Recherches sur la théorie de la démonstration, Warsaw, 1930.
³ M. Davis, Proc. Symp. Appl. Math., 15, 15, 1963.
⁴ J. Friedman, J. Assoc. Comput. Machinery, 10, 1, 1 (1963).

* The latter assertion, for that particular case when free favorable \(F\)-sets are obtained from closed \(F\)-sets in one step of applying rule Б, is essentially contained in (⁴).