Reports of the Academy of Sciences of the USSR

1965, Vol. 163, No. 2

MATHEMATICS

S. Yu. Maslov, G. E. Mints, V. P. Orevkov

UNDECIDABILITY IN CONSTRUCTIVE PREDICATE CALCULUS OF CERTAIN CLASSES OF FORMULAS CONTAINING ONLY UNARY PREDICATE VARIABLES

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

It is known that, in the class of formulas containing only unary predicate variables, the derivability problem is algorithmically decidable in the classical predicate calculus without function symbols. The main purpose of the present communication is to prove, by constructive means, the undecidability of the derivability problem in the constructive, minimal, and positive predicate calculi without function symbols* for the class of formulas containing only one unary predicate variable. In the present communication the terminology and results of paper (1) are used.

1. Let (P) and (P') be arbitrary unary predicate variables, and (R) an arbitrary binary predicate variable. Then Theorems 1–5 hold.

Theorem 1. The class of absolute sequents containing the predicate variable (R), and containing no other predicate variables and no positive occurrences of the sign (\vee), is a decision class for (C, K, M), and (A).

Theorem 2. The class of sequents containing the predicate variable (P), and containing no other predicate variables, no sign (\neg), and no positive occurrences of the quantifier (\forall), is a decision class for (K, M), and (A).

Theorem 3. The class of sequents containing the predicate variable (P), and containing no other predicate variables, no occurrences of the sign (\supset), and no positive occurrences of the sign (\vee) and of the quantifier (\forall), is a decision class for (K) and (M).

Theorem 4. The class of positive sequents containing the predicate variables (P) and (P'), and containing no other predicate variables, is a decision class for (K, M), and (A).

Theorem 5. The class of quasipositive sequents containing the predicate variable (P), and containing no other predicate variables, is a decision class for (K) and (M).

1. We outline the proofs of these theorems. In paper (1) it is shown that the class of absolute sequents of the form

[
Q \mathcal{M} \to \exists x_1 \ldots x_n \bigl(P_1(x_1,\ldots,x_n) \& P_2(x_1,\ldots,x_n)\bigr),
\tag{1}
]

where (Q) is a prefix and (\mathcal{M}) is a disjunction of conjunctions of elementary formulas containing no predicate variables distinct from (P_1) and (P_2), is a decision class for (C, K, M), and (A).

* These calculi will be denoted respectively by (K, M), and (A), and the classical predicate calculus without function symbols by (C).

We shall construct algorithms (\varphi_1,\varphi_2,\varphi_3,\varphi_4), and (\varphi_5) such that, whatever the absolute sequent (S) of the form (1):

1) the algorithm (\varphi_1) transforms (S) into an absolute sequent containing the predicate variable (R) and containing no positive occurrences of the sign (\vee);

2) the algorithm (\varphi_2) transforms (S) into a sequent containing the predicate variable (P) and containing no occurrences of the sign (\neg) and no positive occurrences of the quantifier (\forall);

3) the algorithm (\varphi_3) transforms (S) into a sequent containing the variable (P) and containing no occurrences of (\supset) and no positive occurrences of (\vee) or of the quantifier (\forall);

4) the algorithm (\varphi_4) transforms (S) into a positive sequent containing the predicate variables (P) and (P');

5) the algorithm (\varphi_5) transforms (S) into a quasi-positive sequent containing the predicate variable (P);

6) the sequent (S) is derivable in (\mathbf C) if and only if the sequent (\varphi_1(S)) is derivable in (\mathbf C);

7) whatever (i) may be ((1\leqslant i\leqslant 5)), the sequent (S) is derivable in (\mathbf K) if and only if the sequent (\varphi_i(S)) is derivable in (\mathbf K);

8) whatever (i) may be ((1\leqslant i\leqslant 5)), the sequent (S) is derivable in (\mathbf M) if and only if the sequent (\varphi_i(S)) is derivable in (\mathbf M);

9) whatever (i) may be ((i=1,4)), the sequent (S) is derivable in (\mathbf A) if and only if the sequent (\varphi_i(S)) is derivable in (\mathbf A).

Let (S) be a sequent of the form (1). The result of applying the algorithm (\varphi_1) to the sequent (S) shall be taken (by definition) to be the sequent obtained from (S) by replacing each occurrence of an elementary formula of the form (P_k(y_1,\ldots,y_n)) ((k=1,2)) by the formula

[
\exists \alpha_1\ldots \alpha_{n+k+1}
\left(
\mathop{\&}{i=1}^{\,n+k} R(\alpha_i,\alpha)
\ \&\ R(\alpha_{n+k+1},\alpha_1)
\ \&\ \mathop{\&}{i=1}^{\,n}
\bigl(R(\alpha_i,y_i)\ \&\ R(\alpha,y_i)\bigr)
\right),
\tag{2}
]

where (\alpha_1,\ldots,\alpha_{n+k+1}) are pairwise distinct individual variables.

The result of applying the algorithm (\varphi_2) to the sequent (S) shall be taken (by definition) to be the sequent obtained from (\varphi_1(S)) as a result of replacing each occurrence of a subformula of the form (R(x,y)) by the formula

[
\exists \alpha\beta\,\bigl((P(y)\supset P(x))\supset (P(\alpha)\vee P(\beta))\bigr).
\tag{3}
]

The result of applying the algorithm (\varphi_3) to the sequent (S) shall be taken to be the sequent obtained from (\varphi_1(S)) as a result of replacing each occurrence of an elementary formula of the form (R(x,y)) by the formula

[
\exists \alpha_1\alpha_2\alpha_3\beta_1\beta_2\beta_3
\left(
\mathop{\&}{i=1}^{3}\neg\left(P(\beta_i)\ \&\ \mathop{\&} P(\alpha_j)\right)}^{3
\right)\ \&
]

[
\&\neg\left(P(\alpha_1)\ \&\ P(x)\ \&\ \mathop{\&}_{i=1}^{3} P(\beta_i)\right)
\ \&\ \neg\left(P(\alpha_2)\ \&\ P(\beta_1)\ \&\ P(\beta_2)\ \&\ P(x)\ \&\ P(y)\right).
\tag{4}
]

The result of applying the algorithm (\varphi_4) to (S) shall be taken to be the result of replacing in (\varphi_1(S)) each occurrence of a subformula of the form (R(x,y)) by the formula

[
\exists \alpha_1\alpha_2\alpha_3\beta_1\beta_2\beta_3\ \forall \gamma\, (P'(\gamma)\vee \mathfrak A),
\tag{5}
]

where by (\mathfrak A) is denoted the formula

[
\left(
\mathop{\&}{i=1}^{3}
\left(P(\beta_i)\vee \mathop{\vee} P(\alpha_j)\right)}^{3
\right)
\ \&\ \left(P(\alpha_1)\vee P(x)\vee \mathop{\vee}_{j=1}^{3} P(\beta_j)\right)\ \&
]

[
\&\left(P(\alpha_2)\vee P(\beta_1)\vee P(\beta_2)\vee P(x)\vee P(y)\right).
]

The result of applying the algorithm (\varphi_5) to (S) will be taken to be the result of replacing in (\varphi_1(S)) each occurrence of a subformula of the form (R(x,y)) by the formula

[
\exists \alpha_1 \alpha_2 \alpha_3 \beta_1 \beta_2 \beta_3 \forall \gamma(\neg\neg P(\gamma)\vee \mathfrak A).
\tag{6}
]

Since a sequent (S) is derivable in (\mathbf K) if and only if it is derivable in (\mathbf C), (\mathbf M), and (\mathbf A)*, in order to complete the proof of Theorems 1–5 it remains only to show that from the derivability of the sequent (\varphi_i(S)) ((1\leq i\leq 5)) in (\mathbf K) there follows the derivability of (S) in this calculus. To prove the latter assertion it is enough to note that, for each (i) ((i=1,\ldots,5)), a derivation of the sequent (\varphi_i(S)) in the constructive calculus (G_2) (see ((^2))) can, using the results of ((^3)), be transformed into a derivation of the same sequent in which all formulas in the axioms have the form ((i+1)).

1. If (B) is a sequent, then by ({B}) we shall denote the formula image of the sequent (B). Let (P) be an arbitrary unary predicate variable. Then the following Theorems 6 and 7 hold:

Theorem 6. The class of formulas of the form (({B}\vee \neg{B})), where (B) is a quasi-positive sequent containing the predicate variable (P) and containing no other predicate variables, is a reduction class for (\mathbf K) and (\mathbf M).

Theorem 7. The class of formulas of the form ((\neg\neg{B}\supset {B})), where (B) is a quasi-positive sequent containing the predicate variable (P) and containing no other predicate variables, is a reduction class for (\mathbf K) and (\mathbf M).

Corollary 1. There is no algorithm recognizing the formulas derivable in (\mathbf K) among the formulas derivable in (\mathbf C).

Corollary 2. There is no algorithm recognizing the formulas derivable in (\mathbf K) among the formulas whose double negation is derivable in (\mathbf K).

Theorems 6 and 7 follow from the following lemma.

Lemma. Whatever the sequent (S) of the form (1) may be, the formulas (\neg{\varphi_2(S)}), (\neg{\varphi_3(S)}), (\neg{\varphi_4(S)}), and (\neg{\varphi_5(S)}) are derivable in the constructive predicate calculus.

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

Received
3 I 1965

REFERENCES

(^1) V. P. Orevkov, DAN, 163, No. 1 (1965). (\quad) (^2) S. K. Kleene, Introduction to Metamathematics, Moscow, 1957. (\quad) (^3) S. C. Kleene, Mem. Am. Math. Soc., No. 10, 1 (1952).

* See Theorem 1 of the paper ((^1)).