V. A. MATULIS

ON VARIANTS OF THE CLASSICAL PREDICATE CALCULUS WITH A UNIQUE DERIVATION TREE

(Presented by Academician P. S. Novikov on 4 IX 1962)

This communication uses the terminology, notation, and results of \((^1)\).

1. We shall call a sequent calculus a calculus with a unique derivation tree if the derivation of any sequent derivable in this calculus, regarded as a tree, is unique. Wang Hao in \((^2)\) constructed a variant of the classical propositional calculus with a unique derivation tree. In this communication two variants of the classical predicate calculus with a unique derivation tree are described, denoted below by \(E_1\) and \(E'_1\). Their construction is based on the calculi \(E_0\) and \(E'_0\) described in \((^1)\).

Every word of the form \(x_1x_2 \ldots x_n\), where \(x_1, x_2, \ldots, x_n\) are any pairwise distinct individual variables, will be called a mark. Every word of the form \(\sigma\mathfrak A\), where \(\sigma\) is a mark and \(\mathfrak A\) is a formula, will be called a marked formula; moreover \(\mathfrak A\) will be called the base of the marked formula, and the number of variables that are members of the mark \(\sigma\) will be called the rank of the marked formula \(\sigma\mathfrak A\). Generalized formula strings are defined as follows: a) the empty word is called a generalized formula string; b) if \(\Sigma\) is a generalized formula string and \(\mathfrak C\) is a formula or a marked formula, then the word \(\Sigma\mathfrak C\) is called a generalized formula string. Every expression of the form \(\Gamma \to \Delta\), where \(\Gamma\) and \(\Delta\) are generalized formula strings, will be called a generalized sequent.

2. In the description below of the calculi \(E_1\) and \(E'_1\) 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^{**}, \Gamma_1, \Delta^*, \Delta^{**}, \Delta_1\) are arbitrary generalized formula strings; \(\Gamma_2, \Gamma_3\) are such generalized formula strings whose members may be: a) elementary formulas, b) formulas beginning with the quantifier \(\forall\), and c) such marked formulas whose base begins with the quantifier \(\forall\); \(\Delta_2\) and \(\Delta_3\) are generalized formula strings whose members may be: a) elementary formulas, b) formulas beginning with the quantifier \(\exists\), and c) such marked formulas whose base begins with the quantifier \(\exists\).

The calculus \(E_1\) is specified by the axiom scheme

\[ \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_2 \to \Delta_2\mathfrak B\Delta_1} {\Gamma_2 \to \Delta_2(\mathfrak A \supset \mathfrak B)\Delta_1}. & 2.\quad \dfrac{\Gamma_2\Gamma_1 \to \Delta_1\mathfrak A;\ \Gamma_2\mathfrak B\Gamma_1 \to \Delta_1} {\Gamma_2(\mathfrak A \supset \mathfrak B)\Gamma_1 \to \Delta_1}. \\[2.2em] 3.\quad \dfrac{\Gamma_2 \to \Delta_2\mathfrak A\Delta_1;\ \Gamma_2 \to \Delta_2\mathfrak B\Delta_1} {\Gamma_2 \to \Delta_2(\mathfrak A\&\mathfrak B)\Delta_1}. & 4.\quad \dfrac{\Gamma_2\mathfrak A\mathfrak B\Gamma_1 \to \Delta_1} {\Gamma_2(\mathfrak A\&\mathfrak B)\Gamma_1 \to \Delta_1}. \\[2.2em] 5.\quad \dfrac{\Gamma_2 \to \Delta_2\mathfrak A\mathfrak B\Delta_1} {\Gamma_2 \to \Delta_2(\mathfrak A\vee\mathfrak B)\Delta_1}. & 6.\quad \dfrac{\Gamma_2\mathfrak A\Gamma_1 \to \Delta_1;\ \Gamma_2\mathfrak B\Gamma_1 \to \Delta_1} {\Gamma_2(\mathfrak A\vee\mathfrak B)\Gamma_1 \to \Delta_1}. \\[2.2em] 7.\quad \dfrac{\mathfrak A\Gamma_2 \to \Delta_2\Delta_1} {\Gamma_2 \to \Delta_2\overline{\mathfrak A}\Delta_1}. & 8.\quad \dfrac{\Gamma_2\Gamma_1 \to \Delta_1\mathfrak A} {\Gamma_2\overline{\mathfrak A}\Gamma_1 \to \Delta_1}. \end{array} \]

\[ \frac{ \begin{gathered} 9.\ \Gamma_2 \to \Delta_2 \mathfrak A \Delta_1,\\ x \text{ and } y \text{ satisfy condition I} \end{gathered} }{ \Gamma_2 \to \Delta_2 \forall x[\mathfrak A]^y_x \Delta_1 }. \]

\[ \frac{ \begin{gathered} 10.\ \Gamma_2[\mathfrak A]^x_{z_{n+1}} z_1 \ldots z_n z_{n+1} \forall x \mathfrak A \Gamma_3 \to \Delta_2,\\ x,z_1,\ldots,z_n,z_{n+1} \text{ and } n \text{ satisfy condition II} \end{gathered} }{ \Gamma_2 z_1 \ldots z_n \forall x \mathfrak A \Gamma_3 \to \Delta_2 }. \]

\[ \frac{ \begin{gathered} 11.\ \Gamma_2 \to \Delta_2[\mathfrak A]^x_{z_{n+1}} z_1 \ldots z_n z_{n+1} \exists x \mathfrak A \Delta_3,\\ x,z_1,\ldots,z_n,z_{n+1} \text{ and } n \text{ satisfy condition III} \end{gathered} }{ \Gamma_2 \to \Delta_2 z_1 \ldots z_n \exists x \mathfrak A \Delta_3 }. \]

\[ \frac{ \begin{gathered} 12.\ \Gamma_2 \mathfrak A \Gamma_1 \to \Delta_1,\\ x \text{ and } y \text{ satisfy condition I} \end{gathered} }{ \Gamma_2 \exists x[\mathfrak A]^y_x \Gamma_1 \to \Delta_1 }. \]

Condition I. \(x\) does not occur in \(\mathfrak A\); \(y\) satisfies the following requirements: a) \(y\) is the first, in alphabetical order, object variable among all object variables that occur neither freely nor bound in the sequent obtained from the premise of the substitution rule by replacing the distinguished occurrence of \(\mathfrak A\) by the occurrence \([\mathfrak A]^y_x\); b) \(y\) occurs freely in \(\mathfrak A^*\).

Below, in the formulations of conditions II and II′ (conditions III and III′), the expression \(C_{\mathrm{II}}\) (respectively \(C_{\mathrm{III}}\)) will denote the alphabetically ordered list of all object variables distinct from \(z_1,\ldots,z_n\), free for the variable \(x\) in \(\mathfrak A\), and occurring freely in at least one of the formulas of the generalized formula chain \(\Gamma_2 \forall x \mathfrak A \Gamma_3 \Delta_2\) (respectively \(\Gamma_2 \Delta_2 \exists x \mathfrak A \Delta_3\)).

Condition II (condition III). a) If \(C_{\mathrm{II}}\) (respectively \(C_{\mathrm{III}}\)) is a nonempty list, then \(z_{n+1}\) is the first variable of the list \(C_{\mathrm{II}}\) (respectively \(C_{\mathrm{III}}\)); if \(C_{\mathrm{II}}\) (respectively \(C_{\mathrm{III}}\)) is an empty list, then \(z_{n+1}\) is the first, in alphabetical order, variable not occurring in the formulas of the generalized formula chain \(\Gamma_2 \forall x \mathfrak A \Gamma_3 \Delta_2\) (respectively \(\Gamma_2 \Delta_2 \exists x \mathfrak A \Delta_3\)); b) the rank of every member of the generalized formula chain \(\Gamma_2\) (respectively \(\Gamma_2 \Delta_2\)) is greater than \(n\), and the rank of every member of the generalized formula chain \(\Gamma_3 \Delta_2\) (respectively \(\Delta_3\)) is greater than or equal to \(n\).

The calculus \(E'_1\) is obtained from the calculus \(E_1\) as the result of replacing rules 10 and 11 respectively by the rules

\[ \frac{ \begin{gathered} 10'.\ \Gamma_2[\mathfrak A]^x_{z_{n+1}}\ldots[\mathfrak A]^x_{z_{n+p}} z_1 \ldots z_n z_{n+1}\ldots z_{n+p}\forall x \mathfrak A \Gamma_3 \to \Delta_2,\\ x,z_1,\ldots,z_n,z_{n+1},\ldots,z_{n+p}, n \text{ and } p \text{ satisfy condition II′} \end{gathered} }{ \Gamma_2 z_1 \ldots z_n \forall x \mathfrak A \Gamma_3 \to \Delta_2 }. \]

\[ \frac{ \begin{gathered} 11'.\ \Gamma_2 \to \Delta_2[\mathfrak A]^x_{z_{n+1}}\ldots[\mathfrak A]^x_{z_{n+p}} z_1 \ldots z_n z_{n+1}\ldots z_{n+p}\exists x \mathfrak A \Delta_3,\\ x,z_1,\ldots,z_n,z_{n+1}\ldots z_{n+p}, n \text{ and } p \text{ satisfy condition III′} \end{gathered} }{ \Gamma_2 \to \Delta_2 z_1 \ldots z_n \exists x \mathfrak A \Delta_3 }. \]

Condition II′ (condition III′). a) If \(C_{\mathrm{II}}\) (respectively \(C_{\mathrm{III}}\)) is a nonempty list, then \(z_{n+1},\ldots,z_{n+p}\) coincides with the list \(C_{\mathrm{II}}\) (respectively \(C_{\mathrm{III}}\)); if \(C_{\mathrm{II}}\) (respectively \(C_{\mathrm{III}}\)) is an empty list, then \(p=1\) and \(z_{n+1}\) is the first, in alphabetical order, variable not occurring in the formulas of the generalized formula chain \(\Gamma_2 \forall x \mathfrak A \Gamma_3 \Delta_2\) (respectively \(\Gamma_2 \Delta_2 \exists x \mathfrak A \Delta_3\)); b) the rank of every member of the generalized formula chain \(\Gamma_2\) (respectively

* From condition I it follows that in the premise of the given inference rule the formula \(\mathfrak A\) occurs only once.

respectively \(\Gamma_2\Delta_2\)) is greater than \(n\), and the rank of any member of the generalized chain \(\Gamma_3\Delta_2\) (respectively \(\Delta_3\)) is greater than or equal to \(n\).

The definition of a derivation in the calculus \(\mathrm{E}_1\) (of a derivation in \(\mathrm{E}'_1\)) is analogous to the definition of a derivation for the commonly used sequent variants of predicate calculus, with the additional requirements: a) that the last generalized sequent of the derivation contain no marked formulas among its members, and b) that in each branch of the derivation tree an axiom of the calculus occur exactly once.

Theorem 1. The calculi \(\mathrm{E}_1\) and \(\mathrm{G}_1\) are equipollent. Moreover, if \(S\) is a pure sequent, then it is derivable in \(\mathrm{E}_1\) if and only if it is derivable in \(\mathrm{G}_1\).

Theorem 2. The calculi \(\mathrm{E}'_1\) and \(\mathrm{G}_1\) are equipollent. Moreover, if \(S\) is a pure sequent, then it is derivable in \(\mathrm{E}'_1\) if and only if it is derivable in \(\mathrm{G}_1\).

Theorem 1 (Theorem 2) is proved by establishing the equipollence of the calculi \(\mathrm{E}_1\) and \(\mathrm{E}_0\) (respectively \(\mathrm{E}'_1\) and \(\mathrm{E}'_0\)). The transformation of a derivation in the calculus \(\mathrm{E}_1\) into the corresponding derivation in the calculus \(\mathrm{E}_0\) (respectively, of a derivation in \(\mathrm{E}'_1\) into a derivation in \(\mathrm{E}'_0\)) is carried out directly, by erasing the marks. The transformation of a derivation in the calculus \(\mathrm{E}_0\) into the corresponding derivation in the calculus \(\mathrm{E}_1\) (respectively, of a derivation in \(\mathrm{E}'_0\) into a derivation in \(\mathrm{E}'_1\)) is carried out in several stages connected with the introduction of auxiliary calculi.

1. The calculi \(\mathrm{E}_1\) and \(\mathrm{E}'_1\) possess properties 1) and 2) of the calculi \(\mathrm{E}_0\) and \(\mathrm{E}'_0\) (see (1), Section 3). In addition, \(\mathrm{E}_1\) and \(\mathrm{E}'_1\) possess the following important property: in each of the inference rules of these calculi, the sequents that are the premises of the rule are uniquely constructed from the sequent that is the conclusion of the rule. This last property makes it possible, in an obvious way, to formulate a simple algorithm for searching for a derivation in \(\mathrm{E}_1\) (respectively in \(\mathrm{E}'_1\)) of pure sequents. For any sequent derivable in \(\mathrm{E}_1\) (respectively in \(\mathrm{E}'_1\)), the derivation-search algorithm terminates and yields a derivation of the sequent under consideration in \(\mathrm{E}_1\) (respectively in \(\mathrm{E}'_1\)). If, however, the algorithm is applied to an underivable sequent, it may happen that the process of applying the algorithm terminates and reveals the underivability of the given sequent, but it may also happen that the process of applying the algorithm continues indefinitely. In view of the absence of a decision algorithm for classical predicate calculus, the latter possibility will necessarily be realized for some underivable sequents.

In the calculi \(\mathrm{E}_1\) and \(\mathrm{E}'_1\), a special method of choosing variables in the quantifier rules replaces the mechanism of Skolem functions that underlies some of the methods described in the literature \((^{2–8})\) for searching for an answer to the question of the derivability of formulas in classical predicate calculus.

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

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

Received
24 VIII 1962

CITED LITERATURE

1. V. A. Matulis, DAN, 147, No. 5 (1962).
2. Hao Wang, Intern. Business Mach. J., 4, No. 1, 2 (1960).
3. T. Skolem, Skr. Norske Vidensk.-Akad. Oslo, 1, No. 4, 49 (1929).
4. J. Herbrand, Recherches sur la théorie de la démonstration, Warsaw, 1930.
5. W. V. Quine, J. Symb. Log., 20, No. 2, 141 (1955).
6. Hao Wang, Comm. Assoc. Comput. Mach., 3, 220 (1960).
7. Hao Wang, Bell Syst. Techn. J., 40, No. 1, 1 (1961).
8. P. C. Gilmore, Intern. Business Mach. J., 4, No. 1, 28 (1960).