MATHEMATICS

V. P. OREVKOV

SOME REDUCTION CLASSES AND DECIDABLE CLASSES OF SEQUENTS FOR THE CONSTRUCTIVE PREDICATE CALCULUS

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

1. Below the letters C, K, M, and A will denote, respectively, the classical, constructive, minimal, and positive (absolute)* predicate calculi without function symbols. The term “sequent” will always mean a sequent in whose succedent there is at most one formula. We shall call a sequent positive if it contains no occurrences of the signs \(\supset\) and \(\neg\). We shall call a sequent quasi-positive if it contains no occurrences of the sign \(\supset\) and of formulas of the forms:

\[ \neg \forall \alpha \mathfrak A,\quad \neg \exists \alpha \mathfrak A,\quad \neg(\mathfrak A \& \mathfrak B),\quad \neg(\mathfrak A \vee \mathfrak B),\quad \neg(\mathfrak A \supset \mathfrak B), \]

where \(\mathfrak A\) and \(\mathfrak B\) are formulas, and \(\alpha\) is an individual variable. A quasi-positive (positive) sequent will be called a quasi-absolute (absolute) sequent if it contains no positive occurrences (see (2)) of the quantifier \(\forall\).

Theorem 1. Every absolute sequent derivable in C is also derivable in A (and, consequently, is derivable in M and K).

This theorem follows from the following lemma.

Lemma (*). Every sequent containing no positive occurrences of the signs \(\neg\), \(\supset\), and the quantifier \(\forall\) is derivable in K if and only if it is derivable in C.

Theorem 2. The class of absolute sequents of the form

\[ QN \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 (see (3), § 39), and \(N\) is a disjunction of conjunctions of elementary formulas containing no predicate variables distinct from \(P_1\) and \(P_2\), is a reduction class for C, K, M, and A.

Let us first prove that the mentioned class of sequents is a reduction class for C. Let \(\mathfrak A\) be an arbitrary formula of the predicate calculus. One can construct a formula of the form \(\neg QN\), equivalent to it in C, where \(Q\) is a prefix and \(N\) is a disjunction of simple conjunctions containing only one predicate variable. Denote this predicate variable by \(P_1\), and its arity by \(n\). Introduce a new \(n\)-place predicate variable \(P_2\) and construct the sequent

\[ QN' \to \exists x_1 \ldots x_n\bigl(P_1(x_1,\ldots,x_n)\ \&\ P_2(x_1,\ldots,x_n)\bigr), \tag{2} \]

where the formula \(N'\) is obtained from the formula \(N\) by replacing each occurrence of a formula of the form \(\neg P_1(a_1,\ldots,a_n)\) by the formula \(P_2(a_1,\ldots,a_n)\). It is not hard to prove that the sequent (2) is derivable in C if and only if the formula \(\mathfrak A\) is derivable in the same calculus.

To complete the proof of Theorem 2 it remains only to note that the problem of derivability in K (respectively, in M and in A) can be reduced to the problem of derivability in C, and to refer to Theorem 1.

* The positive (absolute) predicate calculus is obtained from K by removing from the language the sign \(\neg\), and from the list of axioms and rules of inference those in which this sign is used. Sequent variants of M and A of Gentzen type are given in (1).

Remark. It can be proved that a formula \(\mathfrak A\) is refutable on a finite model if and only if the sequent of the form (1), associated with the formula \(\mathfrak A\) by the method indicated above, is also refutable on a finite model. Hence, using the results of \((^4)\), we obtain the following assertion:

The class of absolute sequents of the form (1) derivable in \(\mathbf A\) \(*\) is not effectively separable from the class of absolute sequents of the form (1) refutable on finite models.

2. A bound occurrence of a variable \(a\) in a formula \(\mathfrak A\) will be called a negative occurrence if it lies in the scope of a quantifier complex \(\forall a\) occurring negatively in \(\mathfrak A\), or in the scope of a quantifier complex \(\exists a\) occurring positively in \(\mathfrak A\). In the opposite case, a bound occurrence of a variable in \(\mathfrak A\) will be called positive. An occurrence of an elementary formula \(P(a_1,\ldots,a_n)\) in a formula \(\mathfrak A\) will be called simple if all bound occurrences of the variables \(a_1,\ldots,a_n\) in \(\mathfrak A\) that arise from the occurrence under consideration of the formula \(P(a_1,\ldots,a_n)\) are positive, or if all these occurrences are negative. A formula \(\mathfrak A\) of the predicate calculus will be called a simple formula if all occurrences of elementary formulas in \(\mathfrak A\) are simple occurrences. In particular, any formula containing only unary predicate variables will be simple.

Theorem 3. For the class of simple formulas the derivability problem in \(\mathbf C\) is algorithmically decidable.

This theorem can be proved by moving the quantifiers inside the formula by the method indicated in \((^3)\), p. 204, and using Assertion II § 46 of the same work.

Theorem 4. The derivability problem, both in \(\mathbf K\) and in \(\mathbf M\), is algorithmically decidable for the following classes of sequents:

a) for the class of simple quasi-absolute sequents;

b) for the class of simple quasi-positive sequents containing no positive occurrences of the sign \(\vee\);

c) for the class of simple quasi-positive sequents in whose succedent the sign \(\neg\) does not occur, and there occurs only one unary predicate variable (and no other predicate variables occur);

d) for the class of simple positive sequents in whose succedent only unary predicate variables occur in the scope of the quantifier \(\forall\), and the sign \(\vee\) does not occur;

e) for the class of those quasi-absolute sequents containing no more than binary predicate variables and which, by the method described at the end of § 35 of the book \((^5)\), can be brought to the form

\[ \forall x_1 \ldots x_n \exists y_1 \ldots y_k \forall z_1 \ldots z_m N, \]

where \(0 \leq k \leq 2\); \(N\) is a quantifier-free formula.

3. To prove this theorem we shall construct algorithms \(\varphi\) and \(\varphi'\) satisfying the following conditions:

1) the algorithms \(\varphi\) and \(\varphi'\) transform any quasi-absolute sequent into a sequent containing no occurrences of the sign \(\neg\), nor positive occurrences of the sign \(\supset\) and of the quantifier \(\exists\);

2) a quasi-absolute sequent \(S\) is derivable in \(\mathbf K\) if and only if the sequent \(\varphi(S)\) is derivable in the same calculus;

3) a quasi-absolute sequent \(S\) is derivable in \(\mathbf M\) if and only if the sequent \(\varphi'(S)\) is derivable in the same calculus.

\(*\) According to Theorem 1, this class coincides with the following classes of absolute sequents of the form (1): 1) with the class of sequents derivable in \(\mathbf C\); 2) with the class of sequents derivable in \(\mathbf K\); 3) with the class of sequents derivable in \(\mathbf A\).

These algorithms can be constructed by fixing a definite order for carrying out the transformations described below. Let us first introduce some notation.

Let \(S\) be a quasi-absolute sequent and let \(P_1,\ldots,P_k\) be the list of all pairwise distinct predicate variables occurring in \(S\). Introduce another \(2k\) distinct predicate variables \(P'_1,\ldots,P'_k, P''_1,\ldots,P''_k\), different from \(P_1,\ldots,P_k\) and such that the arities of the predicate variables \(P_i\), \(P'_i\), and \(P''_i\) coincide \((1\leq i\leq k)\). Denote by \(\mathfrak A_1\) the formula

\[ \bigvee_{j=1}^{k}\exists y_1\ldots y_{n_j} \bigl(P'_j(y_1,\ldots,y_{n_j})\ \&\ P''_j(y_1,\ldots,y_{n_j})\bigr), \]

and by \(\mathfrak A_2\) the formula

\[ \mathop{\&}_{j=1}^{k}\forall y_1\ldots y_{n_j} \bigl(P_j(y_1,\ldots,y_{n_j}) \supset P''_j(y_1,\ldots,y_{n_j})\bigr), \]

where \(n_j\) is the arity of the predicate variable \(P_j\) \((1\leq j\leq k)\), and \(y_1,\ldots,y_m\) \((m=\max(n_1,\ldots,n_k))\) are pairwise distinct predicate variables.

Using the derivability in \(\mathbf K\) and \(\mathbf M\) of any formula of the form \(\neg\mathfrak A \equiv \neg\neg\neg\mathfrak A\), transform the sequent \(S\) into an equivalent sequent \(S_0\) containing no occurrences of expressions \(\neg\neg\neg\). Adjoin the formula \(\mathfrak A_2\) to the antecedent of \(S_0\) and replace in \(S_0\) all subformulas of the form \(\neg\neg P_i(\alpha_1,\ldots,\alpha_{n_i})\) by the formulas \(P''_i(\alpha_1,\ldots,\alpha_{n_i})\), and then, in the sequent so obtained, replace all subformulas of the form \(\neg P_i(\alpha_1,\ldots,\alpha_{n_i})\) by the formulas \(P'_i(\alpha_1,\ldots,\alpha_{n_i})\). Denote the sequent obtained as a result of these substitutions by \(S_1\). Suppose that the succedent of the sequent \(S_1\) is empty. Then the result of applying the algorithms \(\varphi\) and \(\varphi'\) to the sequent \(S\) is (by definition) the sequent obtained from \(S_1\) by adjoining the formula \(\mathfrak A_1\) to the succedent.

Suppose that the succedent of the sequent \(S_1\) is not empty. Denote the formula standing in the succedent of \(S_1\) by \(\mathfrak B\). Replace, in the succedent of \(S_1\), the formula \(\mathfrak B\) by the formula \((\mathfrak B \vee \mathfrak A_1)\). The sequent thus obtained is (by definition) the result of applying the algorithm \(\varphi\) to the sequent \(S\). Replace, in the succedent of the sequent \(S_1\), all subformulas of the forms \(P'_i(\alpha_1,\ldots,\alpha_{n_i})\) and \(P''_i(\alpha_1,\ldots,\alpha_{n_i})\) \((1\leq i\leq k)\), respectively, by the formulas

\[ P'_i(\alpha_1,\ldots,\alpha_{n_i})\vee\mathfrak A_1,\qquad P''_i(\alpha_1,\ldots,\alpha_{n_i})\vee\mathfrak A_1. \]

The sequent obtained in this way is (by definition) the result of applying the algorithm \(\varphi'\) to the sequent \(S\).

Item a) of Theorem 4 follows from Theorem 3, the lemma () and the above-indicated properties of the algorithms \(\varphi\) and \(\varphi'\). Items b), c), and d) can be reduced to case a) by moving the quantifiers inside the formulas occurring in the sequent. Item e) follows from assertions VI and VII of § 46 of the book \((^3)\), the lemma () and the properties of the algorithms \(\varphi\) and \(\varphi'\).

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

Received
3 I 1965

REFERENCES

\(^1\) J. Dopp, Logiques construites par une methode de deduction naturelle, Paris, 1962.
\(^2\) Wang Hao, IBM J. Res. and Wevel., 4, 1, 2 (1960).
\(^3\) A. Church, Introduction to Mathematical Logic, 1, Moscow, 1960.
\(^4\) B. A. Trakhtenbrot, DAN, 88, No. 6 (1952).
\(^5\) S. K. Kleene, Introduction to Metamathematics, Moscow, 1957.