Reports of the Academy of Sciences of the USSR
1970. Vol. 195, No. 6

UDC 517.11:(51.01+519.95)

MATHEMATICS

V. Ya. Gerchiu, A. V. Kuznetsov

ON FINITELY AXIOMATIZABLE SUPERINTUITIONISTIC LOGICS

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

1. In the present paper we use the terminology and notation of ((^8)). The studies of superintuitionistic propositional logics carried out in Kishinev since 1963 have as one of their aims the description of those of these logics that are finitely axiomatizable and, moreover, are generated by formulas of small length (by the length of a formula we mean its propositional length, i.e. the number of occurrences of variables). This problem arose in connection with the hypothesis on the finite approximability of superintuitionistic (superconstructive) propositional calculi ((^{7a})). This hypothesis was refuted in ((^8)), but the question remains open whether there exists an algorithm which, given formulas (A) and (B), recognizes whether (A \vdash B), i.e. whether (B) is derivable from (A) (in the intuitionistic propositional calculus with the postulated substitution rule ((^6))).

Already in 1961, when this hypothesis was stated at a seminar at Moscow University, Yu. T. Medvedev suggested that it was false, connecting it with the result of Umezawa ((^{15б})), who constructed a decreasing chain of logics ordered according to type (\omega^\omega). This predetermined the interest in the isomorphic embedding of various systems into the structure (lattice, lattice)* (\mathfrak L) of all superintuitionistic logics or into the dually isomorphic structure (\mathfrak M) of all varieties of pseudoboolean algebras.

Another guide for the investigations is the still unsolved problem of functional completeness in intuitionistic logic, generalized also to other logics. It consists in the requirement to construct a (practically convenient) algorithm which, from a list of formulas, recognizes whether it is functionally complete in the given logic ((^{7б})). For the logic of the algebra (Z_3) (i.e. the first of Jaśkowski’s matrices) such a problem was investigated in detail and solved by M. F. Ratsa ((^{14a-в})), who obtained a convenient algorithm**.

2. We say that a formula (A) is deductively equal to a formula (B) (we write (A \dashv\vdash B)) if (A \vdash B) and (B \vdash A), i.e. if ([A]=[B]). We say that they are equivalent if (\vdash A \sim B) ([A \sim B) means ((A \supset B)\ \&\ (B \supset A)); (\vdash D) means (a \supset a \vdash D]). We call a formula (n)-place ((^{7б})) if the number of distinct variables occurring in it is equal to (n). By the symbol (A[B_1,B_2,\ldots]) we denote the result of substituting the formulas (B_1,B_2,\ldots), respectively, for the variables (a,b,\ldots) in the formula (A). By the signs (F_0,F_1,\ldots,F_{19}) we denote, respectively, the following formulas:

[
\begin{gathered}
a \supset a,\quad a,\quad a \vee \neg a,\quad \neg a \vee \neg\neg a,\quad
\neg\neg a \vee (\neg\neg a \supset a),\quad
a \vee \neg b \vee (a \supset b),\
a \vee (a \supset (b \vee \neg b)),\quad
(a \supset b) \vee (b \supset a),\quad
F_6[a,\neg b],\quad F_3[\neg a,\neg b],\
(a \supset b) \vee (b \supset F_2),\quad
F_6 \vee \neg\neg b,\quad
\neg a \vee (\neg a \supset b) \vee (b \supset a),\quad
a \vee (a \supset F_4[b]),\
\neg\neg a \vee (\neg\neg a \supset (b \vee (b \supset a))),\quad
(a \supset b) \vee (b \supset F_3),\quad
\neg\neg a \supset ((b \supset a) \vee\
\vee(\neg b \supset a)),\quad
\neg\neg a \vee \neg(a\& b) \vee \neg(a\& \neg b),\quad
F_{14}[a,\neg b]\cdot(\neg\neg a \supset b) \vee\
\vee(\neg a \supset F_3[b])\ ***.
\end{gathered}
]

* By (\subseteq), or by (\cap) and closed (relative to modus ponens) union.

** Recently generalized by him to algebras of the form (Z_2+\cdots+Z_2).

*** These formulas are numbered here in the same way as in ((^4)), although in place of (F_{12}) and (F_{16}) in ((^4)) there were other formulas deductively equal to them.

By the relation (\vdash) the set ({F_0,F_1,\ldots,F_{19}}) is partially ordered as shown in Fig. 1. Indeed, all the derivabilities indicated there are obvious or follow from the fact that the following formulas belong to ([F_0]) (i.e., to intuitionistic logic): (F_3[b]\supset F_{11}), (F_4[a\&b]\supset (F_4[(a\vee \neg a)\& b]\supset F_{15})), (F_4[(a\vee \neg a)\&\neg b]\supset F_{16}), (F_3\supset F_{13}), (F_7[a,\neg a]\supset F_3), (F_8[b,a]\supset F_{15}), (F_9[\neg a]\supset F_{18}), (F_9\supset F_{19}), (F_{10}[a\vee\neg a,\neg\neg a]\supset F_4), (F_{11}[\neg\neg a,a]\supset F_4), (F_{12}[\neg a,a]\supset F_4), (F_{12}[\neg a]\supset F_{17}), (F_{13}[\neg\neg a,(a\vee\neg a)\&\& \neg b]\supset F_{18}), (F_{15}[a\vee b,\neg a]\supset F_9), (F_{16}[(a\vee\neg a)\&(b\vee\neg b),\neg a]\supset F_{19}), (F_{17}[\neg a]\supset F_9). The absence of other derivabilities is established by means of the following algebras ((\mathfrak A^+) denotes (\mathfrak A+Z_2), and (\mathfrak A^n) denotes (\mathfrak A\times\mathfrak A\times\cdots\times\mathfrak A), where (\mathfrak A) occurs (n) times): 1) (Z_2), 2) (Z_3), 3) (Z_3^+), 4) (Z_2+Z_5), 5) (Z_5^+), 6) (Z_7^+), 7) ((Z_3^+\times Z_2)^+), 8) (Z_{11}), 9) ((Z_3^2)^+), 10) ((Z_2^3)^+), 11) ((Z_7\times Z_2)^+), 12) ((Z_5\times Z_3)^+); to each of them there corresponds in Fig. 1 a dashed line showing which formulas (true in it) it separates from which (false ones).

Fig. 1

1. Theorem 1. None of the formulas (F_0,F_1,\ldots,F_{19}) can be deductively equal to any formula of smaller length; every formula of length (\le 5) is deductively equal to one of the formulas (F_0,F_1,\ldots,F_{19}).

This was found by enumerating cases for formulas not containing variables other than (a) and (b)*, relying on a list of all (up to equivalence) such formulas of length (\le 3) (there are 200 of them).

The formulas (F_0,F_1,\ldots,F_{19}) have no negative occurrences of disjunction. Therefore, from Theorem 3 of the article ((^8)) and Theorem 1 it follows that

Theorem 2. Every logic generated by some formulas of length (\le 5) is finitely approximable.

Let us note that the formulas (F_0,F_1), and (F_2) are well known; (F_3) has also been considered more than once (see, for example, ((^2)), p. 212, and ((^{20г}))), (F_4) (see ((^{16в},\,^{13},\,^{20б})); equivalent to (a^8)) and (F_7) (see ((^{16а})), p. 186, ((^5,\,^{12}))); (F_5) occurs in ((^{16а})) (in the form of the sequent (R_2); cf. ((^{18}))) and is deductively equal to Smetanich’s formula ((a\supset b)\vee(b\supset c)\vee(c\supset d)) (see ((^{20а}))); (F_6) is the formula (M) from ((^{20а})), and also (P_2) from ((^{18})); (F_8) is the formula (P_2) from ((^9)), and also the characteristic formula ((^{20д})) of the algebra (Z_5^+); (F_{18}) was used in ((^8)); (F_{11}\dashv\vdash F_4\&F_8); (F_{12}\dashv\vdash F_4\&F_{17}); (F_{15}\dashv\vdash F_9\&a^{10}).

1. We say that logics (L_1) and (L_2) are (n)-locally equal if the (n)-place formulas belonging to the logic (L_1) are all and only those that belong to (L_2). Every superintuitionistic logic is (n)-locally equal to the logic of some (pseudo-Boolean) algebra with (n) generators. In particular, ([F_0]) is one-locally equal to (LZ) ((^8)). Note that among the formulas (F_0,F_1,\ldots,F_{19}), those and only those that are true in (Z_{11}) belong to (LZ). And the logic ([\neg a_1\vee(\neg a_1\supset \supset(\ldots\supset(\neg a_k\vee(\neg a_k\supset(\neg b\vee\neg\neg b)))\ldots))]), where (k=2^n-1), is (n)-locally equal to ([F_0]), as is proved with the aid of Glivenko’s theorem ((^6)).

We call a logic tabular* if it is the logic of some finite algebra. A logic (n)-locally equal to a tabular one is called (n)-locally tabular**. In particular, if a formula (A) does not belong to (LZ), then the logic ([A]) is one-locally tabular. If (F_3\vdash A), then the logic ([A]) is two-locally—

* Formulas of length (\le 2n+1) for (n\ge 1) are deductively equal to (n)-place formulas.

** The method by which this is proved does not apply to formulas of length 6, since, for example, the formula (((\neg\neg a\supset a)\supset(a\vee\neg a))\supset(\neg a\vee\neg\neg a)), equivalent to (a^9), is not stable; indeed, it is not true in (Z_7), but is true in the algebra (Z_9), into which (Z_7), considered without (\vee) (with (\supset) and (\neg)), is isomorphically embeddable.

*** Sometimes it is called finite ((^{15})), although its cardinality is infinite.

but is not tabular, since each of the formulas (a^1 b, a^2 b,\ldots) is separated from (F_3) by the algebra (Z_2+Z_\infty). However, the following is true.

Theorem 3. If (A \vdash F_{10}), then the logic ([A]) is (n)-place tabular for every (n=1,2,\ldots)*.

Indeed, such a logic is, in (n) variables, equal to the logic of the direct product of a finite number of algebras of the form ((Z_2^k)^+\ldots^+), where (k\leqslant 2^n), since on other Gödel algebras with (n) generators (F_{10}) is not valid.

1. Finitely axiomatizable superintuitionistic logics form, as M. M. Mints ((^{11})) and Yankov observed, a substructure in (\mathcal L). Dually isomorphic to it is the structure (\mathfrak F) of all formulas—considered up to deductive equivalence—relative to (\vdash) (for (A\vdash B) is equivalent to ([B]\subseteq[A])). The role of the operations of the structure (\mathfrak F) is played by conjunction (\&) and repeated disjunction (\vee') ((A\vee' B) denotes the formula (A\vee B_1), where (B_1) is the result of such a renaming of variables in (B) under which their numbers (more exactly, their positions in the alphabetical sequence of all variables) are increased by the maximum of the numbers of the variables occurring in (A)). The structure (\mathfrak F) is distributive (for the formula (A\vee'(B\& C)) is equivalent to ((A\vee' B)\&(A\vee' C)); cf. ((^{18}))).

Let us note that

[
F_3\vee' F_6 \dashv\vdash F_{11},\quad
F_4\vee' F_8 \dashv\vdash F_{13}\& F_{15}\ **,\quad
\text{and } F_6\vee' F_7 \dashv\vdash F_{10}\& F_{11}.
]

The formulas of length (\leqslant 4) generate in (\mathfrak F) a substructure on 13 formulas:
(F_0,F_1,\ldots,F_9,F_{11},F_4\vee' F_8) and (F_6\vee' F_7) ***.

Formulas (A_1,A_2,\ldots) are called (strongly) independent (cf. ((^{20в,15,166}))) if no formula (A_i) belongs to ([A_1,A_2,\ldots,A_{i-1},A_{i+1},A_{i+2},\ldots]). We call them superindependent if they generate in (\mathfrak F) a free distributive substructure, being free generators in it. This is equivalent to the fact that, for no pairwise distinct (i,\ldots,j,k,\ldots,l), does the following hold:

[
A_i\&\ldots\& A_j \vdash A_k\vee'\ldots\vee' A_l .
\tag{1}
]

For example, the formulas (F_{10},F_{11},F_{12}) are independent (Fig. 1), but not superindependent ((F_{11}\vdash F_{10}\vee'F_{12})). The substructure generated in (\mathfrak F) by formulas of length (\leqslant 5) has cardinality (>7500) (see ((^2)), p. 208); indeed, the following is true.

Theorem 4. The formulas (F_{13},F_{14},F_{15},F_{16},F_{17}) are superindependent. ****

A repeated disjunction of formulas that are false on a Gödel algebra is also false on it. Therefore, to prove the theorem it suffices, considering suitable algebras—some subalgebras of the algebras (Z_{11}), ((Z_8\times Z_3^+)^+), ((Z_6\times Z_3^{++})^{++}), (((Z_3\times Z_3^+)^{++}\times Z_3^+)^{++}),—to check which of the formulas (F_{13},\ldots,F_{17}) are valid on them.

1. Theorem 5. For every positive integer (n) there exist (n) superindependent formulas of length (2n+2). An example is given by those (n) formulas, the (i)-th of which is the result of substituting the formula (\neg a_i) into the formula

[
a_1\vee\bigl(a_1\supset(\ldots\supset(a_n\vee(a_n\supset(\neg b\vee\neg\neg b)))\ldots)\bigr)
]

in place of (a_i) ((^3)).

For the proof it suffices to check the formulas on algebras of the form
[
((\ldots((Z_2^2)^+\times \mathfrak A_1)^+\times\ldots)^+\times \mathfrak A_n)^+,
]
where (\mathfrak A_1,\ldots,\mathfrak A_n) are (Z_1) or (Z_2).

From Theorem 5 (with the aid of Corollary 1 to Theorem 1 from ((^{17}))) there follows the

Corollary. Every finite distributive structure (\langle M;\cap,\cup\rangle) is isomorphically embeddable in the structure (\mathfrak F).

* From the two-place equality of logics (L_1) and (L_2) it follows that the functionally complete systems of formulas in (L_1) are the same as in (L_2). Therefore, for a two-place tabular logic the problem of functional completeness is decidable—by means of constructions of the same kind as those in ((^{19})), §§ 10 and 13.

** Since
[
\vdash F_{11}[b,a]\supset(F_{11}[a,a\& c]\supset(F_{11}[\neg a,\neg a\& c]\supset(F_3\vee' F_6)))
]
and
[
\vdash F_{13}[b,a]\supset(a^{10}\supset(F_9[a,c]\supset(F_9[\neg a,c]\supset(F_4\vee' F_8))).
]

*** Deductively equal to
[
((\neg\neg a\supset a)\supset b)\vee(b\supset(a\vee'\neg a)).
]

**** ((^4)); in general, the formulas of a set (M\subseteq{F_0,F_1,\ldots,F_{19}}) of cardinality (\geqslant 3) are superindependent if and only if (M) is included in
({F_4,F_8,F_{17}}), ({F_8,F_{10},F_{12}}), ({F_8,F_{10},F_{17}}),
({F_{13},F_{14},F_{19}}), ({F_8,F_{14},F_{16},F_{17}}),
({F_9,F_{13},F_{14},F_{16}}), or
({F_{13},F_{14},F_{15},F_{16},F_{17}})
(see ((^3)), but there are misprints there in the indices).

1. An example of an infinite sequence of independent formulas was constructed by Jankov ((^{20\mathrm{v}})) *. Such a sequence can be constructed by means of any scattered formula—after all, the characteristic formulas of those (non-isomorphic) finite algebras on which the given formula is refutable are independent. In the direction of strengthening Jankov’s result the following has been obtained.

Theorem 6. The formulas
[
a^{2n+5}\supset\bigl(b\vee(b\supset a^{2n+4})\bigr),\quad \text{where } n=1,2,\ldots,
]
are superindependent.

Indeed, these formulas (A_1,A_2,A_3,\ldots) are deductively equal to the characteristic formulas of the algebras (Z_7^+, Z_9^+, Z_{11}^+,\ldots), respectively. To prove that for pairwise distinct (i,\ldots,j,k,\ldots,l) (1) cannot hold, it is enough to note that the formulas (A_k,\ldots,A_l) are not true on the algebra ((Z_{2k+5}\times\cdots\times Z_{2l+5})^+), and to show that the formulas (A_i,\ldots,A_j) are true on it. If, for example, (A_i) were not true on it, then a homomorphic image of this algebra would contain an algebra isomorphic to ((Z_{2i+5})^+) (see ((^{20\mathrm{d}})), p. 30). And from this, since the formula (a^7b\supset(c\vee(c\supset a^6b))) (from (8)), false on ((Z_{2i+5})^+), is true on the algebra (Z_{2k+5}\times\cdots\times Z_{2l+5}), it follows that (Z_{2i+5}) is isomorphically embedded in the latter. But this contradicts the fact that the quasi-identity ((^{1\circ}))
[
(a^{2i+5}=1)\supset(a^{2i+4}=1)
]
is not true on (Z_{2i+5}) **, while it is true on the algebras (Z_{2k+5},\ldots,Z_{2l+5}).

The question of whether every countable distributive lattice is isomorphically embeddable in the structure (\mathfrak F) remains open. However, the following holds.

Corollary. Every countable partially ordered set (\langle M;\leq\rangle) is isomorphically embeddable in the structure (\mathfrak F).

Institute of Mathematics with Computing Center
Academy of Sciences of the MSSR
Kishinev

Received
14 V 1970

REFERENCES

(^{1}) S. I. Adian, DAN, 190, 499 (1970).
(^{2}) G. Birkhoff, Lattice Theory, IL, 1952.
(^{3}) V. Ya. Gerchiu, All-Union Symposium on Mathematical Logic, Abstracts, Alma-Ata, 1969, p. 7.
(^{4}) V. Ya. Gerchiu, A. V. Kuznetsov, IX All-Union Algebraic Colloquium, Abstracts, Gomel, 1968, p. 54.
(^{5}) M. Dummett, J. Symb. Logic, 24, 97 (1959).
(^{6}) S. K. Kleene, Introduction to Metamathematics, IL, 1957.
(^{7}) A. V. Kuznetsov, a) Algebra and Logic, seminar, 2, no. 4, Novosibirsk, 1963, p. 47; b) DAN, 160, 274 (1965).
(^{8}) A. V. Kuznetsov, V. Ya. Gerchiu, DAN, 195, no. 5 (1970).
(^{9}) C. G. McKay, J. Symb. Logic, 33, 258 (1968).
(^{10}) A. I. Maltsev, Algebraic Systems, M., 1970.
(^{11}) S. Miura, Nagoya Math. J., 26, 167 (1966).
(^{12}) A. Monteiro, Rev. Union mat. argent. y Asoc. fis. argent., 20, 308 (1962).
(^{13}) I. Nishimura, J. Symb. Logic, 25, 327 (1960).
(^{14}) M. F. Ratsa, a) Collection: Studies in General Algebra, Kishinev, 1965, p. 99; b) DAN, 168, 524 (1966); c) Problems of Cybernetics, no. 21, 185 (1969).
(^{15}) A. S. Troelstra, Proc. Koninkl. Nederl. Acad. Wet., A68, 141 (1965).
(^{16}) T. Umezawa, a) Nagoya Math. J., 9, 181 (1955); b) J. Symb. Logic, 24, 20 (1959).
(^{17}) N. G. Khisamiev, Algebra and Logic, seminar, 6, no. 4, 107, Novosibirsk (1967).
(^{18}) T. Hosoi, J. Fac. Sci. Univ. Tokyo, Sec. 1, 14, 293 (1967).
(^{19}) S. V. Yablonskii, Tr. Matem. Inst. im. V. A. Steklova, AN SSSR, 51, 5 (1958).
(^{20}) V. A. Jankov, a) DAN, 151, 796 (1963); b) DAN, 103,; c) DAN, 181, 33 (1968); d) Izv. AN SSSR, ser. matem., 32, 1044 (1968); e) ibid., 33, 18 (1969).

* Having thereby proved that the cardinalities of the structures (\mathfrak L) and (\mathfrak M) are continuum ((^{20\mathrm{v}})). An analogous result for groups was reported at the X Algebraic Colloquium by A. Yu. Olshanskii; but an explicit example of an analogous sequence of group identities was indicated by S. I. Adian ((^1)).

** It is not equivalent to the formula (a^{2i+5}\supset a^{2i+4}). This for (i=1) was noted by Jankov (see the footnote at the end of the article ((^{7\mathrm{b}}))).