V. P. OREVKOV

UNDECIDABILITY IN THE CONSTRUCTIVE PREDICATE CALCULUS OF THE CLASS OF FORMULAS OF TYPE $\neg\neg \forall\exists$

(Presented by Academician P. S. Novikov, January 9, 1965)

It is known (see, for example, ($^1$)) that for the class of prenex formulas the derivability problem in the constructive predicate calculus is algorithmically decidable. It is also known (see, for example, ($^{2,3}$)) that for the class of formulas having the form $\neg Q M$, where $Q$ is a given prefix and $M$ is a quantifier-free formula, the derivability problem in the constructive predicate calculus is algorithmically decidable if and only if, for this same class of formulas, the derivability problem in the classical predicate calculus is algorithmically decidable. The aim of the present note is to prove the following assertion.

Let $R$ be a binary predicate variable. Then the following theorem holds.

Theorem 1. The class of formulas of the form

\[ \neg\neg \forall x_1 \ldots x_n \exists y_1 \ldots y_m M, \tag{1} \]

where $M$ is a quantifier-free formula containing the predicate variable $R$ and containing no other predicate variables, and $n$ and $m$ are arbitrary positive integers, is a reduction class both for the constructive and for the minimal predicate calculus.

For the proof we reduce to the problem of derivability of formulas of the form (1) in the minimal predicate calculus the problem of compatibility of systems of pairs of words (see ($^4$)). Let $S$ be a system of pairs of words

\[ P_1\alpha Q_1\beta P_2\alpha Q_2\beta \ldots \beta P_k\alpha Q_k, \]

where $P_1, Q_1, \ldots, P_k, Q_k$ are words in the alphabet $\{\xi_1,\ldots,\xi_p\}$ and $\alpha,\beta$ are separator letters not belonging to this alphabet. We introduce the following notation:

\[ A_0 \leftrightarrow \neg (N(x_1)\,\&\,R_0(x_1,x_1)), \]

\[ A_i \leftrightarrow N(y_1)\,\&\,\neg (R_{p+i}(y_1,x_{n_i})\,\&\,N(x_{n_i})\,\& \]

\[ \&\,R_{j_1}(y_1,x_1)\,\&\,R_{j_2}(x_1,x_2)\,\&\,\ldots\,\&\,R_{j_{n_i}}(x_{n_i-1},x_{n_i}})), \]

\[ B_i \leftrightarrow R_0(y_1,y_2)\,\&\,R_{p+i}(y_2,y_3)\,\&\,(R_{l_{m_i}}(y_{m_i+2},y_3)\vee \neg R_0(y_{m_i+3},y_3))\,\& \]

\[ \&\,R_{l_1}(y_1,y_4)\,\&\,R_{l_2}(y_4,y_5)\,\&\,\ldots\,\&\,R_{l_{m_i}}(y_{m_i+2},y_{m_i+3}), \]

\[ C \leftrightarrow \left(A_0 \vee \bigvee_{r=1}^{k} A_r \vee \bigvee_{r=1}^{k} B_r\right), \]

\[ A \leftrightarrow \neg\neg \forall x_1 \ldots x_{n_0}\exists y_1 \ldots y_{m_0+3} C, \]

where

\[ 1 \leqslant i \leqslant k,\quad P_i = \xi_{j_1}\ldots \xi_{j_{n_i}},\quad Q_i = \xi_{l_1}\ldots \xi_{l_{m_i}}, \]

\[ n_0=\max(n_1,\ldots,n_k),\quad m_0=\max(m_1,\ldots,m_k), \]

$N$ is a fixed unary predicate variable, and $R_0,R_1,\ldots,R_p,R_{p+1},\ldots,R_{p+k}$ are pairwise-

various fixed two-place predicate variables and \(x_1,\ldots,x_{n_0}, y_1,\ldots,y_{m_0+3}\) are pairwise distinct individual variables.

Lemma 1. The formula \(A\) is derivable in the minimal predicate calculus if and only if the system \(S\) of pairs of words is compatible.

Denote by \(C'\) the formula obtained by replacing, in the formula \(C\), each occurrence of a formula of the form \(N(t)\) by the formula

\[ \exists t_1t_2\bigl(R(t_1,t_2)\& R(t_2,t_1)R\&(t_1,t)\& R(t_2,t)\bigr) \]

and by replacing each occurrence of a formula of the form \(R_i(t,t')\) \((0\le i\le p+k)\) by the formula

\[ \exists t_1\ldots t_{i+4}\bigl(R(t_1,t)\& R(t_2,t)R\&(t_2,t')\& R(t_3,t')\& \]

\[ \& R(t_{i+4},t_1)\& \mathop{\&}_{j=1}^{i+3} R(t_j,t_{j+1})\bigr). \]

By the method described at the end of § 35 of the book \((^5)\), from the formula \(C'\) one can construct a formula of the form

\[ \forall t_1\ldots t_j\exists u_1\ldots u_l D, \]

where \(D\) is a quantifier-free formula equivalent in the classical predicate calculus* to the formula \(C'\). Denote by \(A'\) the formula

\[ \neg\neg\forall t_1\ldots t_jx_1\ldots x_{n_0}\exists u_1\ldots u_ly_1\ldots y_{m_0+3}D. \]

Lemma 2. The formula \(A'\) is derivable in the minimal predicate calculus if and only if the formula \(A\) is derivable in the same calculus.

Lemma 3. A formula containing no negative occurrences (see \((^6)\)) of disjunction and positive occurrences of implication is derivable in the minimal predicate calculus if and only if it is derivable in the constructive predicate calculus.

Theorem 1 follows from Lemmas 1–3 and from the fact that to the compatibility problem for systems of pairs of words in a fixed (at least two-letter) alphabet there reduces both the derivability problem in the constructive predicate calculus and the derivability problem in the minimal predicate calculus.

Let \(N'\) be a one-place predicate variable. Then the following theorem holds.

Theorem 2. The class of formulas of the form (1), where \(M\) is a quantifier-free formula containing the predicate variable \(N'\) and containing no other predicate variables, is a reduction class for the minimal predicate calculus.

Denote by \(C''\) the formula obtained from the formula \(C'\) by replacing each occurrence of a formula of the form \(R(u,w)\) by the formula

\[ \exists u_1u_2\bigl((N'(w)\supset N'(u))\supset (N'(u_1)\vee N'(u_2))\bigr). \]

By the method described at the end of § 35 of the book \((^5)\), from the formula \(C''\) one can construct a formula of the form, equivalent to it in the classical predicate calculus,

\[ \forall u_1\ldots u_s\exists w_1\ldots w_rD', \]

where \(D'\) is a quantifier-free formula. Denote by \(A''\) the formula

\[ \neg\neg\forall u_1\ldots u_sx_1\ldots x_{n_0}\exists w_1\ldots w_ry_1\ldots y_{m_0+3}D'. \]

Theorem 2 follows from the following lemma:

\[ \text{* The formula obtained will not, generally speaking, be equivalent in the constructive predicate calculus to the formula } C'. \]

Lemma 4. The formula \(A''\) is derivable in the minimal predicate calculus if and only if the formula \(A\) is derivable in this same calculus.

Remark 1. The following classes of formulas are reduction classes both for the constructive and for the minimal predicate calculi:

a) the class of formulas of the form

\[ \neg\neg \forall x_1 \ldots x_{10}\exists y_1 \ldots y_n M \]

and the class of formulas of the form

\[ \neg\neg \forall x_1 \ldots x_n \exists y_1 \ldots y_{13}M, \]

where \(M\) is a quantifier-free formula containing one unary and 34 binary predicate variables and containing no other predicate variables;

b) the class of formulas of the form

\[ \neg\neg \forall x_1 \ldots x_{73}\exists y_1 \ldots y_n M' \]

and the class of formulas of the form

\[ \neg\neg \forall x_1 \ldots x_n \exists y_1 \ldots y_{89}M', \]

where \(M'\) is a quantifier-free formula containing only one binary predicate variable and containing no other predicate variables.

Remark 2. The following classes of formulas are reduction classes for the minimal predicate calculus:

a) the class of formulas of the form

\[ \neg\neg \forall x_1 \ldots x_{97}\exists y_1 \ldots y_n M''; \]

b) the class of formulas of the form

\[ \neg\neg \forall x_1 \ldots x_n \exists y_1 \ldots y_{113}M'', \]

where \(M''\) is a quantifier-free formula containing only one binary predicate variable and containing no other predicate variables.

To prove these assertions it suffices to apply the above reductions to the enumerable set of systems of pairs of words obtained from the calculus \(\mathfrak{S}_2\) of paper \((^7)\) by the method described in § 9 of Chapter VI of the monograph \((^4)\).

Remark 3. It can be proved that the derivability problem is algorithmically decidable, both in the constructive and in the minimal predicate calculi, for the following classes of formulas:

a) for the class of closed formulas of the form

\[ \neg\neg \forall x_1 \ldots x_n M; \]

b) for the class of formulas of the form

\[ \neg\neg \exists x_1 \ldots x_n M, \]

where \(M\) is a quantifier-free formula*.

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

Received
3 I 1965

References

\(^1\) G. E. Mints, DAN, 147, No. 4 (1962).
\(^2\) G. Kreisel, J. Symbolic Logic, 23, 317 (1958).
\(^3\) G. E. Mints, V. P. Orevkov, DAN, 152, No. 3 (1963).
\(^4\) A. A. Markov, Tr. Matem. inst. im. V. A. Steklova AN SSSR, 42 (1954).
\(^5\) S. K. Kleene, Introduction to Metamathematics, M., 1957.
\(^6\) Wang Hao, IBM J. Res. and Wevel, 4, 1, 2 (1960).
\(^7\) T. S. Tseitin, Tr. Matem. inst. im. V. A. Steklova AN SSSR, 52, 172 (1958).

* Assertion b) is obvious (see \((^3)\)).