MATHEMATICS

Ya. S. SMETANICH

ON PROPOSITIONAL CALCULI WITH AN ADDITIONAL OPERATION

(Presented by Academician P. S. Novikov on 2 III 1961)

Let \(T\) be a constructive propositional calculus. By adding to the axioms of \(T\) new axioms, each of which is a formula of \(T\), and preserving the same rules of inference, we obtain a propositional calculus, which we shall denote by \(G\). Let us add to the logical operations \(\wedge, \vee, \supset, \neg\) an additional logical operation \(\varphi\) of one variable and extend the definition of a formula accordingly. Let us add to the axioms of the calculus \(G\) new axioms, each of which is a formula in the extended sense, and preserve in the extended calculus the rules of inference of the calculus \(T\). The resulting calculus we shall call a propositional calculus with an additional operation and denote it by \(G^{\varphi}\). A formula \(\mathfrak{x}\) containing no occurrence of the operation \(\varphi\) will be called a formula of pure logic. We define the consistency* and completeness of the calculus \(G^{\varphi}\). The calculus \(G^{\varphi}\) is consistent if every formula of pure logic provable in it is also provable in the calculus \(G\). The inconsistency of the calculus \(G^{\varphi}\) is defined correspondingly. The calculus \(G^{\varphi}\) is complete if adding to its axioms a formula \(\mathfrak{x}\) not provable in it as a new axiom makes the extended calculus inconsistent.

An additional operation \(\varphi\) is called single-valued if among the axioms describing it there is the axiom of single-valuedness

\[ (x \sim y) \supset (\varphi(x) \sim \varphi(y)). \]

All calculi \(G^{\varphi}\) considered in this article contain the axiom of single-valuedness. In § 3 of the work \((^{1})\) the calculus \(H\), which is a formalization of the first matrix of Jaśkowski \(J_1\), is considered, and 15 complete calculi \(H_i^{\varphi}\) \((1 \leq i \leq 15)\) are constructed, each of which describes a single-valued additional operation \(\varphi\) of one variable adjoined to the calculus \(H\). In connection with this the question arises: are the consistent calculi \(H^{\varphi}\) containing the axiom of single-valuedness completely described by the system of calculi \(H_i^{\varphi}\) \((1 \leq i \leq 15)\), or not? A positive answer to this question is given by Theorem 1 of the present article. The question of a complete description of single-valued additional operations of one variable adjoined to the calculus \(T\) remains open. Some progress on it is provided by Theorem 2.

Let us introduce the definition of a model. In § 2 of the work \((^{2})\) the definition is given of a matrix \(\mathfrak{M}\) as a set with a distinguished element \(\beta_{\mathfrak{M}}\) and with binary functions \(\supset_{\mathfrak{M}}, \wedge_{\mathfrak{M}}, \vee_{\mathfrak{M}}\) and a unary function \(\neg_{\mathfrak{M}}\) defined on this set, taking values in the same set. We shall extend this definition here by adding to the functions one more additional func-

* Consistency of calculi is understood here in a sense different from the commonly accepted one.

of one variable \(\varphi_{\mathfrak M}\). We shall abbreviate the full notation for the matrix \(\mathfrak M\)

\[ \mathfrak M=[A_{\mathfrak M},\{\beta_{\mathfrak M}\};\supset_{\mathfrak M},\wedge_{\mathfrak M},\vee_{\mathfrak M},\neg_{\mathfrak M},\varphi_{\mathfrak M}] \]

by means of \([A_{\mathfrak M},\{\beta_{\mathfrak M}\}]\). The independent variables of functions considered in matrices are denoted by \(\alpha_i\) \((i=1,2,\ldots,n,\ldots)\).

Let us establish a one-to-one correspondence between the formulas of the calculus \(G^{\varphi}\) and the functions of some matrix \(\mathfrak M\). To the formula \(\mathfrak X(a_1,\ldots,a_n)\) we put in correspondence the function \(\mathfrak X'(\alpha_1,\ldots,\alpha_n)\), obtained by replacing the variables of the formula \(a_1,\ldots,a_n\) by the independent variables \(\alpha_1,\ldots,\alpha_n\), and the logical operations \(\supset,\wedge,\vee,\neg,\varphi\) by the corresponding functions of the matrix.

A function of the matrix \(\mathfrak M\) will be called identical if it always assumes the distinguished value \(\beta_{\mathfrak M}\).

Definition 1. The matrix \(\mathfrak M\) is a model of the calculus \(G^{\varphi}\) if the function of the matrix \(\mathfrak X'(\alpha_1,\ldots,\alpha_n)\), corresponding to the formula \(\mathfrak X(a_1,\ldots,a_n)\) provable in the calculus \(G^{\varphi}\), is identical in the matrix \(\mathfrak M\).

The matrix \(\mathfrak M\) is an exact model of the calculus \(G^{\varphi}\) if: 1) \(\mathfrak M\) is a model of the calculus \(G^{\varphi}\); 2) to every function \(\mathfrak X'(\alpha_1,\ldots,\alpha_n)\) identical in the matrix \(\mathfrak M\) there corresponds a formula \(\mathfrak X(a_1,\ldots,a_n)\) provable in the calculus \(G^{\varphi}\).

Definition 2. Let \(\mathfrak M=[A_{\mathfrak M},\{\beta_{\mathfrak M}\}]\) be a model of the calculus \(G^{\varphi}\). Let \(A_{\mathfrak M'}\) be such a subset of the set \(A_{\mathfrak M}\) that the functions of the matrix \(\mathfrak M\), defined on the sum of the sets \(A_{\mathfrak M'}+\{\beta_{\mathfrak M}\}\), take their values from this same set. Obviously, then we obtain a matrix \(\mathfrak M'=[A_{\mathfrak M'},\{\beta_{\mathfrak M}\}]\) with the same functions as in the matrix \(\mathfrak M\). The matrix \(\mathfrak M'\) is called a submodel of the model \(\mathfrak M\).

In the usual way one defines an isomorphism of two matrices \(\mathfrak M_1,\mathfrak M_2\) (or models \(\mathfrak M_1,\mathfrak M_2\)). From Definitions 1 and 2 we obtain two lemmas.

Lemma 1. If the matrix \(\mathfrak M\) is a model of the calculus \(G^{\varphi}\), and the matrix \(\mathfrak M'\) is a submodel of the model \(\mathfrak M\), then the matrix \(\mathfrak M'\) is also a model of the calculus \(G^{\varphi}\).

Lemma 2. Let the matrix \(\mathfrak M_1\) be a model of the calculus \(G^{\varphi}_1\), and the matrix \(\mathfrak M_2\) a model of the calculus \(G^{\varphi}_2\). If the matrices \(\mathfrak M_1\) and \(\mathfrak M_2\) are isomorphic, then \(\mathfrak M_1\) is a model of the calculus \(G^{\varphi}_2\), and \(\mathfrak M_2\) is a model of the calculus \(G^{\varphi}_1\).

Let us construct an exact model of an arbitrary calculus \(G^{\varphi}\), which we shall call the natural model. The set of formulas of the calculus \(G^{\varphi}\) is divided into classes of equivalent formulas (formulas \(\mathfrak X_1\) and \(\mathfrak X_2\) are equivalent if in the calculus the formulas \(\mathfrak X_1\supset\mathfrak X_2\), \(\mathfrak X_2\supset\mathfrak X_1\) are provable). Denote the class of formulas equivalent to the formula \(\mathfrak X\) by \(\widetilde{\mathfrak X}\), and the aggregate of the classes of equivalent formulas of the calculus \(G^{\varphi}\) by \(\widetilde G^{\varphi}\). We now define the matrix \(\mathfrak E\). The set of elements of the matrix \(\mathfrak E\) is the class \(\widetilde G^{\varphi}\). The functions \(\boxplus_{\mathfrak E}\)* are defined as follows:

\[ (\widetilde{\mathfrak X}_1\boxplus_{\mathfrak E}\widetilde{\mathfrak X}_2)=(\widetilde{\mathfrak X_1\boxplus\mathfrak X_2}), \]

and the matrix functions \(\neg_{\mathfrak E},\varphi_{\mathfrak E}\) are defined analogously. Obviously, the matrix \(\mathfrak E\) is an exact model of the calculus \(G^{\varphi}\) with distinguished element \(\widetilde 1\)**.

The finite aggregate of formulas

\[ \{\varphi(0),\varphi(1),\varphi(\varphi(0)),\varphi(\varphi(1)),\varphi(a\vee\neg a)\} \]

together with their negations and double negations will be called the basic set. A nonempty subset of the basic set of formulas will be called

* \(\boxplus\) denotes a binary logical operation \(\supset,\wedge,\vee\).

** \(1\) is the notation for the formula \(a\supset a\), and \(0\) for the formula \(a\wedge\neg a\).

by the choice of the case. Let \(\{\mathfrak{X}_1,\ldots,\mathfrak{X}_k\}\) be a finite class of formulas. Add to the axioms of the calculus \(G^\varphi\) the axioms \(\mathfrak{X}_1,\ldots,\mathfrak{X}_k\). The resulting calculus, which is an extension of the calculus \(G^\varphi\), will be denoted by \(G^\varphi[\mathfrak{X}_1,\ldots,\mathfrak{X}_k]\).

Definition 3. A class of case choices \(\{X_i\}\) \((1 \leq i \leq n)\) will be called complete if, whatever consistent calculus \(H^\varphi\) may be given, there is a case choice
\[ X_{i_0}=\{\mathfrak{X}_1,\ldots,\mathfrak{X}_p\}\quad (1\leq i_0\leq n) \]
such that the calculus
\[ H^\varphi[\mathfrak{X}_1,\ldots,\mathfrak{X}_p] \]
is consistent.

Lemma 3. Let \(\mathfrak{X}\) be a formula of the basic set, and let \(H^\varphi\) be an arbitrary consistent calculus. Then one of the two calculi
\[ H^\varphi[\neg\mathfrak{X}],\qquad H^\varphi[\neg\neg\mathfrak{X}] \]
is consistent.

With the aid of Lemma 3 and the uniqueness axiom, a complete class of case choices is constructed,

\[ \{X_i\}\ (1\leq i\leq 15), \tag{1} \]

whose elements are as follows:

\[ \begin{aligned} X_1&=\{\varphi(0),\varphi(1),\varphi(a\vee \neg a)\};& X_2&=\{\varphi(0),\varphi(1),\neg\neg\varphi(a\vee \neg a)\};\\ X_3&=\{\varphi(0),\neg\neg\varphi(1),\varphi(\varphi(1))\};& X_4&=\{\varphi(0),\neg\neg\varphi(1),\varphi(\varphi(1))\};\\ X_5&=\{\neg\varphi(0),\varphi(1),\varphi(a\vee \neg a)\};& X_6&=\{\neg\varphi(0),\varphi(1),\neg\neg\varphi(a\vee \neg a)\};\\ X_7&=\{\neg\varphi(0),\neg\varphi(1),\neg\varphi(a\vee \neg a)\};& X_8&=\{\neg\varphi(0),\neg\neg\varphi(1),\varphi(\varphi(1))\};\\ X_9&=\{\neg\varphi(0),\neg\neg\varphi(1),\neg\neg\varphi(\varphi(1))\};& X_{10}&=\{\neg\neg\varphi(0),\varphi(1),\varphi(\varphi(0))\};\\ X_{11}&=\{\neg\neg\varphi(0),\neg\neg\varphi(1),\varphi(\varphi(0))\};& X_{12}&=\{\neg\neg\varphi(0),\neg\varphi(1),\neg\varphi(\varphi(0))\};\\ X_{13}&=\{\neg\neg\varphi(0),\varphi(1),\neg\neg\varphi(\varphi(0))\};& X_{14}&=\{\neg\neg\varphi(0),\neg\neg\varphi(1),\\ &&&\quad \neg\neg\varphi(\varphi(0)),\neg\neg\varphi(\varphi(1))\};\\ X_{15}&=\{\neg\varphi(0),\neg\varphi(1),\neg\varphi(a\vee \neg a)\}. \end{aligned} \]

The complete class of case choices (1) just constructed makes it possible to prove the following theorem:

Theorem 1. Let \(H^\varphi\) be an arbitrary consistent calculus. There exists a calculus \(H_i^\varphi\) \((1\leq i\leq 15)\) such that all axioms of \(H^\varphi\) are derivable in the calculus \(H_i^\varphi\).

We indicate the scheme of the proof of Theorem 1. Let \(H^\varphi\) be an arbitrary consistent calculus. Among the elements of the complete case choice (1), on the basis of Definition 3, there is a case choice
\[ X_i=\{\mathfrak{X}_1,\ldots,\mathfrak{X}_k\} \]
such that the calculus
\[ H^\varphi[\mathfrak{X}_1,\ldots,\mathfrak{X}_k] \]
is consistent. Let \(\mathfrak{C}\) be its natural model. With the aid of the uniqueness axiom and the axioms \(\mathfrak{X}_1,\ldots,\mathfrak{X}_k\), a submodel \(\mathfrak{C}'\) of the model \(\mathfrak{C}\) is found, containing the three elements \(\{\hat{0},\hat{1},\mathfrak{B}\}\), where \(\mathfrak{B}\) is one of the formulas
\[ \varphi(0),\ \varphi(1),\ \varphi(a\vee \neg a),\ a\vee \neg a. \]
Each of the calculi \(H_i^\varphi\) \((1\leq i\leq 15)\) has an exact model of three elements \(\{\lambda,\mu,\sigma\}\). The model \(\mathfrak{C}'\) turns out to be isomorphic to an exact model of one of the calculi \(H_i^\varphi\). Consequently, on the basis of Lemma 2, the calculus
\[ H^\varphi[\mathfrak{X}_1,\ldots,\mathfrak{X}_k] \]
has as a model the exact model of some calculus \(H_i^\varphi\). By virtue of the completeness of the calculus \(H_i^\varphi\), all axioms of the calculus \(H^\varphi\) are derivable in the calculus \(H_i^\varphi\).

Corollary. If the calculus \(H^\varphi\) is consistent and complete, then there exists a calculus \(H_i^\varphi\) such that the classes of provable formulas of the calculi \(H^\varphi\), \(H_i^\varphi\) coincide.

Theorem 2. Let \(T^\varphi\) be an arbitrary consistent constructive propositional calculus with an additional operation. There will be found—

there is a calculus \(H_i^{\varphi}\) \((1 \leqslant i \leqslant 15)\) such that all axioms of the calculus \(T^{\varphi}\) are derivable in the calculus \(H_i^{\varphi}\).

For the proof of Theorem 2 the notion is used of the consistency of the calculus \(T^{\varphi}\) relative to the calculus \(H\). The calculus \(T^{\varphi}\) is consistent relative to the calculus \(H\) if every formula of pure logic that is derivable in the calculus \(T^{\varphi}\) is also derivable in the calculus \(H\).

The calculus \(T^{\varphi}\) is extended, by means of a certain selection of cases, to the calculus \(T^{\varphi}[\mathfrak{X}_1,\ldots,\mathfrak{X}_q]\), consistent relative to \(H\), and then an argument analogous to that given in Theorem 1 is carried out.

All-Union Scientific Research Institute
of Electrification of Agriculture

Received
28 II 1961

REFERENCES

1. Ya. S. Smetanich, Tr. Mosk. matem. obshch., 9, 357 (1960).
2. B. Yu. Pilchak, Ukr. matem. zhurn., 4, 174 (1952).