MATHEMATICS

G. E. MINTS, E. P. OREVKOV

A GENERALIZATION OF THE THEOREMS OF V. I. GLIVENKO AND G. KREISEL TO A CLASS OF FORMULAS OF THE PREDICATE CALCULUS

(Presented by Academician P. S. Novikov, 5 IV 1963)

V. I. Glivenko in \((^1)\) proved that a formula of the propositional calculus beginning with the sign of negation is derivable in the constructive (in V. I. Glivenko’s terminology—intuitionistic) propositional calculus if and only if it is derivable in the classical propositional calculus. G. Kreisel in \((^2)\) generalized this result to prenex formulas of the predicate calculus. It is known (see \((^3)\)) that the formula \(\neg \neg \forall x(P(x)\vee \neg P(x))\), where \(P\) is a one-place predicate variable, is derivable in the classical predicate calculus, but is not derivable in the constructive predicate calculus. From this example it follows that in the formulation of Glivenko’s theorem one cannot replace the propositional calculus by the predicate calculus. The aim of the present note is to prove the following assertion.

Theorem 1. If \(\mathfrak A\) is a formula of the predicate calculus containing no negative (see \((^4)\)) occurrences of the universal quantifier, then the formula \(\neg \mathfrak A\) is derivable in the classical predicate calculus if and only if it is derivable in the constructive predicate calculus.

For the proof we consider the sequent calculus, denoted below by \(G_2^{\wedge}\). The notions of formula and sequent for the calculus \(G_2^{\wedge}\) are defined exactly as for the calculus \(G_2\), described in § 78 of the book \((^3)\). The calculus \(G_2^{\wedge}\) is specified by the axiom scheme

\[ C,\ \neg C \to \]

and by the following rules of inference*:

\[ (\supset)\quad \frac{\neg A,\Gamma\to B,\Gamma\to}{(A\supset B),\Gamma\to} \qquad (\neg\supset)\quad \frac{A,\neg B,\Gamma\to}{\neg(A\supset B),\Gamma\to} \]

\[ (\&)\quad \frac{A\Gamma\to \qquad B,\Gamma\to}{(A\&B),\Gamma\to \qquad (A\&B),\Gamma\to} \qquad (\neg\&)\quad \frac{\neg A,\Gamma\to \neg B,\Gamma\to}{\neg(A\&B),\Gamma\to} \]

\[ (\vee)\quad \frac{A,\Gamma\to B,\Gamma\to}{(A\vee B),\Gamma\to} \qquad (\neg\vee)\quad \frac{\neg A,\Gamma\to \qquad \neg B,\Gamma\to}{\neg(A\vee B)\Gamma\to} \]

\[ (\exists)\quad \frac{[A]^x_a,\Gamma\to}{\exists xA,\Gamma\to} \quad \text{and the variable }a\text{ does not occur freely either in }\Gamma\text{ or in the formula }\exists xA \]

\[ (\neg\exists)\quad \frac{\neg[A]^x_t,\Gamma\to}{\neg\exists xA,\Gamma\to} \quad \text{and the term }t\text{ is free for }x\text{ in }A \]

\[ (\forall)\quad \frac{[A]^x_t,\Gamma\to}{\forall xA,\Gamma\to} \quad \text{and the term }t\text{ is free for }x\text{ in }A \]

\[ (\neg\forall)\quad \frac{\neg[A]^x_a,\Gamma\to}{\neg\forall xA,\Gamma\to} \quad \text{and the variable }a\text{ does not occur freely either in }\Gamma\text{ or in the formula }\neg\forall xA \]

\[ (\Pi)\quad \frac{\Delta,A,B,\Gamma\to}{\Delta,B,A,\Gamma\to} \qquad (\neg\neg)\quad \frac{A,\Gamma\to}{\neg\neg A,\Gamma\to} \]

\[ (\У)\quad \frac{\Gamma\to}{A,\Gamma\to} \qquad (C)\quad \frac{A,A,\Gamma\to}{A,\Gamma\to} \]

\[ \text{* The expression }[A]^x_t\text{ denotes the result of substituting the term }t\text{ for all free occurrences of the variable }x\text{ in }A. \]

We shall show that the calculus \(G_2^\Lambda\) is in a certain sense equivalent to the calculus \(G_2\). (Unless otherwise stated, the classical calculus \(G_2\) is meant.) Construct an algorithm \(\varphi\) satisfying the following condition: if \(S\) is the sequent \(\Gamma \to A_1,\ldots,A_n\) \((n \geqslant 0)\), then \(\varphi(S)\) is the sequent \(\neg A_1,\ldots,\neg A_n,\Gamma \to\). If \(\pi\) is an application of some rule of the calculus \(G_2\), then by \(\varphi(\pi)\) we shall denote the result of applying the algorithm \(\varphi\) to the premises (or premise) and to the conclusion of \(\pi\). Below are listed some pairs of rules (the first member of the pair is the notation for a rule of the calculus \(G_2^\Lambda\), the second member of the pair is the notation for a rule of the calculus \(G_2\)). Rules belonging to one pair will be called corresponding to one another.

1) \((\alpha)\) and \((\alpha \to)\), where \(\alpha\) is any of the symbols \(\supset,\ &,\,\vee,\,\forall,\,\exists,\,C,\,\Pi,\,У\).

2) \((\neg\beta)\) and \((\to \beta)\), where \(\beta\) is any of the symbols \(\supset,\ &,\,\vee,\,\forall,\,\exists,\,\neg\).

3) \((\gamma)\) and \((\to \gamma)\), where \(\gamma\) is any of the symbols \(C,\,\Pi,\,У\).

Lemma 1. All rules of the calculus \(G_2^\Lambda\) are admissible \(*\) in the calculus \(G_2\).

Corollary. If a sequent is derivable in the calculus \(G_2^\Lambda\), then it is derivable in the calculus \(G_2\).

Lemma 2. If a sequent \(S\) is an axiom of the calculus \(G_2\), then \(\varphi(S)\) is an axiom of the calculus \(G_2^\Lambda\). If \(\pi\) is an application of a rule of the calculus \(G_2\) distinct from the cut rule, then \(\varphi(\pi)\) is, up to applications of the rule \((\Pi)\), an application of the corresponding rule of the calculus \(G_2^\Lambda\).

Corollary. If a sequent \(S\) is derivable in the calculus \(G_2\), then the sequent \(\varphi(S)\) is derivable in the calculus \(G_2^\Lambda\).

From this and from the corollary of Lemma 1 there follows the following assertion:

Theorem 2. A sequent \(S\) is derivable in the calculus \(G_2\) if and only if the sequent \(\varphi(S)\) is derivable in the calculus \(G_2^\Lambda\).

Lemma 3. All rules of the calculus \(G_2^\Lambda\), with the exception of the rule \((\neg\forall)\), are admissible in the constructive calculus \(G_2\).

Theorem 3. If a sequent is derivable in the calculus \(G_2^\Lambda\) without application of the rule \((\neg\forall)\), then it is derivable in the constructive calculus \(G_2\).

Theorem 1 is obtained from Theorems 2 and 3 in the following way. The sequent \(\to \neg\mathfrak A\) is derivable in the constructive calculus \(G_2\) if and only if in this calculus the sequent \(\mathfrak A \to\) is derivable. Let us also note that if the formula \(\mathfrak A\) contains no negative occurrences of the quantifier \(\forall\), then in no derivation of the sequent \(\mathfrak A \to\) in the calculus \(G_2^\Lambda\) are there applications of the rule \((\neg\forall)\). Now, to prove Theorem 1 it remains only to refer to Theorems 2 and 3.

Theorems analogous to Theorem 1 can be proved for axiomatic theories constructed on the basis of the predicate calculus, provided that the assertions obtained from the formulations of Lemmas 2 and 3 by replacing \(G_2\) by the axiomatic theory under consideration are valid.

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

Received
1 IV 1963

REFERENCES

1. V. Glivenko, Bull. cl. sci. Acad. Roy. Belg., ser. 5, 15, 183 (1929).
2. G. Kreisel, J. Symbolic Logic, 23, 317 (1958).
3. S. K. Kleene, Introduction to Metamathematics, Moscow, 1957.
4. Wang Hao, IBM J. Res. and Wevel, 4, 1, 2 (1960).

* A rule is called admissible in a calculus if from the derivability of its premises in this calculus there follows the derivability of its conclusion.