UDC 51.01:164

MATHEMATICS

G. E. MINTS

A SKOLEM METHOD FOR THE ELIMINATION OF POSITIVE QUANTIFIERS IN SEQUENTIAL CALCULI

(Presented by Academician P. S. Novikov, October 29, 1965)

1. Sequential variants of the pure predicate calculus and of the predicate calculus with equality and function symbols are considered.

The calculus \(LK\) (\(LJ\)) (see \((^1)\)) differs from the classical (respectively, constructive (intuitionistic)) calculus \(G1\), described in \((^2)\), only in the use of two sorts of individual variables: free and bound. Terms are constructed in the usual way from free variables with the aid of function symbols. The calculus \(LK=\) (\(LJ=\)) is obtained by adding to the language of the calculus \(LK\) (respectively, of the calculus \(LJ\)) the predicate symbol \(=\), and to the list of postulates the axiom scheme \(\to t=t\), where \(t\) is an arbitrary term, and the rules of inference\(*\)

\[ \frac{r=s,\;[\Gamma]^a_r\to[\Delta]^a_r}{r=s,\;[\Gamma]^a_s\to[\Delta]^a_s} \qquad \frac{s=r,\;[\Gamma]^a_r\to[\Delta]^a_r}{s=r,\;[\Gamma]^a_s\to[\Delta]^a_s}, \]

where \(\Gamma,\Delta\) are arbitrary lists of formulas, \(r,s\) are arbitrary terms, and \(a\) is an arbitrary free variable.

It is easy to prove that \(LK=\) (\(LJ=\)) is equisize-equivalent to the known variants of the classical (respectively constructive) predicate calculus with equality, for example to the calculi described in § 73 of \((^2)\).

We shall say that a formula \(A\) is derivable in a sequential calculus if the sequent \(\to A\) is derivable in this calculus. The formula image of the sequent \(A_1,\ldots,A_m\to B_1,\ldots,B_n\) is the formula \((A_1\&\ldots\&A_m \supset B_1\vee\ldots\vee B_n)\) (the conjunction of zero formulas denotes the formula \(p\supset p\), and the disjunction of zero formulas the formula \(\neg(p\subset p)\)). We shall often use the fact that the rule of passage from a sequent to its formula image and the rule of the reverse passage are derivable\(**\) in all the calculi mentioned.

1. Quantifier complexes (briefly, complexes) will mean expressions of the form \(Qx\), where \(Q\) is a quantifier and \(x\) is a bound variable (we shall call it the proper variable of the complex). A complex beginning with the quantifier \(Q\) will be called a \(Q\)-complex. A sequent will be called pure if in it the proper variables of different occurrences of quantifier complexes are distinct. We shall assume that all possible free variables are ordered in some way and that, for every \(k\), all possible \(k\)-place function symbols are ordered. Quasi-formulas will mean expressions of the form \([A]^{a_1\ldots a_n}_{x_1\ldots x_n}\), where \(a_1,\ldots,a_n\) are free variables, \(x_1,\ldots,x_n\) are bound variables, and \(A\) is a formula\(***)\).

\(*\) The expression \([E]^x_t\) denotes the result of substituting \(t\) for all occurrences of \(x\) in the word \(E\).

\(**\) A rule is derivable in a calculus if its conclusion is derivable in this calculus from its premises.

\(***) The distinction between quasi-formulas and formulas is caused by the use of two sorts of individual variables. <!-- source-page: 002 --> A **complex** occurring in a formula \(A\) will be called \(A\)-positive (\(A\)-negative) if, as a result of being moved forward by the usual rules of reduction to prenex form, it passes into a \(\forall\)-complex (respectively, into an \(\exists\)-complex). A bound variable will be called \(A\)-positive (\(A\)-negative) if it occurs in an \(A\)-positive (respectively, in an \(A\)-negative) complex.

The definitions of \(S\)-positive (\(S\)-negative) complexes\(^*\) and variables, where \(S\) is a pure sequent, are obtained from the definitions of the preceding paragraph if the formula image of the sequent \(S\) is denoted by \(A\).

Let \(S\) be an arbitrary pure sequent, and let \(x\) be an arbitrary \(S\)-positive variable. We write the list of all proper variables of \(S\)-negative complexes, in whose scope the single occurrence of the complex \(Qx\) in \(S\) lies, in the form \(y_1,\ldots,y_k\). By \(f\) we denote the first (with respect to the ordering fixed in item 1) \(k\)-place function symbol not occurring in \(S\). By \(\mathfrak{S}(S,x)\) we shall denote the formula
\[ [S^-]^x_{f(y_1,\ldots,y_k)}, \]
where \(S^-\) denotes the result of deleting the complex \(Qx\) from \(S\). The sequent \(\mathfrak{S}(S,x)\) will be called the result of applying the Skolem method of elimination of positive quantifiers (s.m.e.) to the pair \((S,x)\). The expression \(\mathfrak{S}(S,x_1,\ldots,x_k,x_{k+1})\) denotes the same as \(\mathfrak{S}(\mathfrak{S}(S,x_1,\ldots,x_k),x_{k+1})\). The expression \(\mathfrak{S}(A,x_1,\ldots,x_k)\) denotes the result of deleting the arrow from \(\mathfrak{S}(\to A,x_1,\ldots,x_k)\). The proof of the following assertion can be copied from the proof of Theorems 1 and 2 of \((^4)\) (in \((^4)\) only classical calculi are considered, but the ideas of the proofs of the theorems mentioned carry over directly to the constructive and minimal predicate calculi without equality).

Theorem 1. The rule
\[ \frac{\forall y_1\ldots \forall y_k [A]^x_{f(y_1,\ldots,y_k)},\ \Gamma \to \Delta} {\forall y_1\ldots \forall y_k \exists x A,\ \Gamma \to \Delta}, \tag{1} \]
where \(f\) is an arbitrary \(k\)-place function symbol not occurring in \(A,\Gamma\) and \(\Delta\), is admissible\({}^{**}\) in \(LK^{=}\), and also in \(LK, LJ\), in the minimal and positive predicate calculi without equality.

Let us note that the sequent
\[ \forall y \exists x\,(((Gx \& y=a)\supset p)\supset Fy)\to \]
\[ \to \exists z\,((Gz\supset p)\supset(Fa \& Fb)) \tag{2} \]
(denote it by \(S\)) is not derivable in \(LJ^{=}\), whereas \(\mathfrak{S}(S,x)\) is derivable in the positive predicate calculus with equality. It follows from this that the rule (1) is not admissible either in the constructive, or in the minimal, or in the positive predicate calculus with equality.

A generalization of Theorem 1 is Theorem 2 (the author has not found its constructive proof in the literature).

Theorem 2. The rule
\[ \frac{\mathfrak{S}(S,x)}{S}, \tag{3} \]
where \(S\) is an arbitrary pure sequent and \(x\) is an arbitrary \(S\)-positive variable, is admissible in \(LK\) and in \(LK^{=}\).

Obviously, it is sufficient to prove that, for any formula \(A\), from the derivability of \(\mathfrak{S}(A,x)\) there follows the derivability of \(A\) (the general case is obtained from this by passing to formula images).

\(^*\) These definitions are equivalent to the definitions of positive and negative quantifiers given in \((^3)\).

\({}^{**}\) A rule is admissible in a calculus if, from the derivability of its premises in this calculus, the derivability of the conclusion follows.

1) The case where \(A\) begins with \(\neg \forall y_1 \ldots \forall y_k \exists x\) is considered with the help of Theorem 2.

2) The case where \(A\) begins with \(\exists y_1 \ldots \exists y_k \forall x\) is reduced to the preceding one in an obvious way.

3) The case where \(A\) begins with \(\exists y_1 \ldots \exists y_i P \forall x\), where \(P\) is a group of quantifier complexes, is exhausted by induction on the number of \(\forall\)-complexes preceding the complex \(\forall x\). Both in the basis and in the induction step, case 2 is applied. All the remaining cases are reduced to case 3 by moving forward (according to the usual rules) all complexes in whose scope \(Qx\) lies, as well as this complex itself.

We note that the converse of rule (3) is admissible in all calculi considered in the present paper. Moreover, for an arbitrary sequent \(S\), in all these calculi, there is derivable, with the help of the theorem on monotone replacement, an implication from the formula image of \(S\) to the formula image \(\mathfrak{S}(S,x)\).

1. The question of the admissibility of rules of the type of rule (3) was raised by E. Rasiowa in (5) in connection with the question of how the set of formulas derivable in elementary constructive axiomatic theory (i.e. an axiomatic theory based on the constructive predicate calculus) changes as a result of applying the Skolem method of quantifier elimination. Theorem 1 shows that if all axioms of the theory are prenex formulas and the predicate calculus without equality is taken as a basis, then the set of derivable formulas does not change (we are speaking of formulas of the old theory). From what has been said about sequent (2) it follows that the set of formulas derivable in an elementary constructive theory with equality may be enlarged as a result of applying the s.m.e. even in the case where all axioms of the theory are prenex formulas.

In connection with the question of whether the consistency of elementary constructive theories is preserved after the application of the s.m.e., the two theorems given below are useful.

Theorem 3. In \(LJ\) and in \(LJ^{=}\), the rule obtained from (3) by imposing the condition is admissible: the succedent of the premise is empty, and the complex \(Qx\) in \(S\) is governed neither by \(S\)-negative complexes nor by \(S\)-positive \(\forall\)-complexes, and \(Q\) is \(\exists\).

This theorem is proved by induction on the number of \(S\)-positive \(\exists\)-complexes governing the complex \(Qx\). The basis of the induction is justified with the help of V. Glivenko’s theorem.

One can show by examples that none of the restrictions mentioned in Theorem 3 can be removed.

Theorem 4. In \(LJ\) and \(LJ^{=}\), the rule obtained from (3) by imposing the condition is admissible: the succedent of the premise is empty and \(S\) contains no \(S\)-positive \(\forall\)-complexes.

Indeed, if \(S\) satisfies the condition mentioned in the theorem, then, by virtue of Theorem 3 from (6), \(S\) is derivable in \(LJ\) (in \(LJ^{=}\)) if and only if it is derivable in \(LK\) (in \(LK^{=}\)). It remains to apply Theorem 2.

One can show by an example that even the application of the s.m.e. in the form of rule (1) can turn a consistent constructive elementary theory with equality into an inconsistent one.

The expression \((+)\) will denote the condition: every \(S\)-positive \(\forall\)-complex that governs the complex with its own variable \(x\) or coincides with it belongs neither to the scope of the sign \(\neg\) nor to the premise of an implication.

The expression \((\alpha^{\sigma_1}, Q\beta^{\sigma_2})\), where \(\alpha, \beta\) are propositional connectives, \(Q\) is a quantifier, and \(\sigma_1, \sigma_2\) are plus or minus signs, will denote the condition: if an occurrence of a complex with its own variable \(x\) in \(S\) lies in the scope of an occurrence of the connective \(\alpha\) in \(S\) having sign \(\sigma_1\) (see (3)), then no-

some occurrence of the connective \(\beta\) in \(S\), having sign \(\sigma_2\), does not lie in the scope of an \(S\)-negative \(Q\)-complex.

Using the theorems on the permutability of applications of rules in the constructive predicate calculus, proved in (7), one can prove the following assertion.

Theorem 5. In \(LJ\) the rule obtained from (3) by imposing the restriction is admissible: \(S\) and \(x\) satisfy condition \((+)\) and the conditions:
\[ (\neg^{-}, \forall\vee^{-}),\quad (\neg^{-}, \forall\neg^{-}),\quad (\neg^{-}, \exists\neg^{-}),\quad (\neg^{-}, \forall\supset^{+}),\quad (\neg^{-}, \exists\supset^{+}),\quad (\supset^{-}, \forall\vee^{-}), \]
\[ (\supset^{-}, \forall\neg^{+}),\quad (\supset^{-}, \exists\neg^{+}),\quad (\supset^{-}, \forall\supset^{+}),\quad (\supset^{-}, \exists\supset^{+}),\quad (\vee^{+}, \forall\vee^{-}),\quad (\exists^{+}, \forall\vee^{-}). \]

Theorem 5 gives a complete classification of the cases of admissibility of application of rule (3) in \(LJ\) in terms of the conditions \((+)\) and \((\alpha^{\sigma_1}, Q\beta^{\sigma_2})\). It can be shown by examples that none of the restrictions mentioned in this theorem can be dropped.

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

Received
7 X 1965

CITED LITERATURE

\(^{1}\) G. Gentzen, Math. Zs., 39, 176 (1934).
\(^{2}\) C. K. Kleene, Introduction to Mathematics, Moscow, 1957.
\(^{3}\) H. Wang, IBM Res. and Devel., 4, 1, 2 (1960).
\(^{4}\) Maehara, J. Math. Soc. Japan, 7, 324 (1935).
\(^{5}\) H. Rasiowa, Constructivity in Mathematics, Amsterdam, 1959, p. 241.
\(^{6}\) G. E. Mints, V. P. Orevkov, DAN, 152, No. 3 (1963).
\(^{7}\) S. C. Kleene, Mem. Am. Math. Soc., 10, 1 (1952).