UDC 517.11:(51.01+519.4)

MATHEMATICS

A. V. KUZNETSOV, V. Ya. GERČIU

ON SUPERINTUITIONISTIC LOGICS AND FINITE APPROXIMABILITY

(Presented by Academician P. S. Novikov, May 14, 1970)

1. Besides the usual classical logic (of propositions) and the well-known intuitionistic logic, constructed on the basis of the intuitionistic propositional calculus \(I\) (see \((^5)\)), logics intermediate between them are often considered. Of those among them whose variety is caused by the difficulties of the semantic construction of a logic that takes into account intuitionistic and constructivist criticism of the laws of logic, the best known are the logic of recursive realizability of S. Kleene and J. Rosser (see \((^5)\)) and the logic of finite problems of Yu. T. Medvedev (see \((^{13,19})\)). The complexity of the investigation of these logics led to the construction of other—simpler—intermediate logics, as well as to the idea of a general study of all such logics. However, even for those of them that are finitely axiomatizable (i.e., are constructed on the basis of a finite list of axioms and the rules of substitution and modus ponens), the question remains open whether, for each of them, there exists an algorithm that makes it possible to recognize from a formula whether it is true in this logic. The hope for its existence was connected with the hypothesis of finite approximability of superintuitionistic (superconstructive) propositional calculi \((^{8в})\), p. 52).* The refutation of this hypothesis is the main result of the present work.

2. We proceed from the usual notion of a formula (of propositional logic) on the basis of an alphabet consisting of the signs of the operations \(&\), \(\vee\), \(\supset\), and \(\neg\), signs for variables \(a, b, c, a, \ldots\), and parentheses; a set of formulas containing all axioms of \(I\) and closed with respect to substitution and modus ponens is called a superintuitionistic logic \((^{8г,19в})\). The least (with respect to \(\subseteq\)) of such logics containing the given formulas \(A_1, A_2, \ldots\) is called the logic generated by the given formulas, and is denoted by \([A_1, A_2, \ldots]\). We say that from a formula \(A\) a formula \(B\) is derivable if \(B \in [A]\).

A means of detecting nonderivability is often a truth matrix, i.e., a set \(E\) with binary operations \(&\), \(\vee\), and \(\supset\), a unary operation \(\neg\), and a subset \(E' \subseteq E\) of “distinguished” elements. If this matrix is regular (i.e., from \(\alpha \in E'\) and \((\alpha \supset \beta) \in E'\) it follows that \(\beta \in E'\)), and the axioms of the calculus \(I\) take on it only values from \(E'\), then all this is preserved also after identifying every such \(\alpha\) and \(\beta\) for which \((\alpha \supset \beta) \in E'\) and \((\beta \supset \alpha) \in E'\). The matrix is thereby transformed into a *pseudoboolean algebra \((^{16})\), i.e., a system \(\langle M; \&, \vee, \supset, \neg\rangle\), which is a structure (lattice) \(\langle M; \&, \vee\rangle\) with relative pseudo-complement \(\supset\) and pseudo-complement \(\neg\) (see \((^1)\)), i.e., implicative—

* The possibility of various refinements of the contentual constructive logic (i.e., the logic of constructive direction in mathematics) was also reflected in the fact that intuitionistic logic, which many called constructive, is now again called intuitionistic. The terms “constructive calculus,” “superconstructive logic,” etc., have changed analogously.

** This hypothesis is, it is true, a consequence of the more general theorem 3.4 of \((^{17})\). However, the latter (in its proof in \((^{17})\) there was a noticeable gap) was refuted by A. Ya. Yankov \((^{19в})\).

*** On irregular matrices see \((^{18})\).

structure \(\langle M;\ &, \vee, \supset\rangle\) \({}^{(4)}\) with least element \(0\) and greatest (“distinguished”) element \(1\). We say that a formula \(A\) is true on a (pseudo-Boolean) algebra \(\mathfrak A\) if \(A=1\) on \(\mathfrak A\). The set of all formulas true on \(\mathfrak A\) is a superintuitionistic logic and is called the logic of the algebra \(\mathfrak A\). We say that an algebra separates a formula \(A\) from formulas \(B_1,B_2,\ldots\) if on it \(B_1,B_2,\ldots\) are true, while \(A\) is not true. If this algebra is finite, then the formula \(A\) is called finitely separable from \(B_1,B_2,\ldots\). A logic \(L\) is called finitely approximable if every formula not belonging to \(L\) is finitely separable from \(L\).* The hypothesis mentioned above is equivalent to the assertion that for all formulas \(A_1,\ldots,A_n\) the logic \([A_1,\ldots,A_n]\) (i.e. \([A_1\&\ldots\&A_n]\)) is finitely approximable, i.e. that every formula not derivable from \(A\) is finitely separable from \(A\).

Fig. 1  Fig. 2  Fig. 3

1. The idea of finite approximability goes back to the works of McKinsey \({}^{(11)}\), A. I. Mal'cev, and others. A universal algebra \(\mathfrak A\) is called finitely approximable \({}^{(12a)}\)** if for any two distinct elements \(\alpha\) and \(\beta\) of it there exists a homomorphism \(\sigma\) of the algebra \(\mathfrak A\) into some finite algebra such that \(\alpha\sigma\ne\beta\sigma\) (cf. \({}^{(12b)}\)). A superintuitionistic logic \(L\) is finitely approximable if and only if the free algebras of the corresponding variety \({}^{(6,12b)}\) of all those pseudo-Boolean algebras on which all formulas of \(L\) are true are finitely approximable. The logic of its free algebra with an infinite number of generators coincides with \(L\). Therefore, if \(B\) is not derivable from the formula \(A\), then \(B\) is separated from \(A\) by a free algebra of the variety corresponding to \([A]\), and even with a finite number of generators (i.e. finitely generated), since the number of variables in \(B\) is finite.

An implicative structure is called Gödelian \({}^{(8b,19a)}\) if its elements distinct from \(1\) form a substructure. Gödelian algebras are both free pseudo-Boolean algebras and those that are subdirectly irreducible. For the latter, and only for them, possess \({}^{(2,10a)}\) a *penultimate element \({}^{(3)}\), i.e. the greatest among the elements distinct from \(1\). From this and from the well-known Birkhoff theorem (see \({}^{(6)}\)) it follows (cf. \({}^{(10a)}\)):

Lemma 1. If \(B\) is not derivable from the formula \(A\), then \(B\) is separated from \(A\) by some finitely generated algebra with a penultimate element.

We say that a formula \(A\) is pretrue on an algebra \(\mathfrak A\) if \(A\) is not true on \(\mathfrak A\), but is true on every proper subalgebra of it and on every factor algebra of it modulo a nontrivial congruence. Such an algebra \(\mathfrak A\) is subdirectly irreducible. On every finite Gödelian algebra its characteristic (in Jankov’s sense \({}^{(19a,g)}\)) formula is pretrue. The following holds (see \({}^{(19g)}\), pp. 29–31):

Lemma 2. If \(A\) is finitely separable from \(B_1,B_2,\ldots\), then \(A\) is separated from them by some finite algebra on which \(A\) is pretrue.

1. We introduce “powers” \(A^n\) and “relative powers” \(A^nB\) as follows:

\[ A^0B \rightleftharpoons A\supset B,\qquad A^2B \rightleftharpoons A\&B,\qquad A^1B \rightleftharpoons A, \]

\[ A^{2n+3}B \rightleftharpoons A^{2n+1}B\supset A^{2n}B,\qquad A^{2n+4}B \rightleftharpoons A^{2n+1}B\vee A^{2n+2}B, \]

\[ A^\infty B \rightleftharpoons a\supset a,\qquad A^n \rightleftharpoons A^n(a\&\neg a)\qquad (n=0,1,2,\ldots,\infty). \]

* Cf. the notion of the finite model property (fmp) \({}^{(10b,18)}\).
* Or residually finite (see \({}^{(9)}\)), or checkable \({}^{(8a)}\).
** Cf. the well-known Gödel theorem on disjunctions; see \({}^{(5)}\), p. 429.

This is justified by the fact that—as in group theory—for every \(n=\) \(1,2,\ldots\) there exists a unique (up to isomorphism) cyclic (i.e., with one generating element) pseudoboolean algebra \(Z_n\) of cardinality \(n\), and it is the homomorphic image (also unique) of the infinite cyclic algebra \(Z_\infty\), i.e., of the free pseudoboolean algebra consisting of the “powers” of the generating element \(a\) (Fig. 1; cf. with \((^{14})\)),—its factor algebra (for \(n\geqslant 2\)) with respect to the filter (see \((^{16})\)) \(\nabla_n\), generated by \(a^n\). The subalgebra of the free implicative structure with generators \(a\) and \(\beta\), consisting of all elements of the form \(a^2\beta\), is isomorphic to \(\nabla_n\) for any even \(n\). The logic \(LZ\) of the algebra \(Z_\infty\) is finitely approximable, since all formulas true on all the algebras \(Z_1, Z_2,\ldots\) belong to it. Among them are the formulas

\[ (a \supset b)\vee(b \supset c)\vee((b\supset c)\supset c)\vee(c\supset(a\vee b)), \tag{1} \]

\[ a^7b \supset (c\vee(c\supset a^6b)). \tag{2} \]

Theorem 1. The logic \(LZ\) is finitely axiomatizable; it is generated by formulas (1) and (2).

By the serial connection of algebras \(\mathfrak A\) and \(\mathfrak B\) we mean the algebra \(\mathfrak A+\mathfrak B\) (cf. \((^{17})\)), consisting of such of its substructures \(\mathfrak A'\) and \(\mathfrak B'\), isomorphic respectively to \(\mathfrak A\) and \(\mathfrak B\), whose intersection contains exactly one element—the greatest in \(\mathfrak A'\) and the least in \(\mathfrak B'\). We call a structure narrow if in it there are no elements \(\alpha,\beta,\gamma\), and \(\delta\) such that \(\alpha<\beta\), \(\gamma<\delta\), \(\alpha\) is not comparable with \(\delta\), and \(\beta\) is not comparable with \(\gamma\).

Lemma 3. A Gödel structure is narrow if and only if formula (1) is true on it.

Lemma 4. Every finitely generated narrow pseudoboolean algebra is a serial connection of a finite number of cyclic ones.

The proof of Theorem 1 rests on Lemmas 1, 3, and 4, on a survey of subalgebras and homomorphic images of algebras of the form \(Z_i+\cdots+Z_k\), on the coincidence of the logic of the algebra \(Z_\infty+\cdots+Z_\infty\) with \(LZ\), and also on the fact that formula (2) is not true on the algebras \(Z_7+Z_2\), \(Z_9+Z_2\), and \(Z_2+Z_7+Z_2\).

1. With a formula \(A\) we associate the logic generated by the characteristic formulas of all finite algebras on which \(A\) is refutable. If there are infinitely many of these algebras, pairwise nonisomorphic, then the formula \(A\) is called scattered. Examples of scattered formulas:

\[ \neg\neg a \vee \vee(\neg\neg a \supset(\neg b\vee(\neg b\supset a))), \]

\[ \neg\neg a\vee\neg(a\& b)\vee(\neg(a\supset b)\supset a) \]

\(*\) (refutable on algebras of the form \((Z_{2n}\times Z_2)+Z_2\) \(**\), beginning with some \(n\)). Generalizing Yankov’s result \((^{19в})\), one obtains

Theorem 2. If \(A\) is a scattered formula, then the logic \(\mathfrak A\) associated with \(A\) is not finitely approximable: \(A\) is not finitely separable from \(\mathfrak A\), although it is finitely separable from any formula in \(\mathfrak A\).

1. For contrast we give the following generalization of Theorem 2.2 from \((^{10б})\):

Theorem 3. Every logic generated by formulas having no negative occurrences of the sign \(\vee\) \(***\) is finitely approximable.

This also follows from the theorem of Popel’—Diego on the finiteness of a finitely generated implicative semistructure \(\langle M;\&, \supset\rangle\) \(****\), since any such formula is stable in the following sense: if it is true on the pseudoboolean algebra \(\langle M;\&, \vee, \supset, \neg\rangle\), then it is also true on every finite subalgebra of the algebra \(\langle M;\&, \subseteq,\neg\rangle\) (\(\vee\) is completed).

\(*\) Deductively equal to the formula \(F\) from \((^{19в})\), p. 34 (i.e., generates \([F]\)).

\(**\) These algebras are taken from \((^{19в})\). \(\times\) denotes direct product.

\(***)\) That is, such that it lies in the scope of an odd number of occurrences of \(\supset\) to its right, and of occurrences of \(\neg\).

\(****\) A. V. Popel’ reported it in 1963 at the V. A. Steklov Mathematical Institute of the USSR Academy of Sciences as a theorem on formulas without \(\vee\) (see \((^{19г})\)); in Diego \((^{3})\) it is for “Hilbert algebras,” i.e., for implicative \((^{8д})\) (but not easily carried over to implicative semistructures \((^{4,10б})\)). It follows from a proposition analogous to Lemma 1 (cf. \((^{2})\)), since discarding the penultimate element reduces the number of generators.

We note that formula (2) is not stable (since the algebra \(Z_7+Z_2\), considered without \(\vee\), is isomorphically embeddable in \(Z_{11}\)); the formula \(a^n\) is stable only for \(n\leq 8\) or \(n=10\), and the formula \(a^n b\)—for \(n\leq 11\). It is worth recalling here Burnside’s problems on periodic groups (see \((^7,^9,^{15})\)) and their connection with questions of finite approximability.* However, the analogy with groups is weakened by the fact that the formula \(a^n\) for \(n\geq 6\) is true on the algebra \(Z_2+Z_\infty\) with two generators, which has infinitely many pairwise nonisomorphic finite factor algebras, while the formula \(a^n b\) for \(n\geq 14\) is true on the same kind of algebra, shown in Fig. 2.

1. A refutation of hypothesis \((8^{\mathrm{v}})\) was found in analyzing an example of a formula refutable on an infinite chain algebra. This algebra is \(Z_\infty+Z_7+Z_2\) (Fig. 3), and the formula is the first of the following:

\[ (a^7b \supset (c\vee(c\supset a^6b)))\vee d^8, \tag{3} \]

\[ a^7\supset (b\vee(b\supset a^6)), \tag{4} \]

\[ a^9b\supset (c\vee(c\supset a^8b)). \tag{5} \]

Theorem 4. Formula (3) is separated from formulas (1), (4), and (5) by the algebra \(Z_\infty+Z_7+Z_2\), but is not finitely separable from them.

The latter follows from Lemmas 2, 3, and 4 and from the fact that an algebra of the form \(Z_n+\mathfrak{B}+Z_2\) \((2\leq n<\infty)\) does not separate (3) from (1), (4), and (5).

We note that the logic of the algebra \(Z_\infty+Z_7+Z_2\) is not finitely approximable, but is decidable (the deciding algorithm is limited to checking the formula on a finite subspace whose cardinality is proportional to the length of the formula); it is generated by the formulas (1), (4), (5), \(a^7b\supset(c\vee(c\supset(d\vee(d\supset a^6b))))\), \(a^7b\supset((c\supset d)\vee(d\supset c)\vee(c\supset a^6b))\), and \(a^7(b^6c)\supset(d\vee(d\supset a^6(b^6c)))\).

Institute of Mathematics with Computing Center
Academy of Sciences of the Moldavian SSR
Kishinev

Received
14 V 1970

CITED LITERATURE

1. G. Birkhoff, Theory of Structures, IL, 1952.
2. R. A. Bull, J. Symb. Logic, 29, 33 (1964).
3. A. Diego, Sur les algèbres de Hilbert, Paris, 1966.
4. H. Curry, Foundations of Mathematical Logic, Moscow, 1969.
5. S. K. Kleene, Introduction to Metamathematics, IL, 1957.
6. P. Cohn, Universal Algebra, Moscow, 1968.
7. A. I. Kostrikin, Izv. AN SSSR, Ser. Mat., 23, 3 (1959).
8. A. N. Kuznetsov, a) Tr. 3rd All-Union Mathematical Congress, 2, Moscow, 1956, p. 145; b) Fifth All-Union Colloquium on General Algebra, Abstracts, Novosibirsk, 1963, p. 32; c) Algebra and Logic, Seminar, 2, no. 4, 47, Novosibirsk (1963); d) DAN, 160, 274 (1965); e) Seventh All-Union Colloquium on General Algebra, Abstracts, Kishinev, 1965, p. 60.
9. A. G. Kurosh, Theory of Groups, Moscow, 1967.
10. C. G. McKay, a) Proc. Koninkl. Nederl. Acad. Wet., A70, 363 (1967); b) J. Symb. Logic, 33, 258 (1968).
11. J. C. C. McKinsey, J. Symb. Logic, 8, 61 (1943).
12. A. I. Maltsev, a) Uch. zap. Ivanovsk. ped. inst., 18, 49 (1958); b) Algebraic Systems, Moscow, 1970.
13. Yu. T. Medvedev, DAN, 142, 1015 (1962).
14. I. Nishimura, J. Symb. Logic, 25, 327 (1960).
15. P. S. Novikov, S. I. Adyan, Izv. AN SSSR, Ser. Mat., 32, 212 (1968).
16. H. Rasiowa, R. Sikorski, The Mathematics of Metamathematics, Warszawa, 1963.
17. A. S. Troelstra, Proc. Koninkl. Nederl. Acad. Wet., A68, 141 (1965).
18. R. Harrop, Proc. Cambr. Philos. Soc., 54, 1 (1958).
19. V. A. Yankov, a) DAN, 151, 1293 (1963); b) DAN, 174, 302 (1967); c) DAN, 181, 33 (1968); d) Izv. AN SSSR, Ser. Mat., 33, 18 (1969).

* From the results of A. I. Kostrikin \((^7)\), P. S. Novikov and S. I. Adyan \((^{15})\) it follows that, for prime \(n\geq 4381\), in the variety of groups defined by the identity \(a^n=1\), its free group with 2 generators is not finitely approximable.