Proof. Condition (i) is straightforward. Hence we detail only the proof of (ii).

It is well-known that

$$ \begin{align*} \textrm{Fg}_{\vdash}^{\boldsymbol{A}}(X) = \bigcup_{\alpha < \lambda^{+}}V_{\alpha}, \end{align*} $$

where the various $V_{\alpha }$ are defined in the following way. First we set $V_{0} := X$ , and at limit ordinals we take unions. At successor ordinals we proceed as follows. If $\alpha < \lambda $ , then

$$ \begin{align*} V_{\alpha+1} := V_{\alpha} \cup \{ & c \in C \colon c = f(\varphi)\text{ for some homomorphism }f \colon \boldsymbol{Fm}(\kappa) \to \boldsymbol{A} \\ &\text{and }\varGamma \cup \{ \varphi \} \subseteq Fm(\kappa) \text{ such that }\varGamma \vdash \varphi \text{ and } v[\varGamma] \subseteq V_{\alpha}\}. \end{align*} $$

We claim that for every $\alpha < \lambda ^{+}$ and $b \in V_{\alpha }$ , there is an algebra $\boldsymbol {B}[b, \alpha ] \leqslant \boldsymbol {A}$ such that $\vert B[b, \alpha ] \vert \leqslant \lambda $ , $Z \subseteq B[b, \alpha ]$ , and $b \in \textrm {Fg}_{\vdash }^{\boldsymbol {B}[b, \alpha ]}(X \cap B[b, \alpha ])$ . To prove this, we reason by induction on $\alpha \leqslant \lambda ^{+}$ . In the case where $\alpha = 0$ we take the subalgebra of $\boldsymbol {A}$ generated by $X \cup Z$ . If $\alpha $ is a limit ordinal and $b \in V_{\alpha }$ , then $b \in V_{\beta }$ for some $\beta < \alpha $ . Therefore, with an application of the inductive hypothesis, we are done.

Then we consider the case where $\alpha = \beta +1$ . Since $b \in V_{\beta + 1}$ , there are a homomorphism $f \colon \boldsymbol {Fm}(\kappa ) \to \boldsymbol {A}$ and $\varGamma \cup \{ \varphi \} \subseteq Fm(\kappa )$ such that $\varGamma \vdash \varphi $ , $b = f(\varphi )$ , and $v[\varGamma ] \subseteq V_{\beta }$ . Now, for every $\gamma \in \varGamma $ , we consider the algebra $\boldsymbol {B}[ \kern 0.4pt f(\gamma ), \beta ]$ given by the inductive hypothesis. Let $\boldsymbol {B}[b, \alpha ]$ be the subalgebra of $\boldsymbol {A}$ generated by

$$ \begin{align*} Z \cup f[Fm(\kappa)] \cup \bigcup_{\gamma \in \varGamma} B[\kern 0.4pt f(\gamma), \beta ]. \end{align*} $$

The fact that $\vert Z \vert + \vert Fm(\kappa ) \vert \leqslant \lambda $ , and that $\vert B[\kern 0.4pt f(\gamma ), \beta ] \vert \leqslant \lambda $ for every $\gamma \in \varGamma $ ensures that $\vert B[b, \alpha ] \vert \leqslant \lambda $ .

It only remains to show that $b \in \textrm {Fg}_{\vdash }^{\boldsymbol {B}[b, \alpha ]}(X \cap B[b, \alpha ])$ . To this end, consider $\gamma \in \varGamma $ . By the inductive hypothesis and condition (i) we obtain

(1) $$ \begin{align} f(\gamma) \in \textrm{Fg}_{\vdash}^{\boldsymbol{B}[\kern 0.4pt f(\gamma), \beta]}(X \cap B[\kern 0.4pt f(\gamma), \beta]) \subseteq \textrm{Fg}_{\vdash}^{\boldsymbol{B}[b, \alpha]}(X \cap B[b, \alpha]). \end{align} $$

Since $f[Fm(\kappa )] \subseteq B[b, \alpha ]$ , the homomorphism $f \colon \boldsymbol {Fm}(\kappa ) \to \boldsymbol {B}[b, \alpha ]$ is well defined. Together with the fact that $\varGamma \vdash \varphi $ and that $f[\varGamma ] \subseteq \textrm {Fg}_{\vdash }^{\boldsymbol {B}[b, \alpha ]}(X \cap B[b, \alpha ])$ by (1), this implies that $b = f(\varphi ) \in \textrm {Fg}_{\vdash }^{\boldsymbol {B}[b, \alpha ]}(X \cap B[b, \alpha ])$ , as desired. This establishes the claim.

Together with the fact that $\textrm {Fg}_{\vdash }^{\boldsymbol {A}}(X) = \bigcup _{\alpha < \lambda ^{+}}V_{\alpha }$ , the claim concludes the proof.⊣

Proof. See [Reference Czelakowski11, Theorem 5.3].⊣

Proof. Under the assumption that the cardinality of the language of a class of matrices $\mathsf {K}$ is $\leqslant \kappa $ , the proof of the equality $\mathbb {S}\mathbb {P}_{\!{\scriptstyle \textrm {R}}_{\kappa ^{+}}}^{}(\mathsf {K}) = \mathbb {U}_{\kappa }\mathbb {S}\mathbb {P}(\mathsf {K})$ is routinary.⊣

Proof. Immediate from Lemma 2.3 and Theorem 2.4.⊣

Proof. See [Reference Font15, Theorems 6.17 and 6.60].⊣

Proof. This result is essentially [Reference Raftery46, Theorem 5.6].⊣

Proof. Suppose, with a view to contradiction, that there is a matrix $\langle \boldsymbol {A}, F \rangle \in \mathbb {U}_{\lambda }(\mathsf {Mod}^{\equiv }(\vdash ))$ such that $\langle \boldsymbol {A}, F \rangle \notin \mathsf {Mod}^{\equiv }(\vdash )$ . First observe that $\langle \boldsymbol {A}, F \rangle $ is a model of $\vdash $ , since $\lambda \geqslant \kappa $ and $\vdash $ is defined on $Fm(\kappa )$ . Then the congruence is not the identity relation. Together with Proposition 2.2(ii), this implies that there are two different $a, b \in A$ such that for every $\varphi (x, \vec {y}) \in Fm(\omega )$ , and every tuple $\vec {c} \in A$ ,

(2) $$ \begin{align} \textrm{Fg}_{\vdash}^{\boldsymbol{A}}(F, \varphi(a, \vec{c})) = \textrm{Fg}_{\vdash}(F, \varphi^{\boldsymbol{A}}(b, \vec{c})). \end{align} $$

We define a chain (under the subalgebra relation) $\langle \boldsymbol {B}_{\alpha } \colon \alpha < \lambda \rangle $ of subalgebras of $\boldsymbol {A}$ as follows. First we let $\boldsymbol {B}_{0}$ be the subalgebra of $\boldsymbol {A}$ generated by $\{ a, b \}$ . At limit ordinals we take unions. Now, suppose that $\boldsymbol {B}_{\alpha }$ has already been defined and that $\alpha < \lambda $ . Consider a formula $\varphi (x, \vec {y}) \in Fm(\omega )$ and a tuple $\vec {c} \in B_{\alpha }$ . By Lemma 2.1 and (2) there is a subalgebra $\boldsymbol {B}[\varphi , \vec {c}, \alpha ] \leqslant \boldsymbol {A}$ such that $\vert B[\varphi , \vec {c}, \alpha ] \vert \leqslant \lambda $ , $a, b, \vec {c} \in B[\varphi , \vec {c}]$ and

(3) $$ \begin{align} \textrm{Fg}_{\vdash}^{\boldsymbol{B}[\varphi, \vec{c}, \alpha]}(F \cap B[\varphi, \vec{c}, \alpha], \varphi(a, \vec{c})) = \textrm{Fg}_{\vdash}^{\boldsymbol{B}[\varphi, \vec{c}, \alpha]}(F \cap B[\varphi, \vec{c}, \alpha], \varphi(b, \vec{c})). \end{align} $$

Then we let $\boldsymbol {B}_{\alpha +1}^{\ast }$ be the subalgebra of $\boldsymbol {A}$ generated by the union of the various $B[\varphi , \vec {c}, \alpha ]$ , and $\boldsymbol {B}_{\alpha }$ the subalgebra of $\boldsymbol {A}$ generated by $B_{\alpha } \cup B_{\alpha +1}^{\ast }$ .

Now we set

$$ \begin{align*} \langle \boldsymbol{B}, G \rangle := \langle \bigcup_{\alpha < \lambda} \boldsymbol{B}_{\alpha}, F \cap \bigcup_{\alpha < \lambda}B_{\alpha} \rangle. \end{align*} $$

Bearing in mind that $\vert B[\varphi , \vec {c}, \alpha ] \vert + \vert Fm(\kappa ) \vert \leqslant \lambda $ , an easy induction shows that $\vert B_{\alpha } \vert \leqslant \lambda $ for every $\alpha < \lambda $ . As a consequence, we obtain that $\vert B \vert \leqslant \lambda $ and, therefore, that $\boldsymbol {B}$ is $\lambda $ -generated. Together with $\langle \boldsymbol {A}, F \rangle \in \mathbb {U}_{\lambda }(\mathsf {Mod}^{\equiv }(\vdash ))$ , this implies that $\langle \boldsymbol {B}, G \rangle \in \mathsf {Mod}^{\equiv }(\vdash )$ .

Now, the fact that $\langle \boldsymbol {B}, G \rangle \in \mathsf {Mod}^{\equiv }(\vdash )$ implies that is the identity relation and, therefore, that . By Lemma 2.2(ii) we can assume without loss of generality that there are a formula $\varphi (x, \vec {y}) \in Fm(\omega )$ and a tuple $\vec {c} \in B$ such that $\varphi (a, \vec {c}) \notin \textrm {Fg}_{\vdash }^{\boldsymbol {B}}(G, \varphi (b, \vec {c}))$ . Observe that there is $\alpha < \lambda $ such that $\vec {c} \in B_{\alpha }$ . By (3) and Lemma 2.1(i) we obtain that

$$ \begin{align*} \varphi(a, \vec{c}) &\in \textrm{Fg}_{\vdash}^{\boldsymbol{B}[\varphi, \vec{c}, \alpha]}(F \cap B[\varphi, \vec{c}, \alpha], \varphi(b, \vec{c}))\\ &= \textrm{Fg}_{\vdash}^{\boldsymbol{B}[\varphi, \vec{c}, \alpha]}(G \cap B[\varphi, \vec{c}, \alpha], \varphi(b, \vec{c}))\\ & \subseteq \textrm{Fg}_{\vdash}^{\boldsymbol{B}}(G, \varphi(b, \vec{c})). \end{align*} $$

But this contradicts the fact that $\varphi (a, \vec {c}) \notin \textrm {Fg}_{\vdash }^{\boldsymbol {B}}(G, \varphi (b, \vec {c}))$ . Hence we reached a contradiction, as desired.⊣

Proof. The “only if” part is immediate. The “if” one is a consequence of Lemma 2.3.⊣

Proof. The “if” part is immediate. To prove the “only if” part, suppose that there is an interpretation $\boldsymbol {\tau }$ of $\vdash $ into $\vdash '$ . We can assume without loss of generality that the sets of function symbols of $\vdash $ and $\vdash '$ are disjoint. Then let $\mathscr {L}$ be the language extending $\mathscr {L}_{\vdash '}$ with the symbols of $\vdash $ . Given a matrix $\langle \boldsymbol {A}, F \rangle \in \mathsf {Mod}^{\equiv }(\vdash ')$ , we denote by $\boldsymbol {A}_{\mathscr {L}}$ the $\mathscr {L}$ -algebra obtained by enriching $\boldsymbol {A}$ with the following interpretation of the n-ary symbols $\ast $ of $\vdash $ : for every $a_{1}, \dots , a_{n} \in A$ ,

$$ \begin{align*} \ast^{\boldsymbol{A}_{\mathscr{L}}}(a_{1}, \dots, a_{n}) := \boldsymbol{\tau}(\ast)^{\boldsymbol{A}}(a_{1}, \dots, a_{n}). \end{align*} $$

Then consider the class of matrices $\mathsf {K} := \{ \langle \boldsymbol {A}_{\mathscr {L}}, F \rangle \colon \langle \boldsymbol {A}, F \rangle \in \mathsf {Mod}^{\equiv }(\vdash ') \}$ , and let $\vdash ''$ be the logic on $Fm_{\mathscr {L}}(\kappa _{\vdash '})$ induced by $\mathsf {K}$ . It is not hard to see that $\mathsf {Mod}^{\equiv }(\vdash '') = \mathsf {K}$ . Together with the fact that $\boldsymbol {\tau }$ is an interpretation of $\vdash $ into $\vdash '$ , this implies that $\vdash ''$ is a compatible expansion of $\vdash $ . As it is clear that $\vdash '$ and $\vdash ''$ are term-equivalent, we are done.⊣

Proof. The “if” part follows from the fact that $\mathbb {S}(\mathsf {K}) \subseteq \mathsf {Mod}^{\equiv }(\vdash ')$ by Lemma 2.8.

To prove the “only if” part, suppose that $\langle \boldsymbol {A}^{\boldsymbol {\tau }}, F \rangle \in \mathsf {Mod}^{\equiv }(\vdash )$ for every $\langle \boldsymbol {A}, F \rangle \in \mathbb {S}(\mathsf {K})$ . By Lemmas 2.3 and 2.9 this yields that $\langle \boldsymbol {A}^{\boldsymbol {\tau }}, F \rangle \in \mathsf {Mod}^{\equiv }(\vdash )$ for every $\langle \boldsymbol {A}, F \rangle \in \mathbb {U}_{\kappa _{\vdash '}}\mathbb {P}_{\!{\scriptstyle \textrm {SD}}}^{}\mathbb {S}(\mathsf {K})$ . With an application of Lemma 2.8, we conclude that $\langle \boldsymbol {A}^{\boldsymbol {\tau }}, F \rangle \in \mathsf {Mod}^{\equiv }(\vdash )$ for every $\langle \boldsymbol {A}, F \rangle \in \mathsf {Mod}^{\equiv }(\vdash ')$ and, therefore, that $\boldsymbol {\tau }$ is an interpretation of $\vdash $ into $\vdash '$ .⊣

Proof. First we show that ${\bigotimes _{i \in I}{\vdash _{i}}}\leqslant {\vdash _{j}}$ for every $j \in I$ . To this end, consider the map $\boldsymbol {\tau }$ that sends every n-ary basic operation of $\bigotimes _{i \in I}{\vdash _{i}}$ to its j-th component (which is an n-ary term of $\vdash _{j}$ ). Consider $\langle \boldsymbol {A}, F \rangle \in \mathsf {Mod}^{\equiv }(\vdash _{j})$ . It is clear that $\langle \boldsymbol {A}^{\boldsymbol {\tau }}, F \rangle \cong \bigotimes _{i \in I}\langle \boldsymbol {A}_{i}, F_{i}\rangle $ where $\langle \boldsymbol {A}_{i}, F_{i}\rangle $ is the trivial $\mathscr {L}_{i}$ -matrix for every $i \in I \smallsetminus \{ j \}$ , and $\langle \boldsymbol {A}_{j}, F_{j} \rangle := \langle \boldsymbol {A}, F \rangle $ . By Proposition 4.5 we have

$$ \begin{align*} \langle \boldsymbol{A}^{\boldsymbol{\tau}}, F \rangle \, \cong\, \bigotimes_{i \in I}\langle \boldsymbol{A}_{i}, F_{i}\rangle \in \bigotimes_{i \in I}\mathsf{Mod}^{\equiv}(\vdash_{i}) \subseteq \mathsf{Mod}^{\equiv}(\bigotimes_{i \in I}{\vdash_{i}}). \end{align*} $$

In particular, this means that $\boldsymbol {\tau }$ is an interpretation of $\bigotimes _{i \in I}{\vdash _{i}}$ into $\vdash _{j}$ , thus $\bigotimes _{i \in I}{\vdash _{i}} \leqslant {\vdash _{j}}$ . As a consequence, $[\kern-1pt[ \bigotimes _{i \in I}{\vdash _{i}} ]\kern-1pt] $ is a lower bound of $\{ [\kern-1pt[ \vdash _{i} ]\kern-1pt] \colon i \in I \}$ .

To prove that $\{ [\kern-1pt[ \vdash _{i} ]\kern-1pt] \colon i \in I \}$ is the greatest lower bound of $[\kern-1pt[ \bigotimes _{i \in I}{\vdash _{i}} ]\kern-1pt] $ , consider a logic $\vdash $ such that ${\vdash } \leqslant {\vdash _{i}}$ for every $i \in I$ . Then for each $i \in I$ there is an interpretation $\boldsymbol {\tau }_{i} $ of $\vdash $ into $\vdash _{i}$ . Let $\boldsymbol {\tau }$ be the map that associates with every basic n-ary symbol $\ast $ of $\vdash $ the following n-ary term of $\bigotimes _{i \in I}{\vdash _{i}}$ :

$$ \begin{align*} \boldsymbol{\tau}(\ast) := \langle \boldsymbol{\tau}_{i}(\ast) \colon i \in I \rangle. \end{align*} $$

Now, consider a matrix $\langle \boldsymbol {A}, F \rangle \in \mathsf {Mod}^{\equiv }(\bigotimes _{i \in I}{\vdash _{i}})$ . From Proposition 4.5 it follows that $\langle \boldsymbol {A}, F \rangle \leqslant \prod _{j \in J} (\bigotimes _{i \in I}\langle \boldsymbol {A}_{i}^{j}, F_{i}^{j}\rangle )$ is a subdirect product for some $\langle \boldsymbol {A}_{i}^{j}, F_{i}^{j}\rangle \in \mathsf {Mod}^{\equiv }(\vdash _{i})$ . It is easy to see that

$$ \begin{align*} \langle \boldsymbol{A}^{\boldsymbol{\tau}}, F \rangle \; \leqslant\; \prod_{j \in J} \Big(\prod_{i \in I}\langle (\boldsymbol{A}_{i}^{j})^{\boldsymbol{\tau}_{i}}, F_{i}^{j}\rangle \Big) \end{align*} $$

is also a subdirect product. Since each $\boldsymbol {\tau }_{i}$ is an interpretation of $\vdash $ into $\vdash _{i}$ , we conclude that

$$ \begin{align*} \langle \boldsymbol{A}^{\boldsymbol{\tau}}, F \rangle \in \mathbb{P}_{\!{\scriptstyle \textrm{SD}}}^{}\mathbb{P}(\mathsf{Mod}^{\equiv}(\vdash)) = \mathbb{P}_{\!{\scriptstyle \textrm{SD}}}^{}(\mathsf{Mod}^{\equiv}(\vdash)). \end{align*} $$

Together with the fact that $\mathsf {Mod}^{\equiv }(\vdash )$ is closed under subdirect products by Lemma 2.3, this yields that $\langle \boldsymbol {A}^{\boldsymbol {\tau }}, F \rangle \in \mathsf {Mod}^{\equiv }(\vdash )$ . Hence we conclude that $\bigotimes _{i \in I}{\vdash _{i}} \leqslant {\vdash }$ .⊣

Proof. The right-to-left direction is an easy exercise. To prove the left-to-right direction, suppose that $\langle \vec {a}, \vec {c}\rangle \in \boldsymbol {\varOmega }^{\boldsymbol {A}}F$ . By Lemma 2.2(i), given an arbitrary $j \in I$ , we need to show that $p(\vec {a}(j)) \in F$ iff $p(\vec {c}(j)) \in F$ , for every unary polynomial function $p(x)$ of $\boldsymbol {A}_{j}$ . To this end, consider a formula $\varphi (x, y_{1}, \dots , y_{n})$ of $\boldsymbol {A}_{j}$ and elements $e_{1}, \dots , e_{n} \in A_{j}$ such that

(4) $$ \begin{align} \varphi^{\boldsymbol{A}_{j}}(\vec{a}(j), e_{1}, \dots, e_{n}) \in F_{j}. \end{align} $$

Since $\pi _{j} \colon A \to A_{j}$ is surjective, there are $\vec {e}_{1}, \dots , \vec {e}_{n} \in A$ whose j-th components are respectively $e_{1}, \dots , e_{n}$ . Moreover, as $F \ne \emptyset $ , we can choose an element $\vec {e} \in F$ . Then consider the basic operation

$$ \begin{align*} \psi(x, y_{1}, \dots, y_{n}, z) := \langle \psi_{i}(x, y_{1}, \dots, y_{n}, z) \colon i \in I \rangle \end{align*} $$

of $\boldsymbol {A}$ , where $\psi _{j} = \varphi $ , and $\psi _{i} = z$ for every $i \in J \smallsetminus \{ j \}$ . We have that for every $i \in I$ ,

$$ \begin{align*} \psi(\vec{a}, \vec{e}_{1}, \dots, \vec{e}_{n}, \vec{e})(i)= \left\{ \begin{array}{ll} \varphi^{\boldsymbol{A}_{j}}(\vec{a}(j), e_{1}, \dots, e_{n}) & \text{if}\ i= j,\\ \vec{e}(i) & \text{otherwise.}\\ \end{array} \right. \end{align*} $$

Together with (4) and $\vec {e} \in F$ , this implies that $\psi (\vec {a}, \vec {e}_{1}, \dots , \vec {e}_{n}, \vec {e}) \in F$ . Since $\langle \vec {a}, \vec {c }\kern 0.4pt \rangle \in \boldsymbol {\varOmega }^{\boldsymbol {A}}F$ , we obtain that $\psi (\vec {c}, \vec {e}_{1}, \dots , \vec {e}_{n}, \vec {e}) \in F$ as well. In particular, this means that

$$ \begin{align*} \varphi^{\boldsymbol{A}_{j}}(\vec{c}(j), e_{1}, \dots, e_{n}) = \psi(\vec{c}, \vec{e}_{1}, \dots, \vec{e}_{n}, \vec{e})(j) \in F_{j}. \end{align*} $$

Hence we conclude that $\langle \vec {a}(j), \vec {c}(j)\rangle \in \boldsymbol {\varOmega }^{\boldsymbol {A}_{j}}F_{j}$ , as desired.⊣

Proof. Condition (i) is an immediate consequence of Lemma 4.7. To prove condition (ii), consider the map $f \colon \langle \boldsymbol {A}, F \rangle ^{\ast } \to \bigotimes _{i \in I}\langle \boldsymbol {A}_{i}, F_{i}\rangle ^{\ast }$ defined as

$$ \begin{align*} f(a/\boldsymbol{\varOmega}^{\boldsymbol{A}}F) := \langle a(i)/\boldsymbol{\varOmega}^{\boldsymbol{A}_{i}}F_{i} \colon i \in I\rangle \end{align*} $$

for every $a \in A$ . From Lemma 4.7 it follows that f is a well-defined embedding. Together with the fact that $\langle \boldsymbol {A}, F \rangle \subseteq _{\textrm {sd}} \bigotimes _{i \in I}\langle \boldsymbol {A}_{i}, F_{i}\rangle $ , this implies that $\langle \boldsymbol {A}, F \rangle ^{\ast } \leqslant _{\textrm {sd}}\bigotimes _{i \in I}\langle \boldsymbol {A}_{i}, F_{i}\rangle ^{\ast }$ .⊣

Proof. The “only if” part is immediate. To prove the “if” one, suppose that each $\vdash _{i}$ has a theorem $\varphi _{i}$ . By substitution invariance, we can assume that $\varphi _{i} = \varphi _{i}(x)$ . Then the formula $\varphi (x) := \langle \varphi _{i}(x) \colon i \in I \rangle $ is a theorem of $\bigotimes _{i \in I}{\vdash _{i}}$ .⊣

Proof. (i) $\Rightarrow $ (ii): Let $\kappa := \prod _{i \in I}\vert Fm(\vdash _{i}) \vert $ and $Fm(\kappa )$ the set of formulas of $\bigotimes _{i \in I} {\vdash _{i}}$ in $\kappa $ variables. We know that $\kappa \geqslant \vert Fm(\kappa ) \vert $ . Since $\bigotimes _{i \in I} \vdash _{i}$ is the logic on $Fm(\kappa )$ induced by $\bigotimes _{i \in I}\mathsf {Mod}^{\equiv }(\vdash _{i})$ , we can apply Theorem 2.4 yielding

$$ \begin{align*} \langle \boldsymbol{A}, F \rangle \in \mathbb{R}\mathbb{S}\mathbb{P}_{\!{\scriptstyle \textrm{R}}_{\kappa^{+}}}^{}(\bigotimes_{i \in I}\mathsf{Mod}^{\equiv}(\vdash_{i})). \end{align*} $$

Then there are a matrix $\langle \boldsymbol {B}, G \rangle $ , a family of matrices $\{ \langle \boldsymbol {B}_{i}^{j}, G_{i}^{j}\rangle \colon i \in I, j \in J \}$ , and a $\kappa ^{+}$ -complete filter F on J such that $\langle \boldsymbol {B}, G \rangle ^{\ast } = \langle \boldsymbol {A}, F \rangle $ , $\langle \boldsymbol {B}_{i}^{j}, G_{i}^{j}\rangle \in \mathsf {Mod}^{\equiv }(\vdash _{i})$ , and

(5) $$ \begin{align} \langle \boldsymbol{B}, G \rangle \leqslant \Big(\prod_{j \in J} (\bigotimes_{i \in I} \langle \boldsymbol{B}_{i}^{j}, G_{i}^{j}\rangle) \Big)/ F{\kern -1pt}. \end{align} $$

It is easy to see that the map

$$ \begin{align*} f \colon \prod_{j \in J} (\bigotimes_{i \in I} \langle \boldsymbol{B}_{i}^{j}, G_{i}^{j}\rangle) \to \bigotimes_{i \in I} (\prod_{j \in J}\langle \boldsymbol{B}_{i}^{j}, G_{i}^{j}\rangle), \end{align*} $$

defined by the rule

$$ \begin{align*} f(\vec{a})(i)(j) := \vec{a}(j)(i), \text{ for every }i \in I, j \in J, \end{align*} $$

is an isomorphism. We shall see that also the map

$$ \begin{align*} g \colon \prod_{j \in J} (\bigotimes_{i \in I} \langle \boldsymbol{B}_{i}^{j}, G_{i}^{j}\rangle) / F \to \bigotimes_{i \in I} (\prod_{j \in J}\langle \boldsymbol{B}_{i}^{j}, G_{i}^{j}\rangle / F), \end{align*} $$

defined by the rule

$$ \begin{align*} g(\vec{a}/ F)(i) := f(\vec{a})(i)/F \text{, for every }i \in I, \end{align*} $$

is an isomorphism. The proof that g is a well-defined surjective homomorphism is routinary. To prove that g is also injective, consider $\vec {a}, \vec {c} \in \prod _{j \in J} (\bigotimes _{i \in I} \langle \boldsymbol {B}_{i}^{j}, G_{i}^{j}\rangle ) $ such that $g(\vec {a}/ F) = g(\vec {c}/ F)$ , i.e., that $f(\vec {a})(i) / F = f(\vec {c}) / F$ for every $i \in I$ . Since $\kappa \geqslant \vert I \vert $ and F is $\kappa ^{+}$ -complete, we have

$$ \begin{align*} \{ j \in J \colon \vec{a}(j) = \vec{c}(j) \} &= \bigcap_{i \in I} \{ j \in J \colon \vec{a}(j)(i) = \vec{c}(j)(i) \}\\ & = \bigcap_{i \in I} \{ j \in J \colon f(\vec{a})(i)(j) = f(\vec{c})(i)(j) \}\\ & \in F{\kern -1pt}. \end{align*} $$

Hence $\vec {a}/ F = \vec {c}/ F$ and, therefore, g is injective. This establishes that g is an isomorphism.

Together with (5), this yields that $\langle \boldsymbol {B}, G \rangle \leqslant \bigotimes _{i \in I} (\prod _{j \in J}\langle \boldsymbol {B}_{i}^{j}, G_{i}^{j}\rangle / F)$ . As a consequence, there are $\langle \boldsymbol {A}_{i}, F_{i}\rangle \in \mathbb {S}\mathbb {P}_{\!{\scriptstyle \textrm {R}}_{\kappa ^{+}}}^{}(\mathsf {Mod}^{\equiv }(\vdash _{i}))$ such that $\langle \boldsymbol {B}, G \rangle \leqslant _{\textrm {sd}} \bigotimes _{i \in I}\langle \boldsymbol {A}_{i}, F_{i}\rangle $ . Together with Corollary 4.8, this implies that

$$ \begin{align*} \langle \boldsymbol{A}, F\rangle \leqslant_{\; \textrm{sd}} \bigotimes_{i \in I}\langle \boldsymbol{A}_{i}, F_{i}\rangle^{\ast}, \end{align*} $$

where $\langle \boldsymbol {A}_{i}, F_{i} \rangle ^{\ast } \in \mathbb {R}\mathbb {S}\mathbb {P}_{\!{\scriptstyle \textrm {R}}_{\kappa ^{+}}}^{}(\mathsf {Mod}^{\equiv }(\vdash _{i}))$ . As $\kappa \geqslant \vert Fm(\vdash _{i})\vert $ , it is not hard to see that $\mathbb {P}_{\!{\scriptstyle \textrm {R}}_{\kappa ^{+}}}^{}(\mathsf {Mod}^{\equiv }(\vdash _{i})) \subseteq \mathsf {Mod}(\vdash _{i})$ . In particular, this implies that $\mathbb {S}\mathbb {P}_{\!{\scriptstyle \textrm {R}}_{\kappa ^{+}}}^{}(\mathsf {Mod}^{\equiv }(\vdash _{i})) \subseteq \mathsf {Mod}(\vdash _{i})$ and, therefore, that $\langle \boldsymbol {A}_{i}, F_{i} \rangle ^{\ast } \in \mathbb {R}(\mathsf {Mod}(\vdash _{i}))$ .

(ii) $\Rightarrow $ (i): From the definition of $\bigotimes _{i \in I}{\vdash _{i}}$ it follows that $\bigotimes _{i \in I}\langle \boldsymbol {A}_{i}, F_{i} \rangle $ is a model of $\bigotimes _{i \in I}{\vdash _{i}}$ . As submatrices of models are still models, this implies that $\langle \boldsymbol {A}, F \rangle \in \mathsf {Mod}(\bigotimes _{i \in I}{\vdash _{i}})$ . Finally, the matrix $\langle \boldsymbol {A}, F \rangle $ is reduced by Corollary 4.8.⊣

Proof. This is an easy consequence of Proposition 4.9, and of Lemmas 4.10 and 4.11⊣

Proof. We detail only the proof of the first inclusion, since the proof of the second one exploits similar ideas. Consider a matrix $\langle \boldsymbol {A}, F \rangle \in \mathbb {R}(\mathsf {Mod}(\bigotimes _{i \in I}{\vdash _{i}}))$ . First we consider the case where $F = \emptyset $ . As the matrix $\langle \boldsymbol {A}, F \rangle $ is reduced, we know that $\boldsymbol {A}$ is trivial by Lemma 4.11(i). Now, the fact that F is empty implies that $\bigotimes _{i \in I}{\vdash _{i}}$ has no theorems. From Proposition 4.9 it follows that there is $j \in I$ such that $\vdash _{j}$ has no theorems. Therefore by Lemma 4.11(ii) the $\mathscr {L}_{j}$ -matrix $\langle \boldsymbol {1}, \emptyset \rangle $ belongs to $\mathbb {R}(\mathsf {Mod}( \vdash _{j}))$ . As a consequence we obtain that

$$ \begin{align*} \langle \boldsymbol{A}, F \rangle = \langle \boldsymbol{1}, \emptyset \rangle^{\flat} \in \bigotimes_{i \in I}(\mathbb{R}(\mathsf{Mod}(\vdash_{i})). \end{align*} $$

Then we consider the case where $F \ne \emptyset $ . From Lemma 4.10 we know that $\langle \boldsymbol {A}, F \rangle \leqslant _{\textrm {sd}} \bigotimes _{i \in I}\langle \boldsymbol {A}_{i}, F_{i} \rangle $ for some $\langle \boldsymbol {A}_{i}, F_{i}\rangle \in \mathbb {R}(\mathsf {Mod}(\vdash _{i}))$ . Moreover, it is easy to see that the map

$$ \begin{align*} f \colon \prod_{i \in I} \langle \boldsymbol{A}_{i}, F_{i}\rangle^{\flat} \to \bigotimes_{i \in I}\langle \boldsymbol{A}_{i}, F_{i} \rangle \end{align*} $$

defined by the rule

$$ \begin{align*} f(\vec{a})(i) := \vec{a}(i)(i)\text{, for every }i \in I \end{align*} $$

is an isomorphism. Together with the fact that $\langle \boldsymbol {A}, F \rangle \leqslant _{\textrm {sd}} \bigotimes _{i \in I}\langle \boldsymbol {A}_{i}, F_{i} \rangle $ , this implies that

$$ \begin{align*} \langle \boldsymbol{A}, F \rangle \leqslant \prod_{i \in I} \langle \boldsymbol{A}_{i}, F_{i}\rangle^{\flat} \end{align*} $$

is a subdirect product. Hence we conclude that $\langle \boldsymbol {A}, F \rangle \in \mathbb {P}_{\!{\scriptstyle \textrm {SD}}}^{}(\bigotimes _{i \in I} \mathbb {R}(\mathsf {Mod}(\vdash _{i})))$ .⊣

Proof of Proposition 4.5. We begin by proving the first part. From Lemmas 2.3 and 4.13 it follows that

$$ \begin{align*} \mathsf{Mod}^{\equiv}(\bigotimes_{i \in I}{\vdash_{i}}) &= \mathbb{P}_{\!{\scriptstyle \textrm{SD}}}^{} \mathbb{R}(\mathsf{Mod}(\bigotimes_{i \in I}{\vdash_{i}})) \subseteq \mathbb{P}_{\!{\scriptstyle \textrm{SD}}}^{}\mathbb{P}_{\!{\scriptstyle \textrm{SD}}}^{} (\bigotimes_{i \in I} \mathbb{R}(\mathsf{Mod}(\vdash_{i})))\\ &= \mathbb{P}_{\!{\scriptstyle \textrm{SD}}}^{} (\bigotimes_{i \in I} \mathbb{R}(\mathsf{Mod}(\vdash_{i}))). \end{align*} $$

Moreover, since $\mathbb {R}(\mathsf {Mod}(\vdash _{i})) \subseteq \mathsf {Mod}^{\equiv }(\vdash _{i})$ for every $i \in I$ , we have

$$ \begin{align*} \mathbb{P}_{\!{\scriptstyle \textrm{SD}}}^{}(\bigotimes_{i \in I} \mathbb{R}(\mathsf{Mod}(\vdash_{i}))) \subseteq \mathbb{P}_{\!{\scriptstyle \textrm{SD}}}^{}(\bigotimes_{i \in I} \mathsf{Mod}^{\equiv}(\vdash_{i})). \end{align*} $$

It only remains to prove that $\mathbb {P}_{\!{\scriptstyle \textrm {SD}}}^{}(\bigotimes _{i \in I} \mathsf {Mod}^{\equiv }(\vdash _{i})) \subseteq \mathsf {Mod}^{\equiv }(\bigotimes _{i \in I}{\vdash _{i}})$ . Since the class $\mathsf {Mod}^{\equiv }(\bigotimes _{i \in I}{\vdash _{i}})$ is closed under subdirect products by Lemma 2.3, it suffices to show that $\bigotimes _{i \in I} \mathsf {Mod}^{\equiv }(\vdash _{i}) \subseteq \mathsf {Mod}^{\equiv }(\bigotimes _{i \in I}{\vdash _{i}})$ . To this end, consider a matrix $\langle \boldsymbol {A}_{i}, F_{i} \rangle \in \mathsf {Mod}^{\equiv }(\vdash _{i})$ for each $i \in I$ . By Lemma 2.3, for every $i \in I$ there is a family $\{ \langle \boldsymbol {A}_{i}^{j}, F_{i}^{j}\rangle \colon j \in J_{i} \} \subseteq \mathbb {R}(\mathsf {Mod}(\vdash _{i}))$ such that $\langle \boldsymbol {A}_{i}, F_{i} \rangle \leqslant \prod _{j \in J_{i}}\langle \boldsymbol {A}_{i}^{j}, F_{i}^{j}\rangle $ is a subdirect product. We can assume without loss of generality that $J_{i} = J_{j}$ for every $i, j \in I$ (for instance, by adding trivial matrices to the factors of products when necessary). Accordingly, we drop the index i in each $J_{i}$ , and write simply J. Under this convention, it is easy to see that

$$ \begin{align*} \bigotimes_{i \in I}\langle \boldsymbol{A}_{i}, F_{i} \rangle \leqslant \prod_{j \in J} (\bigotimes_{i \in I} \langle \boldsymbol{A}_{i}^{j}, F_{i}^{j}\rangle) \end{align*} $$

is a subdirect product. Together with Lemmas 4.13 and 2.3, this yields

$$ \begin{align*} \bigotimes_{i \in I}\langle \boldsymbol{A}_{i}, F_{i} \rangle \in \mathbb{P}_{\!{\scriptstyle \textrm{SD}}}^{}(\bigotimes_{i \in I}\mathbb{R}(\mathsf{Mod}(\vdash_{i}))) \subseteq \mathbb{P}_{\!{\scriptstyle \textrm{SD}}}^{}\mathbb{R}(\mathsf{Mod}(\bigotimes_{i \in I}{\vdash_{i}})) = \mathsf{Mod}^{\equiv}(\bigotimes_{i \in I}{\vdash_{i}}). \end{align*} $$

Hence we conclude that $\bigotimes _{i \in I} \mathsf {Mod}^{\equiv }(\vdash _{i}) \subseteq \mathsf {Mod}^{\equiv }(\bigotimes _{i \in I}{\vdash _{i}})$ , as desired.

To prove the second part, we rely on the first one. Consider a matrix $\langle \boldsymbol {A}, F \rangle \in \mathsf {Mod}^{\equiv }(\bigotimes _{i \in I}{\vdash _{i}}) = \mathbb {P}_{\!{\scriptstyle \textrm {SD}}}^{}(\bigotimes _{i \in I} \mathsf {Mod}^{\equiv }(\vdash _{i}))$ . We can assume without loss of generality that

$$ \begin{align*} \langle \boldsymbol{A}, F \rangle \subseteq \prod_{j \in J} \bigotimes_{i \in I} \langle \boldsymbol{B}_{i}^{j}, G_{i}^{j}\rangle \end{align*} $$

is a subdirect product for some families $\{\langle \boldsymbol {B}_{i}^{j}, G_{i}^{j}\rangle \colon j \in J\} \subseteq \mathsf {Mod}^{\equiv }(\vdash _{i})$ , one for each $i \in I$ . Then for every $i \in I$ , let

$$ \begin{align*} f \colon \prod_{j \in J} (\bigotimes_{i \in I} \langle \boldsymbol{B}_{i}^{j}, G_{i}^{j}\rangle) &\to \bigotimes_{i \in I} (\prod_{j \in J}\langle \boldsymbol{B}_{i}^{j}, G_{i}^{j}\rangle),\\ \pi_i \colon \prod_{i \in I}\prod_{j \in J}B_{i}^{j} &\to \prod_{j \in J}B_{i}^{j} \end{align*} $$

be, respectively, the isomorphism defined in the proof of Lemma 4.10, and the natural projection on the i-th component. Bearing this in mind, for every $i \in I$ let $\langle \boldsymbol {C}_{i}, H_{i}\rangle $ be the matrix where $\boldsymbol {C}_i$ is the subalgebra $\pi _i[f[\boldsymbol {A}]] \subseteq \prod _{j \in J}\boldsymbol {B}_{i}^{j}$ and $H_i = \pi _i[f[F]]$ .

The restriction $f{\upharpoonright }_A \colon \langle \boldsymbol {A}, F \rangle \to \bigotimes _{i \in I} \langle \boldsymbol {C}_{i}, H_{i}\rangle $ is a well-defined matrix embedding such that $\pi _i[f{\upharpoonright }_A [A]] = C_i$ for every $i \in I$ . Hence, we conclude that

$$ \begin{align*} \langle \boldsymbol{A}, F\rangle \leqslant_{\textrm{sd}} \bigotimes_{i \in I} \langle \boldsymbol{C}_{i}, H_{i}\rangle. \end{align*} $$

Now, it is not hard to see that $\langle \boldsymbol {C}_{i}, H_{i}\rangle $ is a subdirect product of $\prod _{j \in J}\langle \boldsymbol {B}_i^{j}, G_{i}^{j}\rangle $ , for every $i \in I$ . Since each $\mathsf {Mod}^{\equiv }(\vdash _{i})$ is closed under subdirect products, this implies that $\langle \boldsymbol {C}_{i}, H_{i}\rangle \in \mathsf {Mod}^{\equiv }(\vdash _i)$ for every $i \in I$ . This proves the inclusion from left to right.

To prove the other inclusion, let $\langle \boldsymbol {A}, F\rangle \leqslant _{\textrm {sd}} \bigotimes _{i \in I}\langle \boldsymbol {A}_{i}, F_{i}\rangle $ where $\langle \boldsymbol {A}_{i}, F_{i}\rangle \in \mathsf {Mod}^{\equiv } (\vdash _i)$ for every $i \in I$ . Then, as in the proof of Lemma 4.13, we have that $\langle \boldsymbol {A}, F \rangle $ is a subdirect product of $\prod _{i \in I} \langle \boldsymbol {A}_{i}, F_{i}\rangle ^{\flat }$ . From the fact that $\langle \boldsymbol {A}_{i}, F_{i}\rangle ^{\flat } \in \bigotimes _{i \in I} \mathsf {Mod}^{\equiv }(\vdash _{i})$ for every $i \in I$ , we obtain that $\langle \boldsymbol {A}, F \rangle \in \mathbb {P}_{\!{\scriptstyle \textrm {SD}}}^{}(\bigotimes _{i \in I} \mathsf {Mod}^{\equiv }(\vdash _{i}))$ .

Proof. As shown essentially in [Reference Taylor47, Lemma 1.9 and 1.10], if $\mathsf {K}_{1}$ and $\mathsf {K}_{2}$ are classes of matrices (resp. algebras) closed under subdirect products, then so is $\mathsf {K}_{1} \bigotimes \mathsf {K}_{2}$ . Together with Lemma 2.3, this implies that the class $\mathsf {Mod}^{\equiv }(\vdash ) \bigotimes \mathsf {Mod}^{\equiv }(\vdash ')$ is closed under subdirect products. By Proposition 4.5 we conclude that $\mathsf {Mod}^{\equiv }({\vdash } \bigotimes {\vdash '}) = \mathsf {Mod}^{\equiv }(\vdash ) \bigotimes \mathsf {Mod}^{\equiv }(\vdash ')$ .⊣

Fact 1. We have that $\langle \boldsymbol {A}, \{ 1 \}\rangle \in \mathsf {Mod}^{\equiv }(\vdash _{\lor })$ .

Proof. It is clear that $\langle \boldsymbol {A}, \{ 1 \}\rangle $ is a model of $\vdash _{\lor }$ . Hence it will be enough to prove that

is the identity relation on A. From the definition of $\vdash _{\lor }$ it follows that $\{ c, 1\}$ is a deductive filter of $\vdash _{\lor }$ on $\boldsymbol {A}$ . Now, an easy computation shows that:

1. (i) The blocks of $\boldsymbol {\varOmega }^{\boldsymbol {A}}\{ 1 \}$ are $\{ a, e, c \}, \{ 0, d\}, \{ b \}, \{ 1\}$ .

2. (ii) The blocks of $\boldsymbol {\varOmega }^{\boldsymbol {A}}\{ c, 1 \}$ are $\{ 0\}, \{ a\}, \{e \}, \{ b, d\}, \{ c, 1\}$ .

Together with the fact

this implies that

is the identity relation on A.⊣

Fact 2. The algebraic reducts of the matrices in $\mathsf {Mod}^{\equiv }(\vdash _{\lor })$ are either trivial or have at least four elements.

Proof. In this proof we assume that semilattices are equipped with the join-order. Consider a matrix $\langle \boldsymbol {B}, F\rangle \in \mathsf {Mod}^{\equiv }(\vdash _{\lor })$ such that $\boldsymbol {B}$ is non-trivial. By Corollary 2.6 we know that $\boldsymbol {B}$ is a semilattice with constants $\textbf {a}, \textbf {b}, \textbf {0}$ such that

(6) $$ \begin{align} \textbf{0} \leqslant \textbf{a} \text{ and }\textbf{0} \leqslant \textbf{b}. \end{align} $$

Now, since $\boldsymbol {B}$ is non-trivial, we know that $F \ne B$ . Together with the fact that

$$ \begin{align*} \textbf{a} \vdash_{\lor} x \quad \textbf{b} \vdash_{\lor} x \quad \textbf{0} \vdash_{\lor} x \end{align*} $$

this implies that $\textbf {a}, \textbf {b}, \textbf {0} \notin F$ . Observe that $\textbf {a} \lor \textbf {b} \in F$ , since $\emptyset \vdash _{\lor }\textbf {a} \lor \textbf {b}$ . Hence, to conclude that B has at least four elements, it will be enough to check that $\textbf {a}, \textbf {b}, \textbf {0}$ are different one from the other. From the fact that $\textbf {a}, \textbf {b} \notin F$ and $\textbf {a} \lor \textbf {b} \in F$ , it follows that $\textbf {a}$ and $\textbf {b}$ are incomparable in the order of $\boldsymbol {B}$ . Together with (6), this implies that $\textbf {0}$ is different from $\textbf {a}$ and $\textbf {b}$ .⊣

Fact 3. $\mathsf {Mod}^{\equiv }(\vdash _{\lnot })$ is the class of matrices $\langle \boldsymbol {B}, F\rangle $ such that either $\boldsymbol {B}$ is trivial or $\boldsymbol {B}$ is a negation algebra and in this case either $F= \emptyset $ or $F= \{ a \}$ for some $a \in B$ that is not a fixed point of $\lnot $ .

Proof. The interested reader may consult the Appendix for the details.⊣

Fact 4. For every $\kappa> 0$ , the logic $\vdash _{\kappa }$ is equivalential.

Proof. Consider the set

$$ \begin{align*} \varDelta(x, y) := \{ x \multimap_{\alpha} y \colon \alpha < \kappa \}. \end{align*} $$

It is easy to see that $\varDelta $ witnesses the validity of the rules in Theorem 2.7. Hence we conclude that $\vdash _{\kappa }$ is equivalential.⊣

Fact 5. For every $\kappa> 0$ , $[\kern-1pt[ \vdash _{\kappa }]\kern-1pt] $ is an upper bound of $[\kern-1pt[ \vdash _{\lor }]\kern-1pt] $ and $[\kern-1pt[ \vdash _{\lnot }]\kern-1pt] $ in $\mathsf {Log}$ .

Proof. Consider the class of matrices $\mathsf {K} := \{ \langle \boldsymbol {A}_{\alpha , \kappa }, \{ 1 \} \rangle \colon \alpha < \kappa \}$ . It is clear that $\vdash _{\kappa }$ is the logic induced by $\mathsf {K}$ and that $\mathbb {S}(\mathsf {K}) = \mathsf {K}$ . Then let $\boldsymbol {\tau }$ be the identity translation of $\mathscr {L}_{\vdash _{\lor }}$ into $\mathscr {L}_{\vdash _{\kappa }}$ . By Fact 1 we have

$$ \begin{align*} \langle \boldsymbol{B}^{\boldsymbol{\tau}}, F \rangle = \langle \boldsymbol{A}, \{ 1 \} \rangle \in \mathsf{Mod}^{\equiv}(\vdash_{\lor}) \end{align*} $$

for every $\langle \boldsymbol {B}, F \rangle \in \mathsf {K}$ . Together with Fact 4 and Proposition 3.9, this implies that $\boldsymbol {\tau }$ is an interpretation of $\vdash _{\lor }$ into $\vdash _{\kappa }$ .

A similar argument (requiring Fact 3) shows that $\vdash _{\lor }$ is also interpretable in $\vdash _{\kappa }$ .⊣

Fact 6. For every $\kappa>0$ , we have $[\kern-1pt[ \vdash ]\kern-1pt] \leqslant [\kern-1pt[ \vdash _{\kappa }]\kern-1pt] $ .

Proof. This is a direct consequence of Fact 5.⊣

Fact 7. There is $\alpha < \kappa ^{+}$ such that the symbol $\multimap _{\alpha }$ does not appear in the terms $\{ \boldsymbol {\tau }(\varphi ) \colon \varphi \in \mathscr {L}_{\vdash } \}$ .

Proof. Straightforward.⊣

Fact 8. The algebra $\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}$ is term-equivalent to

$$ \begin{align*} \langle A; \lor^{\boldsymbol{A}_{\alpha, \kappa^{+}}}, \lnot^{\boldsymbol{A}_{\alpha, \kappa^{+}}}, \textbf{a}, \textbf{b}, \textbf{0}, e\rangle. \end{align*} $$

Proof. Using negation, it is easy to see that all constants from $\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}$ are definable in the displayed algebra. Moreover, if $\beta \ne \alpha $ , then $\multimap _{\beta }^{\boldsymbol {A}_{\alpha , \kappa ^{+}}}$ is a constant map. This shows that all term-functions of $\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}$ are also term-functions of the algebra in the display. The converse is obvious.⊣

Fact 9. If $\gamma (x)$ is a formula of $\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}$ such that $\langle A; \gamma ^{\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}} \rangle $ is a negation algebra, then $\gamma $ can be obtained as a composition of $\lor $ and $\lnot $ .

Proof. Assume that $\langle A; \gamma ^{\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}} \rangle $ is a negation algebra. Suppose, with a view to contradiction, that either $\textbf {0}$ or $\textbf {a}$ or $\textbf {b}$ occur in $\gamma $ . It is not hard to see that this implies that $e \notin \gamma ^{\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}}[A]$ . However, since $\langle A; \gamma ^{\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}}\rangle $ is a negation algebra, we know that

$$ \begin{align*} e = \gamma^{\hat{\boldsymbol{A}}_{\alpha, \kappa^{+}}} \gamma^{\hat{\boldsymbol{A}}_{\alpha, \kappa^{+}}}(e) \in \gamma^{\hat{\boldsymbol{A}}_{\alpha, \kappa^{+}}}[A], \end{align*} $$

which is false. Hence we conclude that $\textbf {0}$ , $\textbf {a}$ , and $\textbf {b}$ do not occur in $\gamma $ .

It only remains to prove that e does not occur in $\gamma $ . Suppose the contrary, with a view to contradiction. An easy induction on the construction of formulas shows that if $\varphi (x)$ is a formula of $\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}$ in which $\textbf {0}$ , $\textbf {a}$ , and $\textbf {b}$ do not occur and in which e occurs, then $\varphi ^{\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}}(0) \in \{ e, \textbf {a}, c \}$ . As $\textbf {0}$ , $\textbf {a}$ , and $\textbf {b}$ do not occur in the composition $\gamma (\gamma (x))$ , this means that $\gamma ^{\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}}\gamma ^{\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}}(0) \ne 0$ . But this contradicts the fact that $\langle A; \gamma ^{\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}}\rangle $ is a negation algebra, as desired.⊣

Fact 10. The blocks of $\boldsymbol {\varOmega }^{\boldsymbol {A}_{\alpha , \kappa ^{+}}^{\boldsymbol {\tau }}}\{ 1 \}$ are $\{ 0, d \}, \{a, c, e \}, \{ b \}, \{ 1 \}$ .

Proof. By Fact 7 we know that the term-functions of $\boldsymbol {A}^{\boldsymbol {\tau }}_{\alpha , \kappa ^{+}}$ are also term-functions of $\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}$ . In particular, this means that $\textrm {Con} \skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}} \subseteq \textrm {Con} \boldsymbol {A}_{\alpha , \kappa ^{+}}^{\boldsymbol {\tau }}$ .

Consider the equivalence relation $\theta $ on A determined by the partition in the statement. Using for instance Fact 8, it is easy to see that $\theta $ is a congruence of $\skew6\hat {\boldsymbol{A}}_{\alpha , \kappa ^{+}}$ . Then $\theta $ is also a congruence of $\boldsymbol {A}^{\boldsymbol {\tau }}_{\alpha , \kappa ^{+}}$ . As $\theta $ is compatible with $\{ 1 \}$ , this implies that $\theta \subseteq \boldsymbol {\varOmega }^{\boldsymbol {A}_{\alpha , \kappa ^{+}}^{\boldsymbol {\tau }}}\{ 1 \}$ .

As a consequence, we obtain that $A / \boldsymbol {\varOmega }^{\boldsymbol {A}_{\alpha , \kappa ^{+}}^{\boldsymbol {\tau }}}\{ 1 \}$ is a set of at most four elements. Moreover, since $\boldsymbol {\varOmega }^{\boldsymbol {A}_{\alpha , \kappa ^{+}}^{\boldsymbol {\tau }}}\{ 1 \}$ is compatible with $\{ 1\}$ , we know that $\langle 0, 1 \rangle \notin \boldsymbol {\varOmega }^{\boldsymbol {A}_{\alpha , \kappa ^{+}}^{\boldsymbol {\tau }}}\{ 1 \}$ . Therefore we have

(8) $$ \begin{align} 2 \leqslant \vert A / \boldsymbol{\varOmega}^{\boldsymbol{A}_{\alpha, \kappa^{+}}^{\boldsymbol{\tau}}}\{ 1 \} \vert \leqslant 4. \end{align} $$

Now, it is easy to see that $\langle \boldsymbol {A}_{\alpha , \kappa ^{+}}, \{ 1 \} \rangle \in \mathbb {R}(\mathsf {Mod}^{\equiv }(\vdash _{\kappa ^{+}}))$ . Since $\boldsymbol {\tau }$ is an interpretation of $\vdash $ into $\vdash _{\kappa ^{+}}$ , this implies that $\langle \boldsymbol {A}_{\alpha , \kappa ^{+}}^{\boldsymbol {\tau }}, \{ 1 \} \rangle \in \mathsf {Mod}(\vdash )$ and, therefore, that $\langle \boldsymbol {A}_{\alpha , \kappa ^{+}}^{\boldsymbol {\tau }}, \{ 1 \} \rangle ^{\ast } \in \mathsf {Mod}^{\equiv }(\vdash )$ . Together with Fact 2 and ${\vdash _{\lor }} \leqslant {\vdash }$ , this implies that either the matrix $\langle \boldsymbol {A}_{\alpha , \kappa ^{+}}^{\boldsymbol {\tau }}, \{ 1 \} \rangle ^{\ast }$ is trivial, or the congruence $\boldsymbol {\varOmega }^{\boldsymbol {A}_{\alpha , \kappa ^{+}}^{\boldsymbol {\tau }}}\{ 1 \}$ has at least four blocks. By (8) we conclude that $\boldsymbol {\varOmega }^{\boldsymbol {A}_{\alpha , \kappa ^{+}}^{\boldsymbol {\tau }}}\{ 1 \}$ has exactly four blocks. Together with the fact that $\theta \subseteq \boldsymbol {\varOmega }^{\boldsymbol {A}_{\alpha , \kappa ^{+}}^{\boldsymbol {\tau }}}\{ 1 \}$ , this implies that $\theta = \boldsymbol {\varOmega }^{\boldsymbol {A}_{\alpha , \kappa ^{+}}^{\boldsymbol {\tau }}}\{ 1 \}$ .⊣

Proof. (i): Let $\varDelta (x, y)$ be the set of formulas witnessing the fact that $\vdash $ is equivalential, as in Theorem 2.7. Moreover, let $\boldsymbol {\tau }$ be an interpretation of $\vdash $ into $\vdash '$ . We consider the set $\varSigma (x, y) := \boldsymbol {\tau }[\varDelta ]$ of formulas of $\mathscr {L}_{\vdash '}$ . In order to establish that $\vdash '$ is equivalential, it will be enough to show that $\varSigma $ and $\vdash '$ satisfy the conditions in Theorem 2.7.

From Proposition 3.3 it follows that $\emptyset \vdash ' \varSigma (x, x)$ and $x, \varSigma (x, y) \vdash ' y$ . It only remains to prove that for every n-ary connective $\ast $ of $\vdash '$ ,

(10) $$ \begin{align} \bigcup_{1 \leqslant i \leqslant n}\varSigma(x_{i}, y_{i}) \vdash' \varSigma(\ast(x_{1}, \dots, x_{n}), \ast(y_{1}, \dots, y_{n})). \end{align} $$

To this end, consider an n-ary connective $\ast $ of $\vdash '$ , a matrix $\langle \boldsymbol {A}, F \rangle \in \mathsf {Mod}^{\equiv }(\vdash ')$ , and tuples $\vec {a}, \vec {c} \in A^{n}$ such that

$$ \begin{align*} \bigcup_{1 \leqslant i \leqslant n}\varSigma^{\boldsymbol{A}}(a_{i}, c_{i}) \subseteq F{\kern -1pt}. \end{align*} $$

Since $\varSigma = \boldsymbol {\tau }[\varDelta ]$ , we have

$$ \begin{align*} \bigcup_{1 \leqslant i \leqslant n}\varDelta^{\boldsymbol{A}^{\boldsymbol{\tau}}}(a_{i}, c_{i}) \subseteq F{\kern -1pt}. \end{align*} $$

As $\varDelta $ is a set of congruence formulas for $\vdash $ , and $\langle \boldsymbol {A}^{\boldsymbol {\tau }}, F \rangle \in \mathsf {Mod}^{\equiv }(\vdash ) = \mathbb {R}(\mathsf {Mod}(\vdash ))$ , the above display implies that $\vec {a} = \vec {c}$ . As a consequence, we obtain that $\ast ^{\boldsymbol {A}}(\vec {a}) = \ast ^{\boldsymbol {A}}(\vec {c}\kern 0.4pt )$ . Since $\emptyset \vdash ' \varSigma (x, x)$ and $\langle \boldsymbol {A}, F \rangle \in \mathsf {Mod}(\vdash ')$ , this yields

$$ \begin{align*} \varSigma^{\boldsymbol{A}}(\ast(\vec{a}), \ast(\vec{c}\kern 0.4pt)) = \varSigma^{\boldsymbol{A}}(\ast(\vec{a}), \ast(\vec{a})) \subseteq F{\kern -1pt}. \end{align*} $$

Hence we conclude that (10) holds.

(ii): Given $i \in I$ , let $\varDelta _{i}(x, y)$ be a set of congruence formulas for $\vdash _{i}$ . Observe that the Cartesian product $\prod _{i \in I} \varDelta _{i}$ can be viewed as a set $\varDelta (x, y)$ of formulas of $\bigotimes _{i \in I}{\vdash _{i}}$ . Since the various $\varDelta _{i}$ satisfy the rules in Theorem 2.7, and $\bigotimes _{i \in I}{\vdash _{i}}$ is the logic induced by $\bigotimes _{i \in I} \mathsf {Mod}^{\equiv }(\vdash _{i})$ , it is easy to see that the set $\varDelta $ satisfies the rules in Theorem 2.7 as well. As a consequence, we conclude that $\bigotimes _{i \in I} {\vdash _{i}}$ is an equivalential logic.⊣

Proof. (i): Observe that the $\mathscr {L}_{\vdash _{i}}$ -reducts of the matrices in (11) are reduced. Together with the fact that $\varDelta $ is a set of congruence formulas for $\vdash _{i}$ , this easily implies that $\varDelta $ satisfies the conditions of Theorem 2.7 for $\bigoplus _{i \in I}{\vdash _{i}}$ . As a consequence, we conclude that $\varDelta $ is a set of congruence formulas for $\bigoplus _{i \in I}{\vdash _{i}}$ .

(ii): Immediate from (i). (iii): Let $\mathsf {M}$ be the class of matrices in (11). It is easy to see that the matrices in $\mathsf {M}$ are reduced and, therefore, that $\mathsf {M} \subseteq \mathsf {Mod}^{\equiv }(\bigoplus _{i \in I}{\vdash _{i}})$ . To prove the other inclusion, consider $\langle \boldsymbol {A}, F \rangle \in \mathsf {Mod}^{\equiv }(\bigoplus _{i \in I}{\vdash _{i}})$ . As $\bigoplus _{i \in I}{\vdash _{i}}$ is equivalential by (ii), we can apply Theorem 2.7 obtaining that $\langle \boldsymbol {A}, F \rangle \in \mathbb {R}(\mathsf {Mod}(\bigoplus _{i \in I}{\vdash _{i}}))$ . It will be enough to show that (for every $i \in I$ ) the $\mathscr {L}_{\vdash _{i}}$ -reduct $\langle \boldsymbol {A}^{-}, F \rangle $ of $\langle \boldsymbol {A}, F \rangle $ is a reduced model of $\vdash _{i}$ . The fact that $\langle \boldsymbol {A}^{-}, F\rangle $ is a model of $\vdash _{i}$ is clear. To prove that it is reduced, let $\varDelta $ be a set of congruence formulas of $\vdash _{i}$ . By (i) we know that $\varDelta $ is also a set of congruence formulas for $\bigoplus _{i \in I}{\vdash _{i}}$ . Together with the fact that $\langle \boldsymbol {A}, F \rangle $ is a reduced model of $\bigoplus _{i \in I}{\vdash _{i}}$ , this implies that for every $a, b \in A$ ,

$$ \begin{align*} a = b \Longleftrightarrow \varDelta^{\boldsymbol{A}}(a, b) \subseteq F \Longleftrightarrow \varDelta^{\boldsymbol{A}^{-}}(a, b) \subseteq F{\kern -1pt}. \end{align*} $$

Since $\langle \boldsymbol {A}^{-}, F \rangle $ is a model of $\vdash _{i}$ , this implies that the matrix $\langle \boldsymbol {A}^{-}, F \rangle $ is reduced.

(iv): By (i) we know that $[\kern-1pt[ \bigoplus _{i \in I}{\vdash _{i}} ]\kern-1pt] $ belongs to $\mathsf {Equiv}$ . Hence it will be enough to show that it is the supremum of $\{ [\kern-1pt[ \vdash _{i}]\kern-1pt] \colon i \in I\}$ in $\mathsf {Log}$ . Recall from Theorem 2.7 that $\mathsf {Mod}^{\equiv }(\vdash _{i}) = \mathbb {R}(\mathsf {Mod}(\vdash _{i}))$ for all $i \in I$ . Together with (iii), this implies that ${\vdash _{j}} \leqslant {\bigoplus _{i \in I}{\vdash _{i}}}$ for all $j \in I$ .

Now, consider a logic $\vdash $ such that ${\vdash _{i}} \leqslant {\vdash }$ for every $i \in I$ . Then for every $i \in I$ , there is an interpretation $\boldsymbol {\tau }_{i}$ of $\vdash _{i}$ into $\vdash $ . Observe that all these $\boldsymbol {\tau }_{i}$ can be joined together into a translation $\boldsymbol {\tau }$ of $\bigoplus _{i \in I}{\mathscr {L}_{i}}$ into $\mathscr {L}_{\vdash }$ . We will show that $\boldsymbol {\tau }$ is also an interpretation of $\bigoplus _{i \in I}{\vdash _{i}}$ into $\vdash $ . To this end, consider a matrix $\langle \boldsymbol {A}, F\rangle \in \mathsf {Mod}^{\equiv }(\vdash )$ . We know that $\langle \boldsymbol {A}^{\boldsymbol {\tau }_{i}}, F\rangle \in \mathsf {Mod}^{\equiv }(\vdash _{i}) = \mathbb {R}(\mathsf {Mod}(\vdash _{i}))$ for every $i \in I$ . This implies that the matrix $\langle \boldsymbol {A}^{\boldsymbol {\tau }}, F\rangle $ belongs to the class in (11). By (iii) we conclude that $\langle \boldsymbol {A}, F\rangle \in \mathsf {Mod}^{\equiv }(\bigoplus _{i \in I}{\vdash _{i}})$ .⊣

Proof. From Proposition 6.1(ii) and Lemma 6.4(iv).⊣

Proof. We first prove that $\mathsf {Log}$ has no minimum. Suppose, with a view to contradiction, that $\mathsf {Log}$ has a minimum $[\kern-1pt[ \vdash ]\kern-1pt] $ . Then let $\kappa := \vert Fm(\vdash ) \vert $ and consider the language $\mathscr {L}$ that consists in $k^{+}$ binary connectives $\{ \multimap _{\alpha } \colon \alpha < \kappa ^{+}\}$ . For every $\alpha < \kappa ^{+}$ , let $\boldsymbol {A}_{\alpha }$ be the $\mathscr {L}$ -algebra with universe $\{ 1, 0, a \}$ and operations defined for every $p , q \in A$ and $\beta < \kappa ^{+}$ as follows:

$$ \begin{align*} p \multimap_{\beta} q:= \left\{\begin{array}{@{\,}ll} 1 & \text{if}\ p=q\ \text{or}\ \beta \ne \alpha,\\ 0 & \text{if}\ p \ne q\ \text{and}\ \beta = \alpha.\\ \end{array} \right. \end{align*} $$

Let also $\vdash _{\kappa ^{+}}$ be the logic (formulated in a countable set of variables) induced by the class of reduced matrices

$$ \begin{align*} \mathsf{M} := \{ \langle \boldsymbol{A}_{\alpha}, \{ 1, a \}\rangle \colon \alpha < \kappa^{+} \}. \end{align*} $$

Clearly, $\mathsf {M} \subseteq \mathsf {Mod}^{\equiv }(\vdash _{\kappa ^{+}})$ .

Since $\vdash $ is the minimum of $\mathsf {Log}$ , there is an interpretation $\boldsymbol {\tau }$ of $\vdash $ into $\vdash _{\kappa ^{+}}$ . On cardinality grounds, there is $\alpha < \kappa ^{+}$ such that the symbol $\multimap _{\alpha }$ does not occur in the formulas $\{ \boldsymbol {\tau }(\varphi ) \colon \varphi \in \mathscr {L} \}$ . In particular, this implies that the matrix $\langle \boldsymbol {A}_{\alpha }^{\boldsymbol {\tau }}, \{ 1, a \} \rangle $ is not reduced.

On the other hand, we know that

is the identity relation, since $\boldsymbol {\tau }$ is an interpretation of  $\vdash $ into $\vdash _{\kappa ^{+}}$ and $\langle \boldsymbol {A}_{\alpha }, \{ 1, a \} \rangle \in \mathsf {Mod}^{\equiv }(\vdash _{\kappa ^{+}})$ . Now, since $A_{\alpha }= \{ 1, 0, a \}$ , the only deductive filter of $\vdash $ on $\boldsymbol {A}_{\alpha }^{\boldsymbol {\tau }}$ extending properly $\{ 1, a \}$ is forcefully $\{ 1, 0, a \}$ . Hence we obtain that

But this implies that $\boldsymbol {\varOmega }^{\boldsymbol {A}_{\alpha }^{\boldsymbol {\tau }}} \{ 1, a \}$ is the identity relation, which is false.

Now, from Lemma 7.1 it follows easily that the class of inconsistent (resp. almost inconsistent) logics is the maximum (resp. a coatom) of $\mathsf {Log}$ . Hence, in order to establish the second part of the theorem it only remains to show that the class $\mathcal {K}$ of all almost inconsistent logics is the unique coatom of $\mathsf {Log}$ , and that a logic $\vdash $ lacks theorems if and only if $[\kern-1pt[ \vdash ]\kern-1pt] \leqslant {\mathcal {K}}$ .

By Lemmas 4.11(ii) and 7.1 a logic $\vdash $ lacks theorems if and only if $[\kern-1pt[ \vdash ]\kern-1pt] \leqslant {\mathcal {K}}$ . Hence it only remains to show that $\mathcal {K}$ is the unique coatom of $\mathsf {Log}$ . Suppose, with a view to contradiction, that there is a coatom $[\kern-1pt[ \vdash ]\kern-1pt] $ in $\mathsf {Log}$ such that $\vdash $ is not almost inconsistent. Since $[\kern-1pt[ \vdash ]\kern-1pt] $ is neither the maximum of nor comparable with $\mathcal {K}$ , we know that $\vdash $ is not inconsistent and that it has theorems. Then there is a matrix $\langle \boldsymbol {A}, F\rangle \in \mathsf {Mod}^{\equiv }(\vdash )$ such that $F \in \mathcal {P}(A) \smallsetminus \{ \emptyset , A \}$ . In particular, this implies that $\vert A \vert \geqslant 2$ . Now, consider the matrix

$$ \begin{align*} \langle \boldsymbol{B}, G \rangle := \langle \boldsymbol{A}, F \rangle^{\vert A \vert} \in \mathbb{P}(\mathsf{Mod}^{\equiv}(\vdash)) \subseteq \mathsf{Mod}^{\equiv}(\vdash) \end{align*} $$

and observe that $\vert B \vert> \vert A \vert $ by Cantor’s Theorem.

Let $\boldsymbol {B}^{+}$ be the expansion of $\boldsymbol {B}$ with all finitary operations on B, and consider the logic $\vdash ^{+}$ formulated in $\vert Fm(\vdash ) \vert $ variables induced by the matrix $\langle \boldsymbol {B}^{+}, G \rangle $ .

Bering in mind that all finitary operations on B are term-function of $\boldsymbol {B}^{+}$ , it is not hard to see that the matrix $\langle \boldsymbol {B}^{+}, G \rangle $ is reduced and that the logic $\vdash ^{+}$ is equivalential (see [Reference Moraschini34, Lemma 3.2] if necessary). Moreover, we have that $\mathbb {S}(\boldsymbol {B}^{+}) = \{ \boldsymbol {B}^{+} \}$ . Together with Proposition 3.9, this implies that the identity map is a translation of $\vdash $ into $\vdash ^{+}$ . Since $\vdash $ is a coatom of $\mathsf {Log}$ , this implies that either $\vdash ^{+}$ is inconsistent or it is equi-interpretable with $\vdash $ . As $G \ne B$ and $\langle \boldsymbol {B}^{+}, G \rangle $ is a model of $\vdash ^{+}$ , we know that $\vdash ^{+}$ is not inconsistent, whence ${\vdash ^{+}} \leqslant {\vdash }$ .

Together with the fact that $\langle \boldsymbol {A}, F \rangle \in \mathsf {Mod}^{\equiv }(\vdash )$ , this implies that $\mathsf {Mod}^{\equiv }(\vdash ^{+})$ contains a matrix of size $\vert A \vert $ . However, from Lemma 2.8 it follows that every non-trivial member of $\mathsf {Mod}^{\equiv }(\vdash ^{+})$ has cardinality $\geqslant \vert B \vert $ . Together with the fact that $\vert A \vert < \vert B \vert $ , this implies that $\boldsymbol {A}$ is trivial, which is false.⊣

Proof sketch. It is well known that if $\mathsf {K}$ is a variety, then $\vDash _{\mathsf {K}}$ is an algebraizable [Reference Blok and Pigozzi5] (and, therefore, equivalential) $2$ -deductive system such that

$$ \begin{align*} \mathsf{Mod}^{\equiv}(\vDash_{\mathsf{K}}) = \{ \langle \boldsymbol{A}, \{ \langle a, a \rangle \colon a \in A \} \rangle \colon \boldsymbol{A} \in \mathsf{K} \}. \end{align*} $$

As a consequence, a variety $\mathsf {K}$ is interpretable into another variety $\mathsf {V}$ if and only if $\vDash _{\mathsf {K}}$ is interpretable into $\vDash _{\mathsf {V}}$ . Hence, the map in the statement is an order-embedding. The fact that it is a lattice homomorphism follows from the description of infima and suprema in $\mathsf {Var}$ [Reference García and Taylor20, Reference Neumann39], and from a straightforward adaptation of the description of infima and suprema of equivalential logics given here to the case of two-deductive systems.⊣

Proof. We claim that if $\mathsf {K}$ and $\mathsf {V}$ are varieties such that ${\mathsf {K}} \leqslant {\mathsf {V}}$ , then ${\vdash _{\mathsf {K}}^{[2]}} \leqslant {\vdash _{\mathsf {V}}^{[2]}}$ . To prove this, let $\boldsymbol {\tau }$ be an interpretation of $\mathsf {K}$ into $\mathsf {V}$ . It is not hard to see that the map $\boldsymbol {\tau }^{\ast }$ , defined by the rule $\langle t_{1}, t_{2}\rangle \longmapsto \langle \boldsymbol {\tau }(t_{1}), \boldsymbol {\tau }(t_{2})\rangle $ , is an interpretation of $\mathsf {K}^{[2]}$ into $\mathsf {V}^{[2]}$ . We will show that $\boldsymbol {\tau }^{\ast }$ is also an interpretation of $\vdash _{\mathsf {K}}^{[2]}$ into $\vdash _{\mathsf {V}}^{[2]}$ . To this end, consider $\langle \boldsymbol {A}, F \rangle \in \mathsf {Mod}^{\equiv }(\vdash _{\mathsf {V}}^{[2]})$ . By Theorem 8.3 there is $\boldsymbol {B} \in \mathsf {V}^{[2]}$ such that $\langle \boldsymbol {A}, F \rangle \cong \langle \boldsymbol {B}, \{ \langle b, b \rangle \colon b \in B \} \rangle $ . As $\boldsymbol {\tau }^{\ast }$ is an interpretation of $\mathsf {K}^{[2]}$ into $\mathsf {V}^{[2]}$ , this yields $\boldsymbol {B}^{\boldsymbol {\tau }^{\ast }} \in \mathsf {K}^{[2]}$ . Hence, by Theorem 8.3 we obtain