MATHEMATICS

V. A. MATULIS

TWO VARIANTS OF THE CLASSICAL PREDICATE CALCULUS WITHOUT STRUCTURAL RULES OF INFERENCE

(Presented by Academician P. S. Novikov on May 19, 1962)

§ 1. In this article the following logical symbolism is used. The expressions \(t_1, t_2, \ldots\) are called individual variables. The order in which they are listed here is called alphabetical. Expressions of the form \(P^0_j\), where \(j = 1, 2, \ldots\), are called propositional variables, and expressions of the form \(P^k_l\), where \(k = 1, 2, \ldots\) and \(l = 1, 2, \ldots\), are called predicate variables. Propositional variables and expressions of the form \(P^k_l(z_1, \ldots, z_k)\), where \(k, l \geq 1\) and \(z_1, \ldots, z_k\) are arbitrary individual variables, are called elementary formulas*.

Logical formulas (briefly, formulas) are defined by the following generating rules: 1) every elementary formula is called a formula; 2) if \(\mathfrak A\) and \(\mathfrak B\) are formulas, then the words \((\mathfrak A \supset \mathfrak B)\), \((\mathfrak A \& \mathfrak B)\), \((\mathfrak A \vee \mathfrak B)\), and \(\neg \mathfrak A\) are called formulas; 3) if \(x\) is an individual variable and \(\mathfrak A\) is a formula, then the words \(\forall x\mathfrak A\) and \(\exists x\mathfrak A\) are called formulas.

Occurrences of individual variables in formulas are divided in the usual way into free and bound (see (1)). If \(x\) and \(y\) are individual variables and \(\mathfrak A\) is a formula, then the expression \([\mathfrak A]^x_y\) will denote the formula obtained from \(\mathfrak A\) as a result of substituting the variable \(y\) for all free occurrences of \(x\) in \(\mathfrak A\). Formula strings are defined by the following generating rules: 1) the empty word is called a formula string; 2) if \(\Sigma\) is a formula string and \(\mathfrak A\) is a formula, then the word \(\Sigma\mathfrak A\) is called a formula string. Every expression of the form \(\Gamma \to \Delta\), where \(\Gamma\) and \(\Delta\) are formula strings, is called a sequent. \(\Gamma\) is called the antecedent of the sequent \(\Gamma \to \Delta\), and \(\Delta\) its succedent. The relation of congruence, introduced in § 33 of the book (1) for formulas, is naturally extended to sequents. Let us denote by \(\varphi\) the operation that transforms each sequent \(S\) into the sequent \(\varphi(S)\), obtained from \(S\) by deleting, in all formulas of the sequent \(S\), all occurrences of such quantifier complexes, in whose scope there are no free occurrences of variables coinciding with the proper variables of these quantifier complexes. We shall say of sequents \(S_1\) and \(S_2\) that they are almost congruent if the sequents \(\varphi(S_1)\) and \(\varphi(S_2)\) are congruent. We shall say that a sequent \(S\) is a pure sequent** if, first, no individual variable occurs in \(S\) both free and bound at the same time, and, second, the sequents \(S\) and \(\varphi(S)\) are graphically equal.

Logical calculi whose derivable objects are sequents will be called sequential calculi. Let \(G'\) and \(G''\) be two sequential calculi. We shall say that they are equipollent if two conditions are satisfied: 1) whatever

* In the symbolic language there will occur individual variables of only one sort.

** By quantifier complexes are meant words of the form \(\forall x\) and \(\exists x\), where \(x\) is some individual variable (\(x\) is called the proper variable of the quantifier complexes).

there was a sequent \(S_1\), derivable in \(G'\), one can construct a sequent \(S_2\), derivable in \(G''\), such that \(S_1\) and \(S_2\) are almost congruent; condition 2) is obtained from 1) by permuting \(S_1\) and \(S_2\) with a simultaneous permutation of \(G'\) and \(G''\).

§ 2. G. Gentzen in the work \((^2)\) constructed a sequent variant of the classical predicate calculus, which he called the calculus LK. In view of the difference between our logical symbolism and Gentzen’s logical symbolism, it will be more convenient for us to refer to the calculus \(G_1\), described in § 77 of the book \((^1)\), which differs from LK only in technical details. The calculus \(G_1\) is poorly adapted for a practically suitable algorithmization of the search for a logical derivation. Better adapted for this purpose is the calculus \(G_3\), described in § 80 of the book just mentioned.

Below we construct new sequent variants \(E_0\) and \(E'_0\) of the classical predicate calculus, which have substantial differences from the calculi \(G_1\) and \(G_3\). Owing to their features, these calculi are better adapted to the search for derivations of sequents than \(G_1\) and \(G_3\). In the description below of the calculi \(E_0\) and \(E'_0\) there appears a number of syntactic (metamathematical) signs and expressions, to which the following meaning is assigned: \(\mathfrak{A}\) and \(\mathfrak{B}\) are arbitrary formulas; \(x,y,z,z_1,z_2,\ldots\) are arbitrary individual variables; \(\Gamma', \Gamma'', \Delta', \Delta''\) are arbitrary formula strings.

The calculus \(E_0\) is given by the axiom schema

\[ \Gamma''\mathfrak{A}\Gamma' \to \Delta'\mathfrak{A}\Delta'' \]

and by the following rules of inference:

\[ \begin{array}{ll} 1.\quad \dfrac{\mathfrak{A}\Gamma' \to \Delta'\mathfrak{B}\Delta''} {\Gamma' \to \Delta'(\mathfrak{A}\supset\mathfrak{B})\Delta''} & 2.\quad \dfrac{\Gamma'\Gamma'' \to \Delta'\mathfrak{A};\ \Gamma'\mathfrak{B}\Gamma'' \to \Delta'} {\Gamma'(\mathfrak{A}\supset\mathfrak{B})\Gamma'' \to \Delta'} \\[2.2em] 3.\quad \dfrac{\Gamma' \to \Delta'\mathfrak{A}\Delta'';\ \Gamma' \to \Delta'\mathfrak{B}\Delta''} {\Gamma' \to \Delta'(\mathfrak{A}\&\mathfrak{B})\Delta''} & 4.\quad \dfrac{\Gamma'\mathfrak{A}\mathfrak{B}\Gamma'' \to \Delta'} {\Gamma'(\mathfrak{A}\&\mathfrak{B})\Gamma'' \to \Delta'} \\[2.2em] 5.\quad \dfrac{\Gamma' \to \Delta'\mathfrak{A}\mathfrak{B}\Delta''} {\Gamma' \to \Delta'(\mathfrak{A}\vee\mathfrak{B})\Delta''} & 6.\quad \dfrac{\Gamma'\mathfrak{A}\Gamma'' \to \Delta';\ \Gamma'\mathfrak{B}\Gamma'' \to \Delta'} {\Gamma'(\mathfrak{A}\vee\mathfrak{B})\Gamma'' \to \Delta'} \\[2.2em] 7.\quad \dfrac{\mathfrak{A}\Gamma' \to \Delta'\Delta''} {\Gamma' \to \Delta'\neg\mathfrak{A}\Delta''} & 8.\quad \dfrac{\Gamma'\Gamma'' \to \Delta'\mathfrak{A}} {\Gamma'\neg\mathfrak{A}\Gamma'' \to \Delta'} \\[2.2em] 9.\quad \dfrac{ \begin{gathered} \Gamma' \to \Delta'\mathfrak{A}\Delta''\\ x \text{ and } y \text{ satisfy condition } (*) \end{gathered}} {\Gamma' \to \Delta'\forall x\,[\mathfrak{A}]^y_x\Delta''} & 10.\quad \dfrac{ \begin{gathered} \Gamma'[\mathfrak{A}]^x_z\forall x\mathfrak{A}\Gamma'' \to \Delta'\\ x \text{ and } z \text{ satisfy condition } (**) \end{gathered}} {\Gamma'\forall x\mathfrak{A}\Gamma'' \to \Delta'} \\[3.2em] 11.\quad \dfrac{ \begin{gathered} \Gamma' \to \Delta'[\mathfrak{A}]^x_z\exists x\mathfrak{A}\Delta''\\ x \text{ and } z \text{ satisfy condition } (**) \end{gathered}} {\Gamma' \to \Delta'\exists x\mathfrak{A}\Delta''} & 12.\quad \dfrac{ \begin{gathered} \Gamma'\mathfrak{A}\Gamma'' \to \Delta'\\ x \text{ and } y \text{ satisfy condition } (*) \end{gathered}} {\Gamma'\exists x\,[\mathfrak{A}]^y_x\Gamma'' \to \Delta'} \end{array} \]

Condition \((*):\) \(x\) does not occur in \(\mathfrak{A}\); \(y\) occurs in the distinguished occurrence of \(\mathfrak{A}\), and moreover only freely, and does not occur in the other occurrences of formulas in the premise\(^*\).

Condition \((**):\) the variable \(z\) is free for \(x\) in \(\mathfrak{A}\) (see § 18 of the book \((^1)\)) and either \(z\) is one of the individual variables occurring freely in \(S\), where \(S\) is the sequent obtained from the premise of the rule of inference by deleting the distinguished occurrence of the formula \([\mathfrak{A}]^x_z\), or \(S\) has no free occurrences of individual variables and \(z\) is an arbitrary individual variable not occurring in \(S\).

The calculus \(E'_0\) is obtained from the calculus \(E_0\) by replacing the rules of inference

\[ {}^*\ \text{It follows from condition } (*) \text{ that in the premise of this rule the formula } \mathfrak{A} \text{ occurs only once.} \]

10 and 11, respectively, with the following rules of inference:

\[ 10'.\quad \frac{ \Gamma'[\mathfrak A]^x_{z_1}\ldots[\mathfrak A]^x_{z_n}\,\forall x\mathfrak A\Gamma'' \to \Delta', \quad x,z_1,\ldots,z_n \text{ satisfy condition }(***) }{ \Gamma'\forall x\mathfrak A\Gamma'' \to \Delta' } \]

\[ 11'.\quad \frac{ \Gamma' \to \Delta'[\mathfrak A]^x_{z_1}\ldots[\mathfrak A]^x_{z_n}\exists x\mathfrak A\Delta'', \quad x,z_1,\ldots,z_n \text{ satisfy condition }(***) }{ \Gamma' \to \Delta'\exists x\mathfrak A\Delta'' } \]

Condition \((***)\): a) the variables \(z_1,\ldots,z_n\) are pairwise distinct and each of these variables is free for \(x\) in \(\mathfrak A\); b) either the list \(z_1,\ldots,z_n\) coincides with the complete list of object variables occurring freely in the sequent \(S\) obtained from the premise by deleting the indicated occurrences of the formulas \([\mathfrak A]^x_{z_1},\ldots,[\mathfrak A]^x_{z_n}\), or there are no free occurrences of object variables in \(S\), \(n=1\), and \(z_1\) does not occur in \(S\).

§ 3. Theorem 1. The calculi \(\mathbf E_0\) and \(\mathbf G_1\) are equipollent. Moreover, if \(S\) is a pure sequent, then it is derivable in \(\mathbf E_0\) if and only if it is derivable in \(\mathbf G_1\).

The proof consists in indicating a method for transforming any derivation of some sequent in one calculus into a derivation of a sequent almost congruent to it in the other calculus. The transformation of a derivation in the calculus \(\mathbf E_0\) into a derivation of the corresponding sequent in the calculus \(\mathbf G_1\) is carried out without essential difficulties. The transformation of a derivation in the calculus \(\mathbf G_1\) into a derivation of the corresponding sequent in the calculus \(\mathbf E_0\) is carried out in several stages connected with the introduction of auxiliary calculi.

Theorem 2. The calculi \(\mathbf E'_0\) and \(\mathbf G_1\) are equipollent. Moreover, if \(S\) is a pure sequent, then it is derivable in \(\mathbf E'_0\) if and only if it is derivable in \(\mathbf G_1\).

This theorem is proved by establishing the equipollence of the calculi \(\mathbf E'_0\) and \(\mathbf E_0\).

Let us note the following two features of the calculi \(\mathbf E_0\) and \(\mathbf E'_0\): 1) in the calculi \(\mathbf E_0\) and \(\mathbf E'_0\) the structural rules are absent; 2) if some sequent \(S_1\) is obtained from a sequent \(S_2\) (from sequents \(S_2\) and \(S_3\)) as a result of a single application of some rule of inference of the calculus \(\mathbf E_0\), then \(S_1\) is derivable in \(\mathbf E_0\) only when \(S_2\) is derivable in this calculus (respectively, \(S_2\) and \(S_3\) are derivable); the same is true for the calculus \(\mathbf E'_0\).

Remark. J. Herbrand in (³) proved the possibility of transforming any derivation in the classical Hilbert-type predicate calculus into such a derivation in which, when applying quantifier rules, fairly strict restrictions on object variables are satisfied. The restrictions on object variables in the quantifier rules of the calculi \(\mathbf E_0\) and \(\mathbf E'_0\) are analogous to the Herbrand restrictions just mentioned. The calculus \(\mathbf E'_0\) has features similar to the method of semantic tableaux proposed by E. Beth in (⁴).

The author expresses deep gratitude to N. A. Shanin, under whose supervision this work was carried out.

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

Received
12 VI 1962

CITED LITERATURE

¹ S. K. Kleene, Introduction to Metamathematics, Moscow, 1957. ² G. Gentzen, Math. Zs., 39, 176, 405 (1934—1935). ³ J. Herbrand, Recherches sur la théorie de la demonstration, Warsaw, 1930. ⁴ E. W. Beth, Semantic Entailment and Formal Derivability, Amsterdam, 1955.