UDC 51.01:164

MATHEMATICS

S. Yu. MASLOV

AN INVERSE METHOD FOR ESTABLISHING DERIVABILITY FOR NON-PRENEX FORMULAS OF THE PREDICATE CALCULUS

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

1. In \((^{1,2})\) various aspects of the inverse method for establishing the derivability of formulas of the classical predicate calculus are set forth. This method is useful for constructing machine algorithms for the search for a logical derivation; however, the variant of the method described in \((^{1})\) is applicable only to searching for a derivation of disjunctions of prenex formulas whose matrices have conjunctive normal form. In most cases, reducing the formula \(F\) under test to prenex form \(F'\) and then searching for a derivation of the formula \(F'\) leads to a more complicated and cumbersome procedure than a direct search for a derivation for \(F\). It is therefore desirable to have such an extension of the inverse method in which we could search for a derivation that contains no “redundancy” for formulas of arbitrary form. The purpose of the present communication is to give a sketch description of an inverse method for establishing the derivability of arbitrary formulas of the calculus \(C'\)—the classical predicate calculus with functional signs.

We shall use the terminology and results of the papers \((^{1,2})\); in particular, we shall consider only such formulas as are described in §3 of \((^{2})\). In doing so we shall take as initial the syntactic definitions of the basic concepts of the inverse method, and not the definitions formulated in \((^{1})\) in terms of realizations.

2. Let \(F\) be a formula of \(C'\) of the form

\[ P(D_1 \& \ldots \& D_\nu), \tag{1} \]

where \(P\) is a quantifier prefix; \(D_1,\ldots,D_\nu\) are simple disjunctions. For each \(l\)-ary functional sign \(g\) we introduce (analogously to what was done in \((^{1})\) for universal quantifiers\(^*\)) \(2^l\) signs \(g_{j_1,\ldots,j_\nu}\), where \(l \geq \nu \geq 0\) and \(1 \leq j_1 < \ldots < j_\nu \leq l\). The concept of an \(F,h\)-atom includes expressions of the form \(\lambda,\lambda',\lambda'',\ldots\). The newly introduced signs and \(F,h\)-atoms are included, alongside the old ones, in the construction of \(F,h\)-chains and \(F,h\)-links. Under interpretation in terms of \(F\)-lists\(^{{**}}\), the fulfillment, for example, of the relation \((i,k)=g_{j_1,\ldots,j_4}(\lambda,(i_1,k_1),\lambda,(i_2,k_2))\) means that in the \(i\)-th position of the \(k\)-th element of the \(F\)-list there stands a term of the form \(g(T_1,\ldots,T_l)\), where \(T_{j_1}=T_{j_3}\), and the term \(T_{j_2}\) (the term \(T_{j_4}\), respectively) coincides with the term standing in the \(i_1\)-st position of the \(k_1\)-st element of the \(F\)-list (respectively, in the \(i_2\)-nd position of the \(k_2\)-nd element). The meaning of more complicated relations and \(F,h\)-links is defined analogously. The concepts of a correct link, sublink, and extension of a link are now generalized without difficulty. On the basis of the new concepts, the notions of an \(F\)-set and the rules for constructing favorable sets are formulated literally.

Now, applying Skolem’s method of eliminating quantifiers \((^{3})\), one can replace all universal quantifiers by functors and apply the inverse method to formulas containing only existential quantifiers. In this case

\(^*\) In \((^{1})\) the introduction of nullary signs for universal quantifiers was not provided for (the case \(\nu=0\)). The introduction of nullary signs for quantifiers would also lead to certain technical advantages.

\(^{{**}}\) What is meant is that terms, along with numbers, enter into \(F\)-lists.

in the practical construction of machine programs it will apparently be convenient, in one form or another, to simulate positive quantifiers by functions. However, in developing the inverse method it would be inadvisable to refuse to consider positive quantifiers. First, this would complicate the application of the inverse method to the theory of derivability. The inverse method can serve as a convenient apparatus for obtaining decidable classes and reduction classes (see (¹, ², ⁴)), and often classes of formulas that are easily formulated in terms of universal quantifiers, when these quantifiers are eliminated, acquire cumbersome and unnatural formulations. Second, excluding positive quantifiers from consideration would close off for us the possibility of generalizing the inverse method to calculi to which the Skolem method is inapplicable. Third, for a suitable organization of the search for a derivation we would in any case have to take care of a mechanism analogous to the mechanism of deleting the principal formula when positive quantifiers are removed (see (⁵)).

1. We shall say that a formula \(F\) of the calculus \(C'\) belongs to the class \(\mathbf{M}\) if, in every \(F\)-prefix, all quantifiers, with the possible exception of the last, are universal quantifiers.

Theorem 1. The class \(\mathbf{M}\) is decidable with respect to derivability.*

Let \(F \in \mathbf{M}\). To establish the derivability of \(F\), we perform saturation over all elementary formulas and terms whose height (the maximum number of superpositions) does not exceed the greatest one occurring in \(F\). Then, if \(F\) is derivable, we can justify the благоприятность of the empty set using only closed and free sets, i.e., in a finite number of steps one can verify the derivability or nonderivability of \(F\). It is convenient first to bring \(F\) to the form

\[ \forall x_1 \ldots x_m \exists y_1 \ldots y_n T, \tag{2} \]

where \(T\) is a quantifier-free formula. The possibility of such a reduction follows from the lemma below.

We shall say that quantifier complexes are adjacent in \(F\) if they enter into one and the same \(F\)-prefix. We shall say that \(\exists x^0\) and \(\exists x^r\) are linked in \(F\) if there is a chain of complexes \(\exists x^0, \exists x^1, \ldots, \exists x^r\) such that, for each \(i\), \(\exists x^{i-1}\) is adjacent in \(F\) to \(\exists x^i\) \((1 \le i \le r)\). We shall say that a formula \(F\) of the calculus \(C\) (of the calculus \(C'\)) belongs to the class \(\mathbf{L}_0\) (respectively, to the class \(\mathbf{L}\)) if, for any complexes \(\exists x\), \(\exists x'\), and \(\forall y\), from the adjacency of \(\exists x\) with \(\forall y\) and the linkedness of \(\exists x\) with \(\exists x'\) it follows that \(\forall y\) is not in the scope of \(\exists x'\).

Lemma. For any formula \(F\) from \(\mathbf{L}\), one can construct an equivalent formula \(F'\) of the form (2), and every \(F'\)-prefix, up to a renaming of variables, coincides with some \(F\)-prefix.

Theorem 2. The class \(\mathbf{L}_0\) is decidable with respect to derivability.**

1. We shall now describe a modification of the inverse method that will allow us to extend the method to arbitrary formulas from \(C'\). Let \(F\) have the form (1). Number, with the numbers from 1 to \(\delta\), the almost elementary formulas*** occurring in \(F\) (and not the conjunctive terms of the matrix, as before). The definition of an \(F\)-set \(\{C,S\}\) formally does not change, but in the interpretation the members of the list \(C\) are understood as almost elementary formulas; in accordance with this, for example, the notions of a closed set and of a subset with a common end are reinterpreted (in the interpretation, the last member of the \(F\)-list may correspond not to one member of \(C\), but to several last members—almost elementary formulas obtained under one removal of the quantifiers of a prefix).

* From Theorem 1 there follows directly the decidability of the class of formulas of the calculus \(C'\) of the form \(\forall x_1 \ldots x_n \exists y \forall z_1 \ldots z_m T\), where \(T\) is a quantifier-free formula (see (⁴)).

** \(\mathbf{L}_0\) is a simultaneous generalization of the class of \(\forall\exists\)-formulas, of the single-fragment, and of the class of “simple formulas” (see (⁶)) of the calculus \(C\).

*** By almost elementary formulas we shall mean elementary formulas and negations of elementary formulas.

Let us indicate how rule B is modified. Under the former formulation of this rule, a favorable set \(H\) was obtained as the result of the “merging” of the sets obtained after discarding the last members of the sets \(H_1,\ldots,H_\delta\).* Under the new conditions, the set \(H\) is likewise obtained by merging sets obtained after discarding the last members from certain sets \(H_1,\ldots,H_f\), but now there may be more than one of these last members for each of \(H_1,\ldots,H_f\). For the old rule B the discarded members constituted a complete list of the numbers from 1 to \(\delta\); now the same condition is formulated differently: for each \(D_i\) \((1 \le i \le \gamma)\) there is a set \(H_j\) \((1 \le j \le f)\), all of whose discarded members belong to the set of numbers of the almost elementary formulas of the disjunction \(D_i\) (condition \((*)\)).

Remark 1. Often, different favorable sets can be combined into a single scheme of sets. Before using a scheme of sets for rule B, one must carry out its specification, i.e., indicate which of the sets falling under the given scheme is to be used. More precisely, what is needed is only the specification of the last—discarded—members, while the non-discarded members may remain written in the form of a scheme of sets. Apparently, in the practical construction of machine algorithms it is advisable to seek a justification of the favorability of the empty set precisely by means of schemes of sets with specification of the last members at each step of the application of rule B.

1. The problem of constructing a machine algorithm for the search for a derivation is a topical one; such an algorithm would give a derivation for derivable formulas and the answer “the formula is underivable” for as broad as possible classes of underivable formulas. The literature describes either algorithms for the search for a derivation which are in no way connected with the theory of decidable classes, or algorithms adapted not to the whole predicate calculus but to one or another decidable class, or else sufficiently general methods for proving the decidability of classes which consider the question in a purely theoretical plane and do not lead to practical algorithms. The inverse method differs favorably from those mentioned. A certain gap between the theoretical and practical aspects of the inverse method (connected with the use of saturation) can easily be overcome with the help of the modification of the method from item 4.

The essential point in this modification is a certain complication of rule B: condition \((*)\) is replaced by the following: for each \(D_i\) \((1 \le i \le \gamma)\) there are sets \(H_{j_1},\ldots,H_{j_t}\) \((1 \le j_1 < \cdots < j_t \le f)\) such that \(D_i\) follows from the conjunction of the discarded members of these sets (i.e., the formula

\[ \left(\mathop{\&}_{k=1}^{t}(E_{k,1}\vee \cdots \vee E_{k,l_k})\right)\supset D_i, \]

where \(E_{k,1},\ldots,E_{k,l_k}\) are almost elementary formulas whose numbers are discarded from the set \(H_{j_k}\), \(1 \le k \le t\)) is tautological. In practice, only very special cases of such a complicated rule B will have to be applied, and therefore no difficulties with checking this condition arise. On the basis of this modification, an algorithm for the search for a derivation can be programmed which is at the same time a decision algorithm for broad classes of formulas.

1. We now turn to the exposition of the inverse method for arbitrary formulas. First of all, let us note that reducing the matrix to conjunctive normal form, used in the exposition of item 4, is useful only for simplifying the formulation of condition \((*)\). Not the slightest difficulties arise in constructing favorable sets in the case when the matrix is arbitrary.

A subformula \(H\) of a formula \(F\) will be called an \(F\)-zone if: 1) \(H\) coincides with \(F\) or occurs in \(F\) as a conjunctive member; 2) after removing from \(H\) all quanti—

* Moreover, a “merging” of such a kind that all connections arising between the elements of the sets \(H_1,\ldots,H_\delta\) are compatible.

universal quantifiers not lying in the scope of existential quantifiers, we obtain a formula of the form \(M_1 \vee \exists x M_2 \vee M_3\) (here the disjunction may be expressed, while the quantifier is unexpressed). The principal difficulty in applying the inverse method to non-prenex formulas is connected with the following: in searching for a derivation of a prenex formula, its matrix is duplicated as a whole (with different substitutions for the variables), whereas for non-prenex formulas separately taken pieces of the formula may be duplicated without bound. In this connection, to search for a derivation of a formula \(F\) by means of the inverse method one should introduce one’s own rule Б for each zone*. Moreover, if a set \(\{C, S\}\) is obtained by rule Б for some zone, then the number of this zone is written as the last member of the list \(C\). When such a set is used for rule Б of its own zone, together with the last member—the zone number—the preceding members are discarded (and the same zone number appears in the new set). When such a set is used for rule Б of a broader zone, only this last member is discarded from it. A set is called unconditional if the zone of this set is the formula \(F\) itself (and conditional in the opposite case). Unconditional sets are defined only when the formula \(F\) itself is an \(F\)-zone. In the opposite case, the external connectives of the formula \(F\) are conjunctions and universal quantifiers; therefore the question of the derivability of \(F\) is trivially reduced to the question of the derivability of a finite number of formulas, each of which is its own zone. For such formulas the following holds.

Theorem 3. The formula \(F\) is derivable if and only if the unconditional empty \(F\)-set is favorable.

Remark 2. For favorable sets in the sense of clauses 2, 4, and 5, and also for unconditional favorable sets in the sense of clause 6, the same properties hold as for favorable sets from (1) (the properties of free and decomposable sets, the properties of subsets, the properties of permutations and “gluings” of favorable sets, etc.). The corresponding analogues of these properties also hold for conditional favorable sets.

Remark 3. The considerations of Remark 1 remain valid for clauses 5 and 6.

The author expresses deep gratitude to the members of the mathematical logic group of the Leningrad Branch of the V. A. Steklov Mathematical Institute of the Academy of Sciences of the USSR for useful discussions.

REFERENCES

1. S. Yu. Maslov, DAN, 159, No. 1 (1964).
2. S. Yu. Maslov, DAN, 171, No. 6 (1966).
3. J. Herbrand, Recherches sur la théorie de la démonstration. Warsaw, 1930.
4. V. P. Orevkov, II Symposium on Cybernetics (abstracts), 1965, p. 176.
5. V. A. Matulis, DAN, 147, No. 5 (1962).
6. V. P. Orevkov, DAN, 163, No. 1 (1965).

* If the external disjunction of a zone is not expressed, then rule Б for this zone must be defined taking account of clause 5 of (1).