Proof. The two maps are isotone, and $\mathcal {L} = \operatorname {\mathrm {Log}}_{\omega } \operatorname {\mathrm {Mod}}_{\omega }^{*} \mathcal {L}$ for each $\mathcal {L}$ in $ \operatorname {\mathrm {Ext}}_{\omega } \mathcal {B}$ by the finitarity of $\mathcal {L}$ and the local finiteness of $ \operatorname {\mathrm {Alg}}^{*} \mathcal {B}$ . Moreover, $\mathsf {K} \subseteq \operatorname {\mathrm {Mod}}_{\omega }^{*} \operatorname {\mathrm {Log}}_{\omega } \mathsf {K}$ for each class $\mathsf {K} \subseteq \operatorname {\mathrm {Mod}}_{\omega }^{*} \mathcal {B}$ . It therefore remains to prove that $ \operatorname {\mathrm {Mod}}_{\omega }^{*} \operatorname {\mathrm {Log}}_{\omega } \mathsf {K} \subseteq \mathbb {S}^{*} \mathbb {P}^{*} (\mathsf {K})$ .

Let $\mathbb {A}$ be a finite reduced model of $ \operatorname {\mathrm {Log}}_{\omega } \mathsf {K}$ of cardinality n with $\mathsf {K} \subseteq \operatorname {\mathrm {Mod}}_{\omega }^{*} \mathcal {B}$ . Then $\mathbb {A} \in \mathbb {H}_{\mathrm {S}} \mathbb {S} \mathbb {P} \mathbb {P}_{\mathrm {U}} (\mathsf {K})$ by Theorem 2.1. There is an n-generated (hence finite) matrix $\mathbb {B} \in \mathbb {S} \mathbb {P} \mathbb {P}_{\mathrm {U}} (\mathsf {K})$ such that $\mathbb {A} \in \mathbb {H}_{\mathrm {S}} (\mathbb {B})$ . The condition $\mathbb {B} \in \mathbb {S} \mathbb {P} \mathbb {P}_{\mathrm {U}} (\mathsf {K})$ implies that there are finitely many $\mathbb {C}_{i} \in \mathbb {P}_{\mathrm {U}} (\mathsf {K})$ for $i \in I$ with strict homomorphisms $h_{i}\colon \mathbb {B} \rightarrow \mathbb {C}_{i}$ such that $\bigcap \{ \operatorname {\mathrm {Ker}} h_{i} \mid i \in I \} = \Delta _{\boldsymbol {B}}$ , where $\Delta _{\boldsymbol {B}}$ is the identity relation on $\boldsymbol {B}$ and $ \operatorname {\mathrm {Ker}} h_{i}$ is the kernel of the homomorphism $h_{i}$ . It follows that there are n-generated (hence finite) matrices $\mathbb {D}_{i} \leq \mathbb {C}_{i}$ such that $\mathbb {D}_{i}$ is the range of $h_{i}$ . Each such matrix $\mathbb {D}_{i}$ is an n-generated submatrix of an ultraproduct of matrices in $\mathsf {K}$ , and therefore embeds into an ultraproduct of n-generated submatrices of matrices in $\mathsf {K} \subseteq \operatorname {\mathrm {Alg}}^{*} \mathsf {K}$ . Since $ \operatorname {\mathrm {Alg}}^{*} \mathcal {L}$ generates a locally finite variety, there are only finitely many such n-generated submatrices. The matrices $\mathbb {D}_{i}$ are thus submatrices of matrices in $\mathsf {K}$ , i.e., $\mathbb {D}_{i} \in \mathbb {S} (\mathsf {K})$ for $i \in I$ . Therefore $\mathbb {A} \in \mathbb {H}_{\mathrm {S}} \mathbb {S} \mathbb {P}_{\omega } \mathbb {S} (\mathsf {K}) \subseteq \mathbb {H}_{\mathrm {S}} \mathbb {S} \mathbb {P}_{\omega } (\mathsf {K})$ , where $\mathbb {P}_{\omega }$ stands for finite products. Since the matrix $\mathbb {A}$ is reduced, we in fact have $\mathbb {A} \in \mathbb {S}^{*} \mathbb {P}_{\omega } (\mathsf {K}) \subseteq \mathbb {S}^{*} \mathbb {P}_{\omega }^{*} (\mathsf {K})$ .

Fact 3.2. Let p be a variable which does not occur in $\Gamma $ . Then $\Gamma $ is an antitheorem of $\mathcal {L}$ if and only if $\Gamma \vdash _{\mathcal {L}} p$ .

Fact 3.3. The following are equivalent:

1. 1. $\Gamma $ is an antitheorem of $\mathcal {L}$ ,

2. 2. $\sigma _{p} [\Gamma ] \vdash _{\mathcal {L}} p$ ,

3. 3. $\sigma [\Gamma ] \vdash _{\mathcal {L}} \varphi $ for each formula $\varphi $ and each substitution $\sigma $ .

Proof. If $\sigma [\Gamma ] \nvdash _{\mathcal {L}} \varphi $ , then there is a model $\langle \boldsymbol {A}, F \rangle $ of $\mathcal {L}$ and a valuation v on it such that $v[\sigma [\Gamma ]] \subseteq F$ but $v(\varphi ) \notin F$ . Thus $\langle \boldsymbol {A}, F \rangle $ is a non-trivial model of $\mathcal {L}$ and the valuation $w(\varphi ) = v(\sigma (\varphi ))$ witnesses that $\Gamma $ is not an antitheorem.

Conversely, if $\Gamma $ is not an antitheorem of $\mathcal {L}$ , then there is a valuation v on some non-trivial model $\langle \boldsymbol {A}, F \rangle $ of $\mathcal {L}$ such that $v[\Gamma ] \subseteq F$ . Consider the valuation w on $\langle \boldsymbol {A}, F \rangle $ such that $w(p) \notin F$ and $w(q) = v(q)$ otherwise. Then $(w \circ \tau _{p})[\sigma _{p} [\Gamma ]] = w[(\tau _{p} \circ \sigma _{p}) [\Gamma ]] = w[\Gamma ] \subseteq F$ while $(w \circ \tau _{p})(p) = w(p) \notin F$ . Thus $\sigma _{p} [\Gamma ] \nvdash _{\mathcal {L}} p$ .

The remaining implication is trivial: we instantiate $\sigma $ by $\sigma _{p}$ and $\varphi $ by p.

Proof. The right-to-left direction is obvious, since $\Gamma \vdash _{\mathcal {L}} \emptyset $ implies $\sigma [\Gamma ] \vdash _{\mathcal {L}} \emptyset $ . To prove the opposite direction it suffices to verify that the condition on the right-hand side of the equivalence indeed defines a logic.

Fact 3.6. $\mathcal {L}$ is an explosive extension of $\mathcal {B}$ if and only if $\mathcal {L} = \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}$ .

Fact 3.7. $ \operatorname {\mathrm {Exp}}_{\mathcal {B}}$ is an interior operator on $ \operatorname {\mathrm {Ext}} \mathcal {B}$ . That is, it is isotone and $ \operatorname {\mathrm {Exp}}_{\mathcal {B}} \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L} = \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L} \leq \mathcal {L}$ .

Fact 3.8. $ \operatorname {\mathrm {Exp}}_{\mathcal {B}} \bigcap _{i \in I} \mathcal {L}_{i} = \bigcap _{i \in I} \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}_{i}$ .

Proof. The inequality $ \operatorname {\mathrm {Exp}}_{\mathcal {B}} \bigcap _{i \in I} \mathcal {L}_{i} \leq \bigcap _{i \in I} \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}_{i}$ holds because $ \operatorname {\mathrm {Exp}}_{\mathcal {B}}$ is an interior operator. Conversely, suppose that $\Gamma \vdash \varphi $ is valid in $ \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}_{i}$ for each $i \in I$ . Then either $\Gamma \vdash _{\mathcal {B}} \varphi $ or $\Gamma \vdash _{\mathcal {L}_{i}} \emptyset $ for each $i \in I$ . But then either $\Gamma \vdash _{\mathcal {B}} \varphi $ or $\Gamma $ is an antitheorem of $\bigcap _{i \in I} \mathcal {L}_{i}$ .

Fact 3.9. $\bigvee _{i \in I} \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}_{i} = \bigcup _{i \in I} \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}_{i}$ .

Proof. This is an immediate consequence of Lemma 3.4.

Fact 3.10. Let $\mathcal {L}_{1} \leq \mathcal {L}_{2}$ . Then $\mathcal {L}_{1} \vee \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}_{2} = \mathcal {L}_{1} \cup \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}_{2}$ .

Proof. By Lemma 3.4, $\Gamma \vdash \varphi $ holds in $\mathcal {L}_{1} \vee \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}_{2}$ if and only if either $\Gamma \vdash _{\mathcal {L}_{1}} \varphi $ or there is some antitheorem $\Delta $ of $\mathcal {L}_{2}$ and some substitution $\sigma $ such that $\Gamma \vdash _{\mathcal {L}_{1}} \sigma (\delta )$ for each $\delta \in \Delta $ . But then $\mathcal {L}_{1} \leq \mathcal {L}_{2}$ implies that $\Gamma $ is an antitheorem of $\mathcal {L}_{2}$ , therefore $\Gamma \vdash \varphi $ holds in $ \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}_{2}$ .

Proof. The two maps are isotone and clearly $\mathcal {L}_{0} \vee \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L} \leq \mathcal {L}$ for $\mathcal {L}$ in $ \operatorname {\mathrm {Exp}} \operatorname {\mathrm {Ext}} \mathcal {L}_{0}$ . Conversely, if $\Gamma \vdash _{\mathcal {L}} \varphi $ for $\mathcal {L} \in \operatorname {\mathrm {Exp}} \operatorname {\mathrm {Ext}} \mathcal {L}_{0}$ , then either $\Gamma \vdash _{\mathcal {L}_{0}} \varphi $ or $\Gamma \vdash _{\mathcal {L}} \emptyset $ . In either case $\Gamma \vdash \varphi $ holds in $\mathcal {L}_{0} \vee \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}$ . Thus $\mathcal {L} = \mathcal {L}_{0} \vee \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}$ . Fact 3.10 now implies that $\mathcal {L} = \mathcal {L}_{0} \cup \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}$ for each $\mathcal {L} \in \operatorname {\mathrm {Exp}} \operatorname {\mathrm {Ext}} \mathcal {L}_{0}$ .

On the other hand, $\mathcal {L} \leq \operatorname {\mathrm {Exp}}_{\mathcal {B}} (\mathcal {L}_{0} \vee \mathcal {L})$ for $\mathcal {L} \in \operatorname {\mathrm {Exp}} \operatorname {\mathrm {Ext}} ( \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}_{0})$ . Conversely, if $\Gamma \vdash \varphi $ holds in $ \operatorname {\mathrm {Exp}}_{\mathcal {B}} (\mathcal {L}_{0} \vee \mathcal {L})$ for $\mathcal {L} \in \operatorname {\mathrm {Exp}} \operatorname {\mathrm {Ext}} ( \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}_{0})$ , then either $\Gamma \vdash _{\mathcal {B}} \varphi $ or $\Gamma \vdash \emptyset $ holds in $\mathcal {L}_{0} \vee \mathcal {L}$ . But $\mathcal {L}_{0} \vee \mathcal {L}$ is the extension of $\mathcal {L}_{0}$ by the explosive rules $\Gamma \vdash \emptyset $ valid in $\mathcal {L}$ , therefore $\Gamma \vdash _{\mathcal {L}_{0} \vee \mathcal {L}} \emptyset $ implies $\Gamma \vdash _{\mathcal {L}_{0}} \emptyset $ or $\Gamma \vdash _{\mathcal {L}} \emptyset $ . If $\Gamma \vdash \emptyset $ holds in $\mathcal {L}_{0}$ , then it holds in $ \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}_{0}$ , and therefore also in $\mathcal {L}$ . Thus $\Gamma \vdash _{\mathcal {B}} \varphi $ or $\Gamma \vdash _{\mathcal {L}} \emptyset $ . In either case $\Gamma \vdash _{\mathcal {L}} \varphi $ . Thus $ \operatorname {\mathrm {Exp}}_{\mathcal {B}} (\mathcal {L}_{0} \vee \mathcal {L}) = \mathcal {L}$ for $\mathcal {L} \in \operatorname {\mathrm {Exp}} \operatorname {\mathrm {Ext}} ( \operatorname {\mathrm {Exp}}_{\mathcal {B}} \mathcal {L}_{0})$ .

Proof. Clearly $\Gamma _{i}, \Delta _{j} \vdash _{\mathcal {L} \cap \mathcal {L}_{\mathrm {exp}}} \varphi _{i}$ for each $i \in I$ , $j \in J$ . Conversely, $\Gamma \vdash _{\mathcal {L}_{\mathrm {exp}}} \varphi $ implies that $\Gamma \vdash _{\mathcal {B}} \varphi $ or for some $\sigma $ and some $j \in J$ we have $\Gamma \vdash _{\mathcal {B}} \sigma (\delta _{j})$ for all $\delta _{j} \in \Delta _{j}$ , thus $\Gamma \vdash \varphi $ holds in the extension of $\mathcal {B}$ by the rules $\Gamma , \Delta _{j} \vdash \varphi $ if $\Gamma \vdash _{\mathcal {L}} \varphi $ . But the rule $\Gamma , \Delta _{j} \vdash \varphi $ can be derived from the rules $\Gamma _{i}, \Delta _{j} \vdash \varphi _{i}$ if $\Gamma \vdash _{\mathcal {L}} \varphi $ .

Proof. Clearly $ \operatorname {\mathrm {Mod}} \mathcal {L} \subseteq \operatorname {\mathrm {Mod}} (\mathcal {L} \cap \mathcal {L}_{\mathrm {exp}})$ and $ \operatorname {\mathrm {Mod}} \mathcal {L}_{\mathrm {exp}} \subseteq \operatorname {\mathrm {Mod}} (\mathcal {L} \cap \mathcal {L}_{\mathrm {exp}})$ . Conversely, suppose that a non-trivial matrix $\langle \boldsymbol {A}, F \rangle $ is a model of neither $\mathcal {L}$ nor $\mathcal {L}_{\mathrm {exp}}$ . Then there are rules $\Gamma \vdash \varphi $ and $\Delta \vdash \emptyset $ , without loss of generality variable disjoint, and valuations v and w on $\mathbb {A}$ such that $\Gamma \vdash _{\mathcal {L}} \varphi $ and $\Delta \vdash _{\mathcal {L}_{\mathrm {exp}}} \emptyset $ and moreover $v[\Gamma ] \subseteq F$ , $v(\varphi ) \notin F$ , and $w[\Delta ] \subseteq F$ . Any valuation u such that $u(p) = v(p)$ if p occurs in $\Gamma $ or $\varphi $ and $u(p) = w(p)$ if p occurs in $\Delta $ then witnesses that the rule $\Gamma , \Delta \vdash \varphi $ , which is valid in $\mathcal {L} \cap \mathcal {L}_{\mathrm {exp}}$ , fails in the matrix $\langle \boldsymbol {A}, F \rangle $ .

Proof. The right-to-left inclusion is clear. Conversely, suppose that $\Gamma \vdash \varphi $ holds in $ \operatorname {\mathrm {Log}} \prod _{i \in I} \mathbb {A}_{i}$ . If no valuation on $\mathbb {A}_{i}$ designates $\Gamma $ , then $\Gamma \vdash \varphi $ holds in $ \operatorname {\mathrm {Exp}}_{\mathcal {B}} \operatorname {\mathrm {Log}} \mathbb {A}_{i}$ . Otherwise, take a valuation $v_{i}$ on $\mathbb {A}_{i}$ which designates $\Gamma $ for each $i \in I$ . If there were some $j \in I$ such that $\Gamma \nvdash \varphi $ in $ \operatorname {\mathrm {Log}} \mathbb {A}_{j}$ , as witnessed by a valuation $w_{j}$ , then the product of the valuation $w_{j}$ with the valuations $v_{i}$ for $i \neq j$ would witness that $\Gamma \nvdash \varphi $ in $ \operatorname {\mathrm {Log}} \prod _{i \in I} \mathbb {A}_{i}$ . Thus $\Gamma \vdash \varphi $ in each $ \operatorname {\mathrm {Log}} \mathbb {A}_{i}$ .

Proof.

$$ \begin{align*} \qquad\quad\operatorname{\mathrm{Log}} (\mathsf{K} \times \mathbb{A}) & = \bigcap_{\mathbb{B} \in \mathsf{K}} \operatorname{\mathrm{Log}} \left( \mathbb{B} \times \mathbb{A} \right) \\ & = \bigcap_{\mathbb{B} \in \mathsf{K}} (\operatorname{\mathrm{Exp}}_{\mathcal{B}} \operatorname{\mathrm{Log}} \mathbb{B} \cup \operatorname{\mathrm{Exp}}_{\mathcal{B}} \operatorname{\mathrm{Log}} \mathbb{A} \cup (\operatorname{\mathrm{Log}} \mathbb{B} \cap \operatorname{\mathrm{Log}} \mathbb{A})) \\ & = \operatorname{\mathrm{Exp}}_{\mathcal{B}} \operatorname{\mathrm{Log}} \mathbb{B} \cup \left(\bigcap_{\mathbb{B} \in \mathsf{K}} (\operatorname{\mathrm{Exp}}_{\mathcal{B}} \operatorname{\mathrm{Log}} \mathbb{B} \cup \operatorname{\mathrm{Log}} \mathbb{A}) \cap \bigcap_{\mathbb{B} \in \mathsf{K}} \operatorname{\mathrm{Log}} \mathbb{B}\right) \\ & = \operatorname{\mathrm{Exp}}_{\mathcal{B}} \operatorname{\mathrm{Log}} \mathbb{A} \cup \left((\operatorname{\mathrm{Log}} \mathbb{A} \cup \bigcap_{\mathbb{B} \in \mathsf{K}} \operatorname{\mathrm{Exp}}_{\mathcal{B}} \operatorname{\mathrm{Log}} \mathbb{B}) \cap \bigcap_{\mathbb{B} \in \mathsf{K}} \operatorname{\mathrm{Log}} \mathbb{B}\right) \\ & = \operatorname{\mathrm{Exp}}_{\mathcal{B}} \operatorname{\mathrm{Log}} \mathbb{A} \cup \operatorname{\mathrm{Exp}}_{\mathcal{B}} \operatorname{\mathrm{Log}} \mathsf{K} \cup (\operatorname{\mathrm{Log}} \mathbb{A} \cap \operatorname{\mathrm{Log}} \mathsf{K}). \end{align*} $$

Proof. A rule $\Gamma \vdash \varphi $ holds in $ \operatorname {\mathrm {Log}} \prod _{i \in I} \mathbb {A}_{i}$ if and only if it either holds in each $\mathbb {A}_{i}$ or $\Gamma $ is an antitheorem of some $ \operatorname {\mathrm {Log}} \mathbb {A}_{i}$ . But $ \operatorname {\mathrm {Log}} \mathbb {A}_{i}$ is a non-trivial extension of $\mathcal {B}$ .

Fact 4.1. Let $\Gamma $ be a finite set of formulas. Then:

1. 1. $\Gamma ~{\vdash _{\mathcal {B}\mathcal {D}}}~\varphi $ if and only if $\bigwedge \Gamma \leq \varphi $ holds in all De Morgan algebras.

2. 2. $\Gamma ~{\vdash _{\mathcal {K}\mathcal {O}}}~\varphi $ if and only if $\bigwedge \Gamma \leq \varphi $ holds in all Kleene algebras.

3. 3. $\Gamma ~{\vdash _{\mathcal {C}\mathcal {L}}}~\varphi $ if and only if $\bigwedge \Gamma \leq \varphi $ holds in all Boolean algebras.

Fact 4.2. The logics $\mathcal {B}\mathcal {D}$ , $\mathcal {K}\mathcal {O}$ , and $\mathcal {C}\mathcal {L}$ enjoy the contraposition property:

$$ \begin{align*} \varphi \vdash_{\mathcal{L}} \psi ~ \implies ~ {-} \psi \vdash_{\mathcal{L}} {-} \varphi. \end{align*} $$

The logics $\mathcal {K}$ and $\mathcal {L}\mathcal {P}$ are related by contraposition as follows:

$$ \begin{align*} \varphi \vdash_{\mathcal{K}} \psi & ~ \implies ~ {-} \psi \vdash_{\mathcal{L}\mathcal{P}} {-} \varphi, & \varphi \vdash_{\mathcal{L}\mathcal{P}} \psi & ~ \implies ~ {-} \psi \vdash_{\mathcal{K}} {-} \varphi. \end{align*} $$

Fact 4.3. The logics $\mathcal {B}\mathcal {D}$ , $\mathcal {K}$ , $\mathcal {L}\mathcal {P}$ , $\mathcal {K}\mathcal {O}$ , and $\mathcal {C}\mathcal {L}$ enjoy the proof by cases property:

$$ \begin{align*} \Gamma, \varphi \vee \psi \vdash_{\mathcal{L}} \chi & \iff \Gamma, \varphi \vdash_{\mathcal{L}} \chi \text{ and } \Gamma, \psi \vdash_{\mathcal{L}} \chi. \end{align*} $$

Proof. The claim for $\mathcal {L}\mathcal {P}$ is equivalent to the fact that $\mathcal {L}\mathcal {P}$ is axiomatized by the law of the excluded middle relative to $\mathcal {B}\mathcal {D}$ . (For a direct semantic proof of the equivalence, see [Reference Přenosil38, proposition 3.5].) The claim for $\mathcal {K}$ then follows from the contraposition relation between $\mathcal {K}$ and $\mathcal {L}\mathcal {P}$ . Finally, the claim for $\mathcal {E}\mathcal {T}\mathcal {L}$ was proved by Pietz & Rivieccio [Reference Pietz and Rivieccio37, Lemma 3.2].

Proof. Since each formula is equivalent in $\mathcal {B}\mathcal {D}$ to a conjunction of disjunctive clauses, we may assume without loss of generality that each formula of $\Gamma $ is a disjunctive clause. If $\gamma \nvdash _{\mathcal {B}\mathcal {D}} \varphi $ for each $\gamma \in \Gamma $ , then each $\gamma \in \Gamma $ contains a literal which does not occur in $\varphi $ . The unique valuation on $\mathbb {BD}_{\boldsymbol {4}}$ which assigns an undesignated value to every literal which occurs in $\varphi $ and a designated value to every other literal then witnesses that $\Gamma \nvdash _{\mathcal {B}\mathcal {D}} \varphi $ .

Proof. If $\gamma \vdash _{\mathcal {L}\mathcal {P}} \emptyset $ , then $\gamma , \tau \vdash _{\mathcal {B}\mathcal {D}} \emptyset $ for some classical tautology $\tau $ by Proposition 4.6, so either $\gamma \vdash _{\mathcal {B}\mathcal {D}} \emptyset $ or $\tau \vdash _{\mathcal {B}\mathcal {D}} \emptyset $ by Proposition 4.7. But $\tau \nvdash _{\mathcal {B}\mathcal {D}} \emptyset $ because $\tau \nvdash _{\mathcal {C}\mathcal {L}} \emptyset $ .

Proof. If $\gamma \vdash _{\mathcal {E}\mathcal {T}\mathcal {L}} \emptyset $ , then $\gamma \vdash _{\mathcal {E}\mathcal {T}\mathcal {L}} {-} \gamma $ , so $\gamma \vdash _{\mathcal {B}\mathcal {D}} {-} \gamma $ by Proposition 4.6 and $\gamma \vdash _{\mathcal {E}\mathcal {C}\mathcal {Q}} \emptyset $ . Thus $ \operatorname {\mathrm {Exp}}_{\mathcal {B}\mathcal {D}} \mathcal {E}\mathcal {T}\mathcal {L} \leq \mathcal {E}\mathcal {C}\mathcal {Q}$ . Conversely, $\mathcal {E}\mathcal {C}\mathcal {Q} \leq \mathcal {E}\mathcal {T}\mathcal {L}$ .

Proof. The inclusion $\mathcal {E}\mathcal {C}\mathcal {Q}_{\omega } \leq \operatorname {\mathrm {Exp}}_{\mathcal {B}\mathcal {D}} \mathcal {C}\mathcal {L}$ is clear. Conversely, suppose that $\gamma \vdash _{\mathcal {C}\mathcal {L}} \emptyset $ . Let $\gamma _{1} \vee \dots \vee \gamma _{n}$ be a disjunction of conjunctive clauses which is equivalent $\gamma $ in $\mathcal {B}\mathcal {D}$ . Then $\gamma _{i} \vdash _{\mathcal {C}\mathcal {L}} \emptyset $ for each $\gamma _{i}$ by the proof by cases property. It follows that $\gamma _{i}$ is equivalent in $\mathcal {B}\mathcal {D}$ to $p_{i} \wedge {-} p_{i} \wedge \varphi _{i}$ for some atom $p_{i}$ and some formula $\varphi _{i}$ . Thus $\gamma \vdash _{\mathcal {B}\mathcal {D}} (p_{1} \wedge {-} p_{1}) \vee \dots \vee (p_{n} \wedge {-} p_{n})$ and $\gamma \vdash _{\mathcal {E}\mathcal {C}\mathcal {Q}_{\omega }} \emptyset $ .

Proof. This follows from the fact that $ \operatorname {\mathrm {Exp}}_{\mathcal {B}\mathcal {D}} \mathcal {C}\mathcal {L} = \mathcal {E}\mathcal {C}\mathcal {Q}_{\omega }$ by Lemma 3.4.

Proof. We first prove that $\mathcal {E}\mathcal {C}\mathcal {Q}_{\omega } \leq \mathcal {L}\mathcal {P} \vee \mathcal {E}\mathcal {C}\mathcal {Q}$ . It suffices to show that the rule $(p \wedge {-} p) \vee (q \wedge {-} q) \vee r \vdash (\varphi \wedge {-} \varphi ) \vee r$ is derivable in $\mathcal {L}\mathcal {P}$ for some $\varphi $ . In particular, let $\varphi = (p \vee q) \wedge ({-} p \vee {-} q)$ . Then $(\varphi \wedge {-} \varphi ) \vee r$ is equivalent to the conjunction of the formulas $p \vee q \vee r$ , $p \vee {-} q \vee r$ , ${-} p \vee q \vee r$ , ${-} p \vee {-} q \vee r$ , $p \vee {-} p \vee r$ , and $q \vee {-} q \vee r$ . But the last two formulas are theorems of $\mathcal {L}\mathcal {P}$ and the rest are derivable from $(p \wedge {-} p) \vee (q \wedge {-} q)$ in $\mathcal {B}\mathcal {D}$ .

It remains to prove that $\mathcal {E}\mathcal {C}\mathcal {Q}_{\omega } \leq (\mathcal {L}\mathcal {P} \cap \mathcal {E}\mathcal {C}\mathcal {Q}_{\omega }) \vee \mathcal {E}\mathcal {C}\mathcal {Q}$ . Consider a model $\mathbb {A}$ of $(\mathcal {L}\mathcal {P} \cap \mathcal {E}\mathcal {C}\mathcal {Q}_{\omega }) \vee \mathcal {E}\mathcal {C}\mathcal {Q}$ . Then $\mathbb {A}$ is a model of $\mathcal {E}\mathcal {C}\mathcal {Q}$ , as well as a model of either $\mathcal {L}\mathcal {P}$ or $\mathcal {E}\mathcal {C}\mathcal {Q}_{\omega }$ by Proposition 3.15. In the former case, $\mathbb {A}$ is still a model of $\mathcal {E}\mathcal {C}\mathcal {Q}_{\omega }$ because $\mathcal {E}\mathcal {C}\mathcal {Q}_{\omega } \leq \mathcal {L}\mathcal {P} \vee \mathcal {E}\mathcal {C}\mathcal {Q}$ .

Proof. This holds because $\mathcal {L}\mathcal {P} \vee \mathcal {E}\mathcal {C}\mathcal {Q} = \operatorname {\mathrm {Log}} \mathbb {B}_{\boldsymbol {2}} \times \mathbb {P}_{\boldsymbol {3}}$ and $(\mathcal {L}\mathcal {P} \vee \mathcal {E}\mathcal {C}\mathcal {Q}) \cap \mathcal {K} = (\mathcal {L}\mathcal {P} \cup \mathcal {E}\mathcal {C}\mathcal {Q}_{\omega }) \cap \mathcal {K} = (\mathcal {L}\mathcal {P} \cap \mathcal {K}) \cup (\mathcal {E}\mathcal {C}\mathcal {Q}_{\omega } \cap \mathcal {K}) = \mathcal {K}\mathcal {O} \cup \mathcal {E}\mathcal {C}\mathcal {Q}_{\omega } = \mathcal {K}\mathcal {O} \vee \mathcal {E}\mathcal {C}\mathcal {Q}$ .

Proof. If $\mathcal {E}\mathcal {C}\mathcal {Q} \nleq \mathcal {L}$ , then $\mathcal {L}$ has a non-trivial reduced model $\langle \boldsymbol {A}, F \rangle $ such that $a \in F$ for some $a \leq {-} a$ . But then the three- or four-element submatrix $\mathsf {f} < a \leq {-} a < \mathsf {t}$ of $\langle \boldsymbol {A}, F \rangle $ is a model of $\mathcal {L}$ . In either case the Leibniz reduct of this submatrix is isomorphic to $\mathbb {P}_{\boldsymbol {3}}$ , therefore $\mathbb {P}_{\boldsymbol {3}}$ is a model of $\mathcal {L}$ and $\mathcal {L} \leq \mathcal {L}\mathcal {P}$ .

Proof. If $\mathcal {L}$ is an explosive extension of $\mathcal {B}\mathcal {D}$ such that $\mathcal {L} \leq \mathcal {L}\mathcal {P}$ , then $\mathcal {L} = \operatorname {\mathrm {Exp}}_{\mathcal {B}\mathcal {D}} \mathcal {L} \leq \operatorname {\mathrm {Exp}}_{\mathcal {B}\mathcal {D}} \mathcal {L}\mathcal {P} = \mathcal {B}\mathcal {D}$ .

Proof. This is a particular instance of Theorem 3.13.

Proof. Consider an extension $\mathcal {L}$ of $\mathcal {E}\mathcal {C}\mathcal {Q}$ by the explosive rules $\Gamma _{i} \vdash \emptyset $ for $i \in I$ . Intersecting with $\mathcal {L}\mathcal {P}$ yields a logic axiomatized by the rules $\Gamma _{i} \vdash p_{i} \vee {-} p_{i}$ for $i \in I$ , where the atom $p_{i}$ does not occur in $\Gamma _{i}$ by Proposition 3.14. (We rename the variables of $\Gamma $ if necessary.) But a matrix validates $\Gamma _{i} \vdash p_{i} \vee {-} p_{i}$ if and only if it validates either $\Gamma _{i} \vdash \emptyset $ or $\emptyset \vdash p_{i} \vee {-} p_{i}$ . Since $\mathcal {E}\mathcal {C}\mathcal {Q}$ is the smallest proper explosive extension of $\mathcal {B}\mathcal {D}$ , it follows that a matrix validates both $p, {-} p \vdash \emptyset $ and $\Gamma _{i} \vdash p_{i} \vee {-} p_{i}$ if and only if it validates either $\Gamma _{i} \vdash \emptyset $ or both $\emptyset \vdash p \vee {-} p$ and $p, {-} p \vdash \emptyset $ . But $\mathcal {L} \leq \mathcal {E}\mathcal {C}\mathcal {Q}_{\omega } \leq \mathcal {L}\mathcal {P} \vee \mathcal {E}\mathcal {C}\mathcal {Q}$ , therefore a matrix is a model of both $\mathcal {E}\mathcal {C}\mathcal {Q}$ and $\mathcal {L}\mathcal {P} \cap \mathcal {L}$ if and only if it is a model of $\mathcal {L}$ , i.e., $(\mathcal {L}\mathcal {P} \cap \mathcal {L}) \vee \mathcal {E}\mathcal {C}\mathcal {Q} = \mathcal {L}$ .

Proof. Right to left, it suffices to verify that the rule $\chi _{n} \vee q, {-} q \vee r \vdash r$ holds in $\mathbb {ETL}_{\boldsymbol {8}}$ for each $n \geq 1$ , where $\chi _{n} := (p_{1} \wedge {-} p_{1}) \vee \dots \vee (p_{n} \wedge {-} p_{n})$ . This is true because for each valuation v on $\mathbb {ETL}_{\boldsymbol {8}}$ we have $v(\chi _{n}) \leq \mathsf {a} \vee \mathsf {c}$ , so $v(\chi _{n} \vee q) = \mathsf {t}$ implies $v(q) \geq \mathsf {b}$ . But then $v({-} q) \leq \mathsf {c}$ , so $v({-} q \vee r) = \mathsf {t}$ implies $v(r) = \mathsf {t}$ .

Conversely, suppose that $\Gamma \vdash _{\mathcal {K}_{-}} \varphi $ . By finitarity, we may assume that $\Gamma = \{ \gamma \}$ . We first prove two auxiliary claims. Firstly, we show that if the left-to-right implication holds for each $\gamma \in \{ \delta _{1}, \delta _{2}, \delta _{3} \}$ , where

$$ \begin{align*} \delta_{1} & := \gamma_{2} \vee \gamma_{3}, & \delta_{2} & := \gamma_{3} \vee \gamma_{1}, & \delta_{3} & := \gamma_{1} \vee \gamma_{2}, \end{align*} $$

then it holds for $\gamma := \gamma _{1} \vee \gamma _{2} \vee \gamma _{3}$ . If the implication holds in these three cases, then we have formulas $\psi _{i}$ and classical contradictions $\chi _{i}$ for $1 \leq i \leq 3$ such that

$$ \begin{align*} \delta_{i} & \vdash_{\mathcal{B}\mathcal{D}} \chi_{i} \vee \psi_{i} & & \text{ and } & \delta_{i} & \vdash_{\mathcal{B}\mathcal{D}} {-} \psi_{i} \vee \varphi. \end{align*} $$

Observe that

$$ \begin{align*} \gamma_{1} & \vdash_{\mathcal{B}\mathcal{D}} \delta_{2} \vee \delta_{3}, & \gamma_{2} & \vdash_{\mathcal{B}\mathcal{D}} \delta_{3} \vee \delta_{1}, & \gamma_{3} & \vdash_{\mathcal{B}\mathcal{D}} \delta_{1} \vee \delta_{2}. \end{align*} $$

Now take

$$ \begin{align*} \psi & := (\psi_{1} \vee \psi_{2}) \wedge (\psi_{2} \vee \psi_{3}) \wedge (\psi_{3} \vee \psi_{1}), & \chi & := \chi_{1} \vee \chi_{2} \vee \chi_{3}. \end{align*} $$

Then

$$ \begin{align*} \gamma_{1} \vdash_{\mathcal{B}\mathcal{D}} \delta_{2} \wedge \delta_{3} \vdash_{\mathcal{B}\mathcal{D}} (\chi_{2} \vee \psi_{2}) \wedge (\chi_{3} \vee \psi_{3}) \vdash_{\mathcal{B}\mathcal{D}} \chi_{2} \vee \chi_{3} \vee (\psi_{2} \wedge \psi_{3}) \vdash_{\mathcal{B}\mathcal{D}} \chi \vee \psi, \end{align*} $$

and likewise $\gamma _{2} \vdash _{\mathcal {B}\mathcal {D}} \chi \vee \psi $ and $\gamma _{3} \vdash _{\mathcal {B}\mathcal {D}} \chi \vee \psi $ . Moreover,

$$ \begin{align*} \gamma_{1} \vdash_{\mathcal{B}\mathcal{D}} \delta_{2} \wedge \delta_{3} \vdash_{\mathcal{B}\mathcal{D}} ({-} \psi_{2} \wedge {-} \psi_{3}) \vee \varphi \vdash_{\mathcal{B}\mathcal{D}} {-} \psi \vee \varphi, \end{align*} $$

and likewise $\gamma _{2} \vdash _{\mathcal {B}\mathcal {D}} {-} \psi \vee \varphi $ and $\gamma _{3} \vdash _{\mathcal {B}\mathcal {D}} {-} \psi \vee \varphi $ . By the proof by cases property for $\mathcal {B}\mathcal {D}$ (Fact 4.3) we have

$$ \begin{align*} \gamma_{1} \vee \gamma_{2} \vee \gamma_{3} & \vdash_{\mathcal{B}\mathcal{D}} \chi \vee \psi & & \text{ and } & \gamma_{1} \vee \gamma_{2} \vee \gamma_{3} & \vdash_{\mathcal{B}\mathcal{D}} {-} \psi \vee \varphi, \end{align*} $$

therefore the implication holds for $\gamma := \gamma _{1} \vee \gamma _{2} \vee \gamma _{3}$ .

Secondly, we show that if the left-to-right implication holds for $\varphi _{1}$ and $\varphi _{2}$ , then it holds for $\varphi := \varphi _{1} \wedge \varphi _{2}$ . The assumption yields formulas $\psi _{1}, \psi _{2}$ and contradictions $\chi _{1}$ , $\chi _{2}$ such that

$$ \begin{align*} \gamma & \vdash_{\mathcal{B}\mathcal{D}} \chi_{i} \vee \psi_{i} & & \text{ and } & \gamma & \vdash_{\mathcal{B}\mathcal{D}} {-} \psi_{i} \vee \varphi_{i}. \end{align*} $$

But then taking $\chi := \chi _{1} \vee \chi _{2}$ and $\psi := \psi _{1} \wedge \psi _{2}$ yields that

$$ \begin{align*} \gamma & \vdash_{\mathcal{B}\mathcal{D}} \chi \vee \psi & & \text{ and } & \gamma & \vdash_{\mathcal{B}\mathcal{D}} {-} \psi \vee \varphi. \end{align*} $$

We now prove the left-to-right implication for arbitrary $\gamma $ using these two auxiliary claims. By the first claim, it suffices to prove the implication for $\gamma := \gamma _{1} \vee \gamma _{2}$ , where $\gamma _{1}$ and $\gamma _{2}$ are conjunctive clauses. By the second claim, it suffices to prove the implication under the assumption that $\varphi $ is a disjunctive clause.

If $\gamma $ is a classical contradiction, the implication holds trivially for $\chi := \gamma $ and $\psi := {-} \gamma $ . Otherwise, we may suppose that without loss of generality the conjunctive clause $\gamma _{2}$ is not a classical contradiction.

Suppose now that the right-hand side of the implication fails and $\gamma _{1}$ is not a classical contradiction. Taking $\psi := \gamma $ , either $\gamma _{1} \nvdash _{\mathcal {B}\mathcal {D}} {-} \gamma \vee \varphi $ or $\gamma _{2} \nvdash _{\mathcal {B}\mathcal {D}} {-} \gamma \vee \varphi $ . In particular, either $\gamma _{1} \nvdash _{\mathcal {B}\mathcal {D}} \varphi $ or $\gamma _{2} \nvdash _{\mathcal {B}\mathcal {D}} \varphi $ . Suppose without loss of generality that $\gamma _{2} \nvdash _{\mathcal {B}\mathcal {D}} \varphi $ . Then $\gamma _{2}$ has no literal in common with $\varphi $ , therefore there is a valuation v on $\mathbb {ETL}_{\boldsymbol {8}}$ such that $v(l) = \mathsf {t}$ for each literal l of $\gamma _{2}$ while $v(l) \in \{ \mathsf {f}, \mathsf {b}, \mathsf {c} \}$ for each literal l of $\varphi $ . This valuation v witnesses that $\gamma \nvdash _{\mathcal {K}_{-}} \varphi $ .

On the other hand, suppose that the right-hand side of the implication fails and $\gamma _{1}$ is a classical contradiction. Taking $\chi := \gamma _{1}$ and $\psi := \gamma _{2}$ , either $\gamma _{1} \nvdash _{\mathcal {B}\mathcal {D}} {-} \gamma _{2} \vee \varphi $ or $\gamma _{2} \nvdash _{\mathcal {B}\mathcal {D}} {-} \gamma _{2} \vee \varphi $ . The latter case, where $\gamma _{2} \nvdash _{\mathcal {B}\mathcal {D}} \varphi $ , has already been dealt with. Suppose therefore that $\gamma _{1} \nvdash _{\mathcal {B}\mathcal {D}} {-} \gamma _{2} \vee \varphi $ .

Now consider the following valuation v on $\mathbb {ETL}_{\boldsymbol {8}}$ . If p and ${-} p$ are both literals of $\gamma _{1}$ , take $v(p) := \mathsf {a}$ . If p but not ${-} p$ is a literal of $\gamma _{1}$ , take $v(p) := \mathsf {t}$ , while if ${-} p$ but not p is a literal of $\gamma _{1}$ , take $v(p) := \mathsf {f}$ . For atoms such that neither p nor ${-} p$ is a literal of $\gamma _{1}$ , take $v(p) := \mathsf {b}$ if p is a literal of $\gamma _{2}$ and $v(p) := \mathsf {c}$ if ${-} p$ is a literal of $\gamma _{2}$ . (These two subcases are mutually exclusive, since $\gamma _{2}$ is not a classical contradiction.) For other atoms p take arbitrary $v(p) \in \{ \mathsf {b}, \mathsf {c} \}$ .

We have $v(\gamma _{1}) = \mathsf {a}$ , since $\gamma _{1}$ contains both p and ${-} p$ for some atom p. Moreover, $v(\gamma _{2}) \in \{ \mathsf {t}, \mathsf {b} \}$ , since $\gamma _{2}$ is a conjunction of literals l with ${v(l) \in \{ \mathsf {t}, \mathsf {b} \}}$ : if l is a literal of both $\gamma _{1}$ and $\gamma _{2}$ , then ${-} l$ is not a literal of $\gamma _{1}$ , since $\gamma _{1} \nvdash _{\mathcal {B}\mathcal {D}} {-} \gamma _{2}$ . Thus $v(\gamma ) = v(\gamma _{1} \vee \gamma _{2}) = \mathsf {t}$ . But $v(\varphi ) \in \{ \mathsf {f}, \mathsf {b}, \mathsf {c} \}$ because all literals take values in $\{ \mathsf {f}, \mathsf {b}, \mathsf {c}, \mathsf {t} \}$ and no literal of $\varphi $ takes the value $\mathsf {t}$ because $\gamma _{1} \nvdash _{\mathcal {B}\mathcal {D}} \varphi $ , so $\gamma \nvdash _{\mathcal {K}_{-}} \varphi $ .

Fact 5.17. $\mathcal {E}\mathcal {T}\mathcal {L}_{n+1} < \mathcal {E}\mathcal {D}\mathcal {S}_{n}$ .

Proof. We have $\chi _{n+1} \vdash _{\mathcal {B}\mathcal {D}} \chi _{n} \vee p_{n+1}$ and $\chi _{n+1} \vdash _{\mathcal {B}\mathcal {D}} {-} p_{n+1} \vee \chi _{n}$ , hence $\chi _{n+1} \vdash _{\mathcal {E}\mathcal {D}\mathcal {S}_{n}} \chi _{n}$ . But $\mathcal {E}\mathcal {T}\mathcal {L}_{n} \leq \mathcal {E}\mathcal {D}\mathcal {S}_{n}$ , so $\chi _{n+1} \vdash _{\mathcal {E}\mathcal {D}\mathcal {S}_{n}} \emptyset $ . On the other hand, $\mathcal {E}\mathcal {D}\mathcal {S}_{1} \nleq \mathcal {E}\mathcal {T}\mathcal {L}_{\omega }$ because $\chi _{n} \vee q, {-} q \vee r$ is not a classical contradiction.

Proof. Suppose that $\Gamma \vdash _{\mathcal {L}\mathcal {P} \cap \mathcal {E}\mathcal {T}\mathcal {L}} \varphi $ and $\Gamma \nvdash _{\mathcal {B}\mathcal {D}} \varphi $ . In $\mathcal {B}\mathcal {D}$ the formula $\varphi $ is equivalent to a conjunction of disjunctive clauses $\varphi _{i}$ for $i \in I$ . Then $\Gamma , \tau \vdash _{\mathcal {B}\mathcal {D}} \varphi $ for some classical tautology $\tau $ by Proposition 4.6. But $\Gamma \nvdash _{\mathcal {B}\mathcal {D}} \varphi $ , so ${\tau \vdash _{\mathcal {B}\mathcal {D}} \varphi _{i}}$ by Proposition 4.7. Each $\varphi _{i}$ is thus a tautology, hence it is equivalent to $q_{i} \vee {-} q_{i} \vee \psi _{i}$ for some atom $q_{i}$ and some formula $\psi _{i}$ . By Proposition 4.6, $\Gamma \vdash _{\mathcal {E}\mathcal {T}\mathcal {L}} \varphi $ implies that $\Gamma \vdash _{\mathcal {B}\mathcal {D}} \delta $ and $\Gamma \vdash _{\mathcal {B}\mathcal {D}} {-} \delta \vee q \vee {-} q \vee \psi _{i}$ for some $\delta $ . The rule $p, {-} p \vee q \vee {-} q \vee r \vdash q \vee {-} q \vee r$ then suffices to derive $\varphi _{i}$ from $\Gamma $ . The equivalence of this rule and the rule $p, {-} p \vee q \vee {-} q \vdash q \vee {-} q$ follows from the fact that in any De Morgan algebra, the elements of the form $q \vee {-} q \vee r$ are precisely the elements of the form $q \vee {-} q$ . Finally, we can derive $\varphi $ from the set of formulas $\{ \varphi _{i} \mid i \in I \}$ in $\mathcal {B}\mathcal {D}$ .

Proof. Suppose that $\Gamma \vdash _{\mathcal {K}\mathcal {O}_{-}} \varphi $ and $\Gamma \nvdash _{\mathcal {B}\mathcal {D}} \varphi $ . We may assume that $\varphi $ is a disjunctive clause, as in the proof of Proposition 5.19. Then $\Gamma , \tau \vdash _{\mathcal {B}\mathcal {D}} \varphi $ for some tautology $\tau $ by Proposition 4.6, hence $\tau \vdash _{\mathcal {B}\mathcal {D}} \varphi $ by Proposition 4.7. It follows that $\varphi $ is equivalent to $r \vee {-} r \vee \alpha $ for some atom r and some formula $\alpha $ . Then $\Gamma \vdash _{\mathcal {K}_{-}} \varphi $ implies that $\Gamma \vdash _{\mathcal {B}\mathcal {D}} \chi \vee \psi $ and $\Gamma \vdash _{\mathcal {B}\mathcal {D}} {-} \psi \vee r \vee {-} r \vee \alpha $ for some formula $\psi $ and some contradiction $\chi $ by Proposition 5.16. The formula $\varphi $ is thus derivable from $\Gamma $ in the extension of $\mathcal {B}\mathcal {D}$ by the rules $\chi _{n} \vee q, {-} q \vee r \vee {-} r \vee s \vdash r \vee {-} r \vee s$ for $n \in \omega $ . But these rules are derivable from the simpler rules $\chi _{n} \vee q, {-} q \vee r \vee {-} r \vdash r \vee {-} r$ , as in the proof of Proposition 5.19.

Proof. By Fact 3.10 we have $(\mathcal {L}\mathcal {P} \cap \mathcal {E}\mathcal {T}\mathcal {L}) \vee \mathcal {E}\mathcal {C}\mathcal {Q} = (\mathcal {L}\mathcal {P} \cap \mathcal {E}\mathcal {T}\mathcal {L}) \vee \operatorname {\mathrm {Exp}} \mathcal {E}\mathcal {T}\mathcal {L} = (\mathcal {L}\mathcal {P} \cap \mathcal {E}\mathcal {T}\mathcal {L}) \cup \operatorname {\mathrm {Exp}} \mathcal {E}\mathcal {T}\mathcal {L} = (\mathcal {L}\mathcal {P} \cap \mathcal {E}\mathcal {T}\mathcal {L}) \cup \mathcal {E}\mathcal {C}\mathcal {Q}$ and $(\mathcal {L}\mathcal {P} \vee \mathcal {E}\mathcal {C}\mathcal {Q}) \cap \mathcal {E}\mathcal {T}\mathcal {L} = (\mathcal {L}\mathcal {P} \cup \mathcal {E}\mathcal {C}\mathcal {Q}_{\omega }) \cap \mathcal {E}\mathcal {T}\mathcal {L} = (\mathcal {L}\mathcal {P} \cap \mathcal {E}\mathcal {T}\mathcal {L}) \cup (\mathcal {E}\mathcal {C}\mathcal {Q}_{\omega } \cap \mathcal {E}\mathcal {T}\mathcal {L})$ . It therefore suffices to find $\Gamma $ and $\varphi $ such that $\Gamma \vdash _{\mathcal {E}\mathcal {C}\mathcal {Q}_{\omega } \cap \mathcal {E}\mathcal {T}\mathcal {L}} \varphi $ but $\Gamma \nvdash _{\mathcal {E}\mathcal {C}\mathcal {Q}} \varphi $ and $\Gamma \nvdash _{\mathcal {L}\mathcal {P}} \varphi $ .

The rule $(p_1 \wedge {-} p_1) \vee (p_2 \wedge {-} p_2), q, {-} q \vee r \vdash r$ holds in $\mathcal {E}\mathcal {C}\mathcal {Q}_{\omega } \cap \mathcal {E}\mathcal {T}\mathcal {L}$ but not in $\mathcal {L}\mathcal {P} = \operatorname {\mathrm {Log}} \mathbb {P}_{\boldsymbol {3}}$ . Moreover, $\mathcal {E}\mathcal {C}\mathcal {Q} = \operatorname {\mathrm {Log}} \mathbb {ETL}_{\boldsymbol {4}} \times \mathbb {BD}_{\boldsymbol {4}}$ and there is a valuation on $\mathbb {ETL}_{\boldsymbol {4}} \times \mathbb {BD}_{\boldsymbol {4}}$ which designates $(p_1 \wedge {-} p_1) \vee (p_2 \wedge {-} p_2)$ , therefore the rule in question holds in $\mathcal {E}\mathcal {C}\mathcal {Q}$ only if $q, {-} q \vee r \vdash _{\mathcal {E}\mathcal {C}\mathcal {Q}} r$ . But $q, {-} q \vee r \nvdash _{\mathcal {E}\mathcal {C}\mathcal {Q}} r$ .

Proof. Suppose that $\mathcal {L}\mathcal {P} \cap \mathcal {E}\mathcal {C}\mathcal {Q} \nleq \mathcal {L}$ . Then $p \wedge {-} p \nvdash _{\mathcal {L}} q \vee {-} q$ , so $\mathcal {L}$ has a reduced model $\langle \boldsymbol {A}, F \rangle $ with $a \in F$ and $b \notin F$ such that $a \leq {-} a$ and ${-} b \leq b$ . The congruence $\theta (a, {-} a)$ is compatible with F: if $x \in F$ and $\langle x, y \rangle \in \theta (a, {-} a)$ , then $x \wedge a = y \wedge a$ by the above description of principal congruences on De Morgan algebras. Since $x \wedge a \in F$ , we have $y \in F$ . Since the matrix $\langle \boldsymbol {A}, F \rangle $ is reduced, the congruence $\theta (a, {-} a)$ is the identity relation, therefore $a = {-} a$ .

Consider the submatrix $\langle \boldsymbol {B}, G \rangle $ of $\langle \boldsymbol {A}, F \rangle $ generated by a and $c = (a \wedge b) \vee {-} b$ . Note that $c = {-} c = (a \vee {-} b) \wedge b$ . The elements a and c are distinct, since $a \in F$ but $c \notin F$ (because $b \notin F$ ). The universe of $\boldsymbol {B}$ is the set $\{ \mathsf {f}, a \wedge c, a, c, a \vee c, \mathsf {t} \}$ and $G := F \cap \boldsymbol {B} = \{ a, a \vee c, \mathsf {t} \}$ . The congruence $\theta (a \vee c, \mathsf {t})$ is compatible with G and the matrix $\langle \boldsymbol {B} / \theta (a \vee c, \mathsf {t}), G / \theta (a \vee c, \mathsf {t}) \rangle $ is isomorphic to $\mathbb {BD}_{\boldsymbol {4}}$ . Therefore $\mathbb {BD}_{\boldsymbol {4}}$ is a model of $\mathcal {L}$ and $\mathcal {L} \leq \mathcal {B}\mathcal {D}$ .

Proof. If $\mathcal {L}$ is a non-trivial extension of $\mathcal {B}\mathcal {D}$ , then it has a non-trivial reduced model $\langle \boldsymbol {A}, F \rangle $ . Then $\mathsf {t} \in F$ and $\mathsf {f} \notin F$ , so the submatrix of $\langle \boldsymbol {A}, F \rangle $ with the universe $\{ \mathsf {f}, \mathsf {t} \}$ is isomorphic to $\mathbb {B}_{\boldsymbol {2}}$ . Therefore $\mathbb {B}_{\boldsymbol {2}}$ is a model of $\mathcal {L}$ and $\mathcal {L} \leq \mathcal {C}\mathcal {L}$ .

Proof. Suppose that $\mathcal {L}\mathcal {P} \nleq \mathcal {L}$ . Then $\emptyset \nvdash _{\mathcal {L}} p \vee {-} p$ , so $\mathcal {L}$ has a reduced model $\langle \boldsymbol {A}, F \rangle $ such that $a \notin F$ for some $a \in \boldsymbol {A}$ such that ${-} a \leq a$ . Consider the submatrix $\langle \boldsymbol {B}, G \rangle $ of $\langle \boldsymbol {A}, F \rangle $ generated by a. The universe of $\boldsymbol {B}$ is the set $\{ \mathsf {f}, {-} a, a, \mathsf {t}\}$ and $G := F \cap \boldsymbol {A} = \{ \mathsf {t} \}$ . The congruence $\theta ({-} a, a)$ on $\boldsymbol {B}$ is compatible with G and the matrix $\langle \boldsymbol {B} / \theta ({-} a, a), G / \theta ({-} a, a) \rangle $ is isomorphic to $\mathbb {K}_{\boldsymbol {3}}$ . Therefore $\mathbb {K}_{\boldsymbol {3}}$ is a model of $\mathcal {L}$ and $\mathcal {L} \leq \mathcal {K}$ .

The claim that $\mathcal {L}\mathcal {P}$ and $\mathcal {C}\mathcal {L}$ have the same theorems was proved by Priest [Reference Priest39]. To prove that $\mathcal {K}$ and $\mathcal {B}\mathcal {D}$ also have the same theorems, recall the contrapositive relation between $\mathcal {K}$ and $\mathcal {L}\mathcal {P}$ : $\emptyset \vdash _{\mathcal {K}} \varphi $ implies ${-} \varphi \vdash _{\mathcal {L}\mathcal {P}} \emptyset $ . But $ \operatorname {\mathrm {Exp}}_{\mathcal {B}\mathcal {D}} \mathcal {L}\mathcal {P} = \mathcal {B}\mathcal {D}$ , so ${-} \varphi \vdash _{\mathcal {B}\mathcal {D}} \emptyset $ , and by contraposition $\emptyset \vdash _{\mathcal {B}\mathcal {D}} \varphi $ .

Proof. Suppose that $\mathcal {E}\mathcal {T}\mathcal {L} \nleq \mathcal {L}$ . Then $p, {-} p \vee q \nvdash _{\mathcal {L}} q$ and $\mathcal {L}$ has a reduced model $\langle \boldsymbol {A}, F \rangle $ such that $a \in F$ and ${-} a \vee b \in F$ but $b \notin F$ for some $a, b \in \boldsymbol {A}$ . Without loss of generality we may take $b := a \wedge b$ and $a := a \wedge ({-} a \vee b)$ , i.e., we may assume that $b \leq a$ and $a \leq {-} a \vee b$ .

Consider the submatrix $\langle \boldsymbol {B}, G \rangle $ of $\langle \boldsymbol {A}, F \rangle $ generated by a and b. Let $\boldsymbol {C}$ be the algebra shown in Figure 4. By Lemma 6.6 there is a homomorphism $h\colon \boldsymbol {C} \rightarrow \boldsymbol {B}$ . Take $H := h^{-1}[G]$ . Then the matrix $\langle \boldsymbol {C}, H \rangle $ is a model of $\mathcal {L}$ , being an strict homomorphic preimage of a model of $\mathcal {L}$ . We have $a \in H$ and $b \notin H$ .

We distinguish two cases. If $a \wedge {-} a \notin H$ , then $H = \{ a, a \vee {-} a, b \vee {-} b, \mathsf {t} \}$ , hence $\theta (a, a \vee {-} a)$ is compatible with H and the matrix $\langle \boldsymbol {C} / \theta (a, a \vee {-} a), H / \theta (a, a \vee {-} a) \rangle $ is isomorphic to $\mathbb {P}_{\boldsymbol {3}} \times \mathbb {B}_{\boldsymbol {2}}$ . On the other hand, if $a \wedge {-} a \in H$ , then $H = \{ a, a \vee {-} a, b \vee {-} b, \mathsf {t}, a \wedge {-} a, {-} a, {-} b \}$ , hence $\theta (a \wedge {-} a, \mathsf {t})$ is compatible with H and the matrix $\langle \boldsymbol {C} / \theta (a \wedge {-} a, \mathsf {t}), H / \theta (a \wedge {-} a, \mathsf {t}) \rangle $ is isomorphic to $\mathbb {P}_{\boldsymbol {3}}$ . Thus either $\mathbb {P}_{\boldsymbol {3}} \times \mathbb {B}_{\boldsymbol {2}}$ is a model of $\mathcal {L}$ and $\mathcal {L} \leq \mathcal {L}\mathcal {P} \vee \mathcal {E}\mathcal {C}\mathcal {Q}$ , or $\mathbb {P}_{\boldsymbol {3}}$ is a model of $\mathcal {L}$ and $\mathcal {L} \leq \mathcal {L}\mathcal {P} \leq \mathcal {L}\mathcal {P} \vee \mathcal {E}\mathcal {C}\mathcal {Q}$ .

Proof. If $\mathcal {L}\mathcal {P} \nleq \mathcal {L}_{1}$ and $\mathcal {L}\mathcal {P} \nleq \mathcal {L}_{2}$ , then $\mathcal {L}_{1} \vee \mathcal {L}_{2} \leq \mathcal {K}$ . Likewise, if $\mathcal {E}\mathcal {T}\mathcal {L} \nleq \mathcal {L}_{1}$ and $\mathcal {E}\mathcal {T}\mathcal {L} \nleq \mathcal {L}_{2}$ , then $\mathcal {L}_{1} \vee \mathcal {L}_{2} \leq \mathcal {L}\mathcal {P} \vee \mathcal {E}\mathcal {C}\mathcal {Q}$ . But if $\mathcal {L}\mathcal {P} \leq \mathcal {L}_{1}$ and $\mathcal {E}\mathcal {T}\mathcal {L} \leq \mathcal {L}_{1}$ , then $\mathcal {C}\mathcal {L} \leq \mathcal {L}_{1}$ , and likewise for $\mathcal {L}_{2}$ .