R. A. PLIUSHKEVICHUS

ON ONE VARIANT OF CONSTRUCTIVE PREDICATE CALCULUS WITHOUT STRUCTURAL RULES OF INFERENCE

(Presented by Academician P. S. Novikov on 22 X 1964)

Let us list the principal syntactic signs and expressions used below, with an explanation of their meaning: \(\mathfrak A, \mathfrak B\) are arbitrary logical formulas (abbreviated: formulas); \(\mathfrak C\) is either an elementary formula, or a formula beginning with the sign \(\neg\), or a formula \(\forall x \neg \mathfrak A\); \(\mathfrak D\) is an arbitrary non-elementary formula not beginning with the sign \(\neg\) and not being a formula \(\forall x \neg \mathfrak A\); \(\Gamma, \Gamma', \Gamma''\) are arbitrary formula chains; \(\Theta\) is an arbitrary formula or the empty word; \(x, y, z, x_1, y_1, z_1,\ldots\) are arbitrary object variables. We shall also use certain terms and notations from the paper \((^1)^*\), as well as the terminology of the book \((^2)\).

Let \(J_0\) denote the calculus specified by the axiom scheme

\[ \Gamma'\mathfrak A\Gamma'' \to \mathfrak A \]

and by the following rules of inference:

\[ \begin{array}{ll} 1.\quad \dfrac{\Gamma\mathfrak A \to \mathfrak B}{\Gamma \to (\mathfrak A \supset \mathfrak B)} & 2a.\quad \dfrac{\Gamma'\Gamma'' \to \mathfrak C;\ \Gamma'\mathfrak B\Gamma'' \to \Theta} {\Gamma'(\mathfrak C \supset \mathfrak B)\Gamma'' \to \Theta} \\[1.2em] 3.\quad \dfrac{\Gamma \to \mathfrak A;\ \Gamma \to \mathfrak B}{\Gamma \to (\mathfrak A \& \mathfrak B)} & 2b.\quad \dfrac{\Gamma'(\mathfrak D \supset \mathfrak B)\Gamma'' \to \mathfrak D;\ \Gamma'\mathfrak B\Gamma'' \to \Theta} {\Gamma'(\mathfrak D \supset \mathfrak B)\Gamma'' \to \Theta} \\[1.2em] 5a.\quad \dfrac{\Gamma \to \mathfrak A}{\Gamma \to (\mathfrak A \vee \mathfrak B)} & 4.\quad \dfrac{\Gamma'\mathfrak A\mathfrak B\Gamma'' \to \Theta} {\Gamma'(\mathfrak A \& \mathfrak B)\Gamma'' \to \Theta} \\[1.2em] 5b.\quad \dfrac{\Gamma \to \mathfrak B}{\Gamma \to (\mathfrak A \vee \mathfrak B)} & 6.\quad \dfrac{\Gamma'\mathfrak A\Gamma'' \to \Theta;\ \Gamma'\mathfrak B\Gamma'' \to \Theta} {\Gamma'(\mathfrak A \vee \mathfrak B)\Gamma'' \to \Theta} \\[1.2em] 7.\quad \dfrac{\Gamma\mathfrak A \to}{\Gamma \to \neg \mathfrak A} & 8a.\quad \dfrac{\Gamma'\Gamma'' \to \mathfrak C} {\Gamma'\neg \mathfrak C\Gamma'' \to \Theta} \\[1.2em] 9.\quad \Gamma \to \mathfrak A & 8b.\quad \dfrac{\Gamma'\neg \mathfrak D\Gamma'' \to \mathfrak D} {\Gamma'\neg \mathfrak D\Gamma'' \to \Theta} \end{array} \]

\(x\) and \(y\) satisfy

\[ \dfrac{\text{condition }(*)}{\Gamma \to \forall x\,[\mathfrak A]^y_x} \]

\[ \begin{array}{ll} 11.\quad \Gamma \to [\mathfrak A]^x_z & 10.\quad \Gamma'[\mathfrak A]^x_z\,\forall x\mathfrak A\,\Gamma'' \to \Theta \\[0.8em] \quad x\text{ and }z\text{ satisfy} & \quad x\text{ and }z\text{ satisfy} \\[0.4em] \quad \dfrac{\text{condition }(**)}{\Gamma \to \exists x\mathfrak A} & \quad \dfrac{\text{condition }(**)}{\Gamma'\forall x\mathfrak A\Gamma'' \to \Theta} \\[1.4em] & 12.\quad \Gamma'\mathfrak A\Gamma'' \to \Theta \\[0.8em] & \quad x\text{ and }y\text{ satisfy} \\[0.4em] & \quad \dfrac{\text{condition }(*)}{\Gamma'\exists x\,[\mathfrak A]^y_x\Gamma'' \to \Theta} \end{array} \]

\[ {}^*\ \text{As V. A. Matulis has informed me, in the paper }(^1)\text{, in the formulation of the definition of a pure} \]
sequent the following condition was omitted: in the sequent \(S\) there cannot be a quantifier complex in whose scope there is another quantifier complex with the same proper variable as that of the first quantifier complex.

The conditions () and (*) are exactly the same as in \((^1)\).

Theorem 1. The calculus \(J_0\) and the constructive calculus \(G1\) (see \((^2)\), §77) are not equipollent. Moreover, if \(S\) is a pure sequent, then it is derivable in \(J_0\) if and only if it is derivable in the constructive calculus \(G1\).

In constructive logic, the passage from the constructive calculus \(G1\) and the equipollent constructive calculi \(G2\) and \(G3\) (see \((^2)\), §§78 and 80) to the calculus \(J_0\) pursues the same aim as the passage in classical logic from the classical calculi \(G1\), \(G2\), and \(G3\) to the calculus \(E_0\), constructed in \((^1)\): the calculus \(J_0\) is better adapted to the search for a derivation in the constructive predicate calculus than the constructive calculus \(G3\).

The principal differences between the calculus \(J_0\) and the constructive calculus \(G3\) are as follows: 1) in the calculus \(J_0\) there are no structural rules of inference and the notion of an initial sequent is not used; 2) the principal formulas of the inference rules of the calculus \(J_0\) are repeated in the premisses only of those rules for which such duplication of the principal formula is indeed necessary; 3) the restrictions on variables in the quantifier rules of the calculus \(J_0\) are stronger than in the constructive calculus \(G3\).

The necessity of the above-mentioned duplication of the principal formula in the rules 2б, 8б, and 10 is seen as follows. Consider the rules for transforming sequents:

\[ \text{2б}^{*}.\quad \frac{\Gamma'\Gamma'' \to \mathfrak D;\ \Gamma'\mathfrak B\Gamma'' \to \Theta} {\Gamma'(\mathfrak D \supset \mathfrak B)\Gamma'' \to \Theta} \]

\[ \text{8б}^{*}.\quad \frac{\Gamma'\Gamma'' \to \mathfrak D} {\Gamma'\neg\mathfrak D\Gamma'' \to \Theta} \]

\[ \text{10}^{*}.\quad \frac{\Gamma'[\mathfrak A]_{z}^{x}\Gamma'' \to \Theta} {x\ \text{and}\ z\ \text{satisfy}} \]

\[ \frac{\text{the condition }(**)} {\Gamma'\forall x\,\mathfrak A\Gamma'' \to \Theta} \]

Let \(J_0^{*}\) (respectively \(J_0^{**}\), respectively \(J_0^{***}\)) denote the calculus obtained from \(J_0\) by replacing rule 2б by rule \(2б^{*}\) (respectively, rule 8б by rule \(8б^{*}\), rule 10 by rule \(10^{*}\)). The calculi \(J_0^{*}\), \(J_0^{**}\), and \(J_0^{***}\) are not equipollent with the calculus \(J_0\). Indeed, in \(J_0^{*}\) the sequent

\[ (((\mathfrak A \supset \mathfrak B)\vee \mathfrak A)\supset \mathfrak B)\to \mathfrak B, \]

where \(\mathfrak A\) and \(\mathfrak B\) are elementary formulas, is not derivable; in \(J_0^{**}\) the sequent

\[ \to \neg\neg(\mathfrak A \vee \neg\mathfrak A), \]

where \(\mathfrak A\) is an elementary formula, is not derivable; in \(J_0^{***}\) the sequent

\[ \forall x\bigl((\mathfrak A \supset [\mathfrak A]_{z_1}^{x})\supset \mathfrak A\bigr)\to [\mathfrak A]_{z_2}^{x}, \]

where \(\mathfrak A\) is an elementary formula containing a free occurrence of the variable \(x\), and \(z_1\) and \(z_2\) are variables distinct from one another and from \(x\), is not derivable. At the same time, the three indicated sequents are derivable in \(J_0\), and the last sequent is derivable even in \(J_0^{*}\). We note that if to \(J_0^{*}\), \(J_0^{**}\), and \(J_0^{***}\) one adjoins the structural rule of contraction of repetitions, then the calculi thereby obtained turn out to be equipollent with the calculus \(J_0\).

All inference rules of the calculus \(J_0\), except rules 2a, 2б, 5a, 5б, 8a, 8б, and 11, are invertible.*

The realizations of rules 2a, 2б, 8a, and 8б turn out to be invertible in those cases where \(\Theta\) is the empty word. In connection with rules 2a and 2б, we note that if the conclusion of some realization of rule 2a (rule 2б) is derivable, then the right premiss of this realization of rule 2a (respectively, of rule 2б) is also derivable.

\[ \rule{3cm}{0.4pt} \]

* An inference rule is called invertible if, in each of its realizations (i.e. in each figure obtained from the inference rule as the result of substituting concrete formulas, concrete formula strings, and concrete variables for the syntactic signs and expressions symbolizing, respectively, formulas, formula strings, and variables), a sequent standing below the line is derivable if and only if all sequents standing above the line are derivable.

1. For the proof of Theorem 1 an auxiliary calculus \(J_0^+\) is introduced, which is obtained from the calculus \(J_0\) by replacing rules \(2a, 2b, 8a\), and \(8b\), respectively, by the rules

\[ 2a^+.\quad \frac{\Gamma'\Gamma'' \to \mathfrak{C}_1;\ \Gamma'\mathfrak{B}\Gamma'' \to \Theta} {\Gamma'(\mathfrak{C}_1 \supset \mathfrak{B})\Gamma'' \to \Theta} \qquad 8a^+.\quad \frac{\Gamma'\Gamma'' \to \mathfrak{C}_1} {\Gamma'\neg \mathfrak{C}_1\Gamma'' \to \Theta} \]

\[ 2b^+.\quad \frac{\Gamma'(\mathfrak{D}_1 \supset \mathfrak{B})\Gamma'' \to \mathfrak{D}_1;\ \Gamma'\mathfrak{B}\Gamma'' \to \Theta} {\Gamma'(\mathfrak{D}_1 \supset \mathfrak{B})\Gamma'' \to \Theta} \qquad 8b^+.\quad \frac{\Gamma'\neg \mathfrak{D}_1\Gamma'' \to \mathfrak{D}_1} {\Gamma'\neg \mathfrak{D}_1\Gamma'' \to \Theta} \]

Here \(\mathfrak{C}_1\) is an arbitrary formula beginning with the sign \(\neg\), or a formula \(\forall x\neg\mathfrak{A}\), while \(\mathfrak{D}_1\) is an arbitrary formula not beginning with the sign \(\neg\) and not being a formula \(\forall x\neg\mathfrak{A}\).

Theorem 2. a) The calculus \(J_0^+\) and the constructive calculus \(G1\) are equivalent in scope. Moreover, if \(S\) is a pure sequent, then it is derivable in \(J_0\) if and only if it is derivable in the constructive calculus \(G1\). b) The calculus \(J_0^+\) and the calculus \(J_0\) are equivalent in scope.

The proof of part a) is carried out as follows:

1) A simple method is indicated for transforming any derivation tree in the calculus \(J_0^+\) into a derivation tree in the constructive calculus \(G1\) having the same final sequent as the first derivation tree.

2) An auxiliary calculus is introduced, obtained from \(J_0^+\) by adjoining the structural rules \(\to Y_1Y \to\), \(\Pi \to\) (see (2), §77) and Gentzen’s structural rule of contraction of repetitions (see (3)):

\[ \frac{\Gamma\mathfrak{A}\Gamma'\mathfrak{A}\Gamma'' \to \Theta} {\Gamma\mathfrak{A}\Gamma'\Gamma'' \to \Theta} \qquad C'\to . \]

It is proved that, whatever pure sequent \(S\) may be, any derivation of it in the constructive calculus \(G1\) can be transformed into a derivation of the sequent \(S\) in the calculus thus obtained.

3) It is proved that every pure* derivation in the indicated extension of the calculus \(J_0^+\) can be transformed into a pure derivation in the calculus \(J_0^+\) with the same final sequent as the first derivation. In proving item 3), the greatest difficulty is the proof of the eliminability of applications of the structural rule \(C'\to\). In this proof the following concepts and considerations are used.

We shall say that a formula chain \(\Delta_1\) is similar to a formula chain \(\Delta_2\) if exactly the same formulas occur in \(\Delta_1\) as in \(\Delta_2\).

The relation “the formula chain \(\Delta\) majorizes the formula \(\mathfrak{A}\)” (symbolic notation \(\Delta \succ \mathfrak{A}\)) is defined by the following generating rules: \(\mathfrak{A}\succ \mathfrak{A}\); if \(\Delta \succ \mathfrak{M}\), then \(\Delta \succ \neg\neg\mathfrak{M}\); if \(\Delta \succ \mathfrak{M}\), then \(\Delta \succ \neg\forall x[\neg\mathfrak{M}]_x^y\); if \(\Delta \succ \mathfrak{M}\), then \(\Delta \succ (\mathfrak{M}\supset \mathfrak{N})\); if \(\Delta \succ \neg\mathfrak{M}\), then \(\Delta \succ (\mathfrak{M}\supset \mathfrak{N})\); if \(\Delta_1 \succ \mathfrak{M}\), \(\Delta_2 \succ \mathfrak{N}\), and \(\Delta\) is a formula chain similar to \(\Delta_1\Delta_2\), then \(\Delta \succ (\mathfrak{M}\&\mathfrak{N})\); if \(\Delta \succ \mathfrak{M}\), then \(\Delta \succ (\mathfrak{M}\vee\mathfrak{N})\); if \(\Delta \succ \mathfrak{N}\), then \(\Delta \succ (\mathfrak{M}\vee\mathfrak{N})\); if \(\Delta \succ \mathfrak{M}\), then \(\Delta \succ \exists x[\mathfrak{M}]_x^y\), where \(x\) and \(y\) are variables such that \(y\) is free for \(x\) in \(\mathfrak{M}\).

It is easy to see that the majorization relation is algorithmically decidable.

Lemma 1. a) If \(\Delta \succ \mathfrak{A}\) and \(\Delta'\mathfrak{A}\Delta'' \succ \mathfrak{B}\), then \(\Delta\Delta'\Delta'' \succ \mathfrak{B}\); b) if \(\Delta \succ \mathfrak{A}\), then the sequent \(\Delta \to \mathfrak{A}\) is derivable in the calculus \(J_0^+\).

Lemma 2. If one can construct a pure derivation tree in the calculus \(J_0^+\) for the sequent \(\Gamma'\mathfrak{A}\Gamma'' \to \Theta\) (a pure derivation tree in the calculus \(J_0^+\) for the sequent \(\Gamma'\mathfrak{A}\Gamma'' \to \Theta\) without such applications of the rules \(2b^+\) and \(8b^+\) in which \(\mathfrak{D}_1\) is an elementary formula) and \(\Delta\) is a formula chain such that: 1) every member of this formula chain is a member of the formula chain \(\Gamma'\Gamma''\), and 2) \(\Delta \succ \mathfrak{A}\), then one can construct a pure derivation tree in the calculus \(J_0^+\) of the seq—

* A derivation tree is called pure if it has the variable-purity property (see (2), §78).

of the sequent \(\Gamma'\Gamma'' \to \Theta\) (respectively, a pure derivation tree in the calculus \(J_0^+\) of the sequent \(\Gamma'\Gamma'' \to \Theta\) without such applications of the rules \(2\delta^+\) and \(8\delta^+\), in which \(\mathfrak D_1\) is an elementary formula).

Item b) of Theorem 2 is easily proved by means of a method analogous to that used in paper \((^4)\), and by means of Lemma 2.

1. In the actual search for a derivation in the constructive predicate calculus, it is expedient (in order to shorten the search process) to adjoin to the calculus \(J_0\) certain admissible rules of inference, for example the rule

\[ \frac{ \Gamma''\mathfrak A_1\mathfrak A_2\ldots \mathfrak A_{n-1}(\mathfrak A_n \supset \mathfrak B)\Gamma'' \to \mathfrak A_n;\quad \Gamma'\mathfrak B\Gamma'' \to \Theta }{ \Gamma'\bigl((\mathfrak A_1 \supset (\mathfrak A_2 \supset \cdots \supset (\mathfrak A_{n-1}\supset \mathfrak A_n)\cdots))\supset \mathfrak B\bigr)\Gamma'' \to \Theta }, \]

where \(\mathfrak A_1,\ldots,\mathfrak A_{n-1}\) are arbitrary formulas, and \(\mathfrak A_n\) is an arbitrary formula whose principal logical sign is different from the sign \(\supset\).

In order, in searching for a derivation, to postpone as far as possible the examination of variants connected with the irreversible rules of inference of the calculus \(J_0\), it is expedient to adjoin to the calculus \(J_0\) a number of reversible rules based on well-known equivalences derivable in the constructive predicate calculus. The following rules may serve as examples of such admissible rules of inference:

\[ \frac{ \Gamma'(\mathfrak A' \supset (\mathfrak A'' \supset \mathfrak B))\Gamma'' \to \Theta }{ \Gamma'((\mathfrak A' \& \mathfrak A'') \supset \mathfrak B)\Gamma'' \to \Theta } \qquad \frac{ \Gamma'\neg \mathfrak A\Gamma'' \to\ ;\quad \Gamma'\mathfrak B\Gamma'' \to }{ \Gamma'(\mathfrak A \supset \mathfrak B)\Gamma'' \to } \]

\[ \frac{ \Gamma'\neg\neg \mathfrak A\neg \mathfrak B\Gamma'' \to \Theta }{ \Gamma'\neg(\mathfrak A \supset \mathfrak B)\Gamma'' \to \Theta } \qquad \frac{ \Gamma'\forall x\,\neg \mathfrak A\Gamma'' \to \Theta }{ \Gamma'\neg\exists x\,\mathfrak A\Gamma'' \to \Theta } \]

In searching for a derivation it is also expedient, in suitable cases, to use Lemma 2 (for removing certain formulas from the antecedents of sequents).

In conclusion the author expresses his deep gratitude to N. A. Shanin, and also to V. A. Matulis for their attention to the work and valuable advice.

Institute of Physics and Mathematics
Academy of Sciences of the Lithuanian SSR

Received
8 IX 1964

CITED LITERATURE

\(^1\) V. A. Matulis, DAN, 147, No. 5 (1962).
\(^2\) S. C. Kleene, Introduction to Metamathematics, Moscow, 1957.
\(^3\) G. Gentzen, Math. Zs., 39, 176, 405 (1934—1935).
\(^4\) N. N. Vorob’ev, Tr. Matem. inst. im. V. A. Steklova AN SSSR, 52, 193 (1958).