UDC 517.11

MATHEMATICS

V. A. YANKOV

CONSTRUCTION OF A SEQUENCE OF STRONGLY INDEPENDENT SUPERINTUITIONISTIC PROPOSITIONAL CALCULI

(Presented by Academician P. S. Novikov on 12 X 1967)

By a superintuitionistic logic we shall mean a set of propositional formulas in the language with four connectives \(\&, \supset, \vee, \neg\), containing the intuitionistic axioms and closed under the rules of substitution and modus ponens. A logic is a calculus if it is obtained by adding to the intuitionistic axioms a finite number of additional ones and closing under the rules of inference.

Logics in a sequence \(N_1,\ldots,N_k,\ldots\) will be called strongly independent (see \((^1)\)) if, for every \(i\), \(N_i\) is not contained in the logic generated by all \(N_j\) with \(j \ne i\). The models of the intuitionistic propositional calculus studied in \((^2)\) under the name of pseudo-Boolean algebras will be called Brouwer algebras . A Gödelian Brouwer algebra (see \((^3)\)) will be called (in the finite case) a Brouwer algebra with a unique immediate predecessor of the greatest element* . By a \(\Lambda\)-algebra we shall hereafter mean a finite Gödelian Brouwer algebra \(\alpha\) in which there is a system of three generators \(a_1,a_2,a_3\) and the following relations hold:

\[ \begin{aligned} 1)\quad &\neg(a_1\&a_2)=\neg(a_2\&a_3)=\neg(a_1\&a_3)=(\neg\neg a_3 \supset a_3)=\\ &=(\neg\neg a_2 \supset a_2)=\neg\neg(a_1 \vee a_2 \vee a_3)=V;\\ 2)\quad &\neg a_3 \vee \neg a_2 \vee (\neg\neg a_1 \supset a_1)=\omega . \end{aligned} \]

Here \(V\) is the greatest element of \(\alpha\), and \(\omega\) is its unique immediate predecessor.

In \((^3)\), for every Gödelian Brouwer algebra \(\alpha\) a formula \(X_\alpha\) was introduced with the property that an arbitrary formula \(F\) is refutable on \(\alpha\) (see \((^3)\), bearing in mind that in \(\alpha\) the greatest element \(V\) is singled out) if and only if \(F \vdash X_\alpha\) (Theorem 2 of \((^3)\); the symbol \(\vdash\) denotes derivability of \(X_\alpha\) from \(F\) using the intuitionistic axioms, modus ponens, and substitution). In \((^3)\) the following ordering of Gödelian Brouwer algebras is also introduced (isomorphic algebras being identified): \(\alpha \leqslant \beta\) if and only if \(X_\alpha \vdash X_\beta\). The following two lemmas ensure the possibility of constructing a sequence of strongly independent calculi.

Lemma 1. Two \(\Lambda\)-algebras are either incomparable or isomorphic.

Lemma 2. There exist \(\Lambda\)-algebras with an arbitrarily large number of elements.

As for the second of these lemmas, the desired \(\Lambda\)-algebras can be constructed as shown in diagram 1 (the distinguished element \(V\) is at the top).

It follows from these lemmas that there exists a sequence \(\{\alpha_i\}\) of incomparable \(\Lambda\)-algebras. It is convenient for us to assume that \(\{\alpha_i\}\) even contains all noniso-

* In \((^3)\) they were called implicative structures, which was not quite exact, since it did not reflect the presence of the operation \(\neg\). The terminology has not yet become fixed, but the term chosen in \((^2)\) seems unsuccessful.

** In \((^2)\) an equivalent notion of a strongly compact pseudo-Boolean algebra is introduced.

morphic \(\Lambda\)-algebras (being a \(\Lambda\)-algebra is a decidable property, as is isomorphism of finite Brouwer algebras). Then \(X_{\alpha_i}\) and \(a_i\) determine the desired calculi \(N_i\).

Indeed, for \(j \ne i\) all \(X_\alpha\) are generally valid on \(a_i\), in view of the incomparability of \(a_j\) and \(a_i\), while \(X_\alpha\) is refuted on \(a_i\), whence \(X_{\alpha_i}\) cannot be contained in the logic generated by all \(X_{\alpha_j}\) \((j \ne i)\).

Diagram 1

Corollary 1 (classical). There exists a continuum of distinct superintuitionistic logics.

Corollary 2. There exists a superintuitionistic logic that is not a calculus. (Such is the logic \(L\) generated by all \(X_\alpha\).)

Corollary 3. There exists a strictly increasing sequence \(M_i\) of superintuitionistic calculi \(\left(M_i\right.\) is determined by the axiom \(\displaystyle \mathop{\&}_{i=1}^{j} X_{\alpha_i}\)).

The logic \(L\) also has the following property. The formula

\[ F \equiv \neg(a_1 \& a_2)\ \&\ \neg(a_2 \& a_3)\ \&\ \neg(a_1 \& a_3)\ \& \]
\[ \&(\neg\neg a_3 \supset a_3)\ \&\ (\neg\neg a_2 \supset a_2)\ \&\ \neg\neg(a_1 \vee a_2 \vee a_3)\ \supset \]
\[ \supset \neg a_3 \vee \neg a_2 \vee (\neg\neg a_1 \supset a_1) \]

is not contained in \(L\), but there is no finite Brouwer algebra \(a\) on which \(F\) would be refuted while all formulas of \(L\) would be generally valid.

The first assertion follows from the fact that in a derivation of \(F\) we can use only a finite number of formulas \(X_{\alpha_i}\), but, taking \(a_j\) distinct from all such \(a_i\), we have: \(F\) is refuted on \(a_j\), while all \(X_{\alpha_i}\) are generally valid on \(a_j\).

If, however, \(F\) is refuted on some finite Brouwer algebra \(\alpha\) on which all \(\Lambda_{\alpha_i}\) are generally valid, then, after applying a finite number of times the passage from the algebra to some homomorphic image of it or to some subalgebra of it, we could find a \(\Lambda\)-algebra \(\beta\) with the same properties, but among the \(a_i\) there is an algebra isomorphic to it, so that \(X_{\alpha_i} \in L\) and \(X_{\alpha_i}\) is refuted on \(\beta\), which contradicts the assumption.

It follows from this theorem that Theorem 3, 4 formulated in \((^1)\) is false. The error in the proof (independently noticed by A. V. Kuznetsov and by me) consists in the implicit application of the relation

\[ \overline{\left(L \cap \bigcup_{i=1}^{\infty} L_i\right)} = \bigcap_{i=1}^{\infty} \overline{(L \cup L_i)}. \]

(Here \(L, L_i\) are logics, and the bar denotes closure with respect to the rules of inference), which is not always satisfied, as follows from the present work.

Moscow Institute of Physics and Technology

Received
14 IX 1967

REFERENCES

1. A. S. Troelstra, Proc. Kohinkl. Nederl. Akad. Wet., A68, No. 1 (1965).
2. H. Rasiowa, R. Sikorski, The mathematics of the metamathematics, Warszawa, 1963.
3. V. A. Yankov, DAN, 151, No. 6 (1963).