On the complexity of the Leibniz hierarchy

TL;DR

This paper establishes the computational complexity of determining whether a finite logical matrix corresponds to various classes of algebraizable logics, proving EXPTIME-completeness for most cases.

Contribution

It provides the first complexity classification for the problem of identifying algebraizable and related logics from finite matrices.

Findings

Determined EXPTIME-completeness for algebraizable logic recognition

Extended results to order algebraizable, weakly algebraizable, equivalential, and protoalgebraic logics

Showed truth-equational logic recognition is EXPTIME-hard

Abstract

We prove that the problem of determining whether a finite logical matrix determines an algebraizable logic is complete for EXPTIME. The same result holds for the classes of order algebraizable, weakly algebraizable, equivalential and protoalgebraic logics. Finally, the same problem for the class of truth-equational logic is shown to be hard for EXPTIME.

Equations

$$\Gamma ⊢\phi ⟺\Delta ⊢\phi \text{ for some finite }\Delta \subseteq \Gamma .$$

$$\Gamma {⊢}_{\mathsf{M}}\phi ⟺\text{ for every evaluation }f,\text{ if }f[\Gamma ]\subseteq F\text{, then }f(\phi )\in F.$$

$$⟨a,b⟩\in {\Omega }^{\mathbf{A}}F⟺\Delta (a,b,\vec{c})\subseteq F\text{ for all }\vec{c}\in A.$$

$$F=\{a\in A:\mathbf{A}\models \mathbf{\tau }(a)\}.$$

$$\Delta (x_1,y_1)\cup \cdots \cup \Delta (x_n,y_n)⊢\Delta (f(x_1,\dots ,x_n),f(y_1,\dots ,y_n)).$$

$$b\in F⟺\mathbf{B}/{\Omega }^{\mathbf{B}}F\models \mathbf{\tau }(b/{\Omega }^{\mathbf{B}}F).$$

$${\mathsf{Mod}}^{\ast }(⊢)=(\mathbb{S}{\mathbb{P}}_{\text{textsc}r}(\mathsf{M}){)}^{\ast }=({\mathbb{P}}_{\text{textsc}sd}\mathbb{S}{\mathbb{P}}_{\text{textsc}u}(\mathsf{M}){)}^{\ast }=({\mathbb{P}}_{\text{textsc}sd}\mathbb{S}(\mathsf{M}){)}^{\ast },$$

$${\mathsf{Mod}}^{\ast }(⊢)=({\mathbb{P}}_{\text{textsc}sd}((\mathbb{S}(\mathsf{M}){)}^{\ast }){)}^{\ast }.$$

$${\mathsf{Mod}}^{\ast }(⊢)=({\mathbb{P}}_{\text{textsc}sd}((\mathbb{S}(\mathsf{M}){)}^{\ast }){)}^{\ast }={\mathbb{P}}_{\text{textsc}sd}((\mathbb{S}(\mathsf{M}){)}^{\ast }),$$

$$b\in F⟺\mathbf{B}/{\Omega }^{\mathbf{B}}F\models \mathbf{\tau }(b/{\Omega }^{\mathbf{B}}F).$$

$$G=\{b\in B:\mathbf{B}\models \mathbf{\tau }(b)\}\text{ and }F\subseteq \{a\in A:\mathbf{A}/{\Omega }^{\mathbf{A}}F\models \mathbf{\tau }(a/{\Omega }^{\mathbf{A}}F)\}.$$

$${\epsilon }^{\mathbf{A}/{\Omega }^{\mathbf{A}}F}(a/{\Omega }^{\mathbf{A}}F)={\delta }^{\mathbf{A}/{\Omega }^{\mathbf{A}}F}(a/{\Omega }^{\mathbf{A}}F),\text{ for all }a\in F\text{ and }⟨\mathbf{A},F⟩\in \mathsf{M}.$$

$${\epsilon }^{\mathbf{B}}(b)={\delta }^{\mathbf{B}}(b)\text{ for every }⟨\mathbf{B},G⟩\in {\mathsf{Mod}}^{\ast }(⊢)\text{ and }b\in G.$$

$$\mathsf{M}\models \forall x(P(x)\to \epsilon (x)\approx \delta (x)).$$

$${\mathsf{Mod}}^{\ast }(⊢)$$

$$G=\{b\in B:\mathbf{B}\models \mathbf{\tau }(b)\}.$$

$$(C\times C)\cap {\Omega }^{\mathbf{B}}G\subseteq {\Omega }^{\mathbf{C}}(G\cap C).$$

$$C/{\Omega }^{\mathbf{C}}(G\cap C)\models \mathbf{\tau }(b/{\Omega }^{\mathbf{C}}(G\cap C)).$$

$$b/{\Omega }^{\mathbf{C}}(G\cap C)\in (G\cap C)/{\Omega }^{\mathbf{C}}(G\cap C).$$

$$G\supseteq \{b\in B:\mathbf{B}\models \mathbf{\tau }(b)\}$$

$$G\supseteq \{b\in B:\mathbf{B}\models {\mathbf{\tau }}^{\prime }(b)\}.$$

$$\varnothing ⊢\Delta (x,x)\text{ and }x,\Delta (x,y)⊢y.$$

$$\Delta (x,y):=$$

$$\mathbf{\tau }(x):=$$

$$\varnothing$$

$${\Delta }^{\prime }(x_1,y_1)\cup \cdots \cup \Delta$$

$$F\subseteq \{a\in A:\mathbf{A}\models \mathbf{\tau }(a)\}=\{a\in A:\mathbf{A}/{\Omega }^{\mathbf{A}}F\models \mathbf{\tau }(a/{\Omega }^{\mathbf{A}}F)\}.$$

$$b\in G⟺\mathbf{B}\models \mathbf{\tau }(b).$$

$$b\in G⟺\mathbf{B}\models {\mathbf{\tau }}^{\prime }(b).$$

$$\mathbf{B}\models \mathbf{\tau }(b)⟺\mathbf{B}\models {\mathbf{\tau }}^{\prime }(b)$$

$$\Gamma /{\Omega }^{\mathbf{Tm}(x)}\Gamma =\{\phi /{\Omega }^{\mathbf{Tm}(x)}\Gamma \in Tm(x)/{\Omega }^{\mathbf{Tm}(x)}\Gamma :\mathbf{\tau }(\phi )\subseteq {\Omega }^{\mathbf{Tm}(x)}\Gamma \}.$$

Full text

1. Introduction

Abstract algebraic logic is a field that studies uniformly propositional logics [12, 14, 15, 16]. One of its main achievements is the development of the so-called Leibniz hierarchy (see Figure 1), which provides a taxonomy of propositional logics inspired by the idea that logics can be classified accordingly to the definability of logical equivalence and truth predicates. The most prominent example of a class of logics belonging to the Leibniz hierarchy is probably the one of algebraizable logics [8], i.e. logics which are equivalent to equational consequences relative to classes of algebras in the sense of [6, 7].

The role of the Leibniz hierarchy in abstract algebraic logic has been compared [34] to that of the Maltsev hierarchy [18, 27, 36] in universal algebra, where the latter provides a taxonomy of varieties by means of properties typically related to the shape of congruence lattices. Recently, this analogy has been made precise in such a way that the Leibniz hierarchy can be regarded as a natural extension of the Maltsev hierarchy to arbitrary propositional logics [24, 25, 26].

In the context of these considerations, the issue of whether it is actually possible to classify logics in the Leibniz hierarchy seems to deserve special attention. The goal of this paper is to shed light on this question, complementing previous work both in the setting of the Leibniz [29] and Maltsev hierarchies [17] (see also [21]).

It is well known that logics can be defined both syntactically, e.g. by means of Hilbert calculi, and semantically, e.g. by means of (logical) matrices. Accordingly, the problem of classifying logics in the Leibniz hierarchy can be formulated in two versions: for each level $\mathsf{K}$ of the Leibniz hierarchy of Figure 1 we consider the following problems:

Is the logic determined by a given finite Hilbert calculus in $\mathsf{K}$? 2. 2.

Is the logic determined by a given finite matrix in $\mathsf{K}$?

Problem 1 was shown to be undecidable in [29]. On the other hand, Problem 2 turns out to solvable by means of algorithms that run in exponential or double exponential time (Lemmas 3.1 and 3.2), see also [30]. Thus it makes sense to ask which is its computational complexity [2, 31].

The main result of this paper shows that Problem 2 is hard for EXPTIME for every choice of $\mathsf{K}$ in Figure 1 (Theorem 5.5). Since the class EXPTIME is strictly larger than PTIME by the Hierarchy Theorem of Hartmanis and Stearns [20], this implies that these problems are not tractable.

2. The Leibniz hierarchy

This section contains a concise presentation of the main concepts used in the paper; for a systematic exposition we refer the reader to [12, 14, 15, 16]. A matrix is a pair $\langle\bm{A},F\rangle$, where $\bm{A}$ is an algebra and $F\subseteq A$. A congruence $\theta$ of $\bm{A}$ is compatible with $F\subseteq A$, when $F$ is a union of blocks of $\theta$. The largest congruence of $\bm{A}$ compatible with $F$ (which always exists) is denoted by $\bm{\varOmega}^{\bm{A}}F$ and is called the Leibniz congruence of $\bm{A}$ w.r.t. $F$. A matrix $\langle\bm{A},F\rangle$ is reduced when $\bm{\varOmega}^{\bm{A}}F$ is the identity relation. The reduction of $\langle\bm{A},F\rangle$ is the matrix $\langle\bm{A}/\bm{\varOmega}^{\bm{A}}F,F/\bm{\varOmega}^{\bm{A}}F\rangle$. The last matrix is always reduced. Given a class of matrices $\mathsf{K}$, we denote by $\mathsf{K}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}$ the class of isomorphic copies of the reductions of members of $\mathsf{K}$, and by $\mathbb{S}(\mathsf{K})$ the class of substructures of members of $\mathsf{K}$.

A logic $\vdash$ is a substitution invariant closure relation on the set of terms (constructed from a given countable set of variables) of a fixed algebraic language. A logic $\vdash$ is finitary if for every set of formulas $\varGamma\cup\{\varphi\}$,

[TABLE]

Every class $\mathsf{M}$ of matrices determines a logic $\vdash_{\mathsf{M}}$ as follows:

[TABLE]

Observe that a matrix and its reduction determine the same logic. A matrix $\langle\bm{A},F\rangle$ is a model of a logic $\vdash$ when $\vdash\mkern 1.19998mu\subseteq\mkern 1.19998mu\vdash_{\langle\bm{A},F\rangle}$. We denote by $\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$ the class of reduced models of $\vdash$.

The main classes in the Leibniz hierarchy can de defined as follows. A logic $\vdash$ is protoalgebraic if there is a set of formulas $\varDelta(x,y,\vec{z})$ such that for every model $\langle\bm{A},F\rangle$ of $\vdash$ and every $a,b\in A$ we have:

[TABLE]

A logic is equivalential if there exists a set of formulas $\varDelta(x,y)$ without parameters $\vec{z}$, which satisfies condition (1).

A logic $\vdash$ is truth equational if there is a set of equations $\bm{\tau}(x)$ such that for every $\langle\bm{A},F\rangle\in\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$ we have

[TABLE]

Finally, a logic is algebraizable (resp. weakly-algebraizable) when it is equivalential (resp. protoalgebraic) and truth-equational. The Leibniz hierarchy, as described above, is represented in Figure 1 where arrows stand for the inclusion relation.

We will rely on the following observations.

Theorem 2.1**.**

Let $\vdash$ be the logic determined by a finite set of finite matrices $\mathsf{M}$.

$\vdash$* is protoalgebraic if and only if there is a set of formulas $\varDelta(x,y)$ (in variables $x$ and $y$) such that $\emptyset\vdash\varDelta(x,x)$ and $x,\varDelta(x,y)\vdash y$.* 2. 2.

$\vdash$* is equivalential if and only if there is a set of formulas $\varDelta(x,y)$ satisfying the conditions of point 1 and such for every basic $n$-ary operation $f$*

[TABLE]

Moreover, in this case $\varDelta$ satisfies condition (1) for every model of $\vdash$. 3. 3.

$\vdash$* is weakly algebraizable (resp. algebraizable) iff it is protoalgebraic (resp. equivalential) and there is a set of equations $\bm{\tau}(x)$ such that for all $\langle\bm{B},F\rangle\in\mathbb{S}(\mathsf{M})$ and $b\in B$:*

[TABLE]

Proof.

Items 1 and 2 are well-known (see for instance [14]). Thus we detail only the proof of 3. First we claim that if $\vdash$ is protoalgebraic, then $\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)=\mathbb{P}_{\!\textsc{sd}}((\mathbb{S}(\mathsf{M}))^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}})$. To prove this, observe that $\vdash$ is finitary logic, since $\mathsf{M}$ is a finite set of finite matrices [14, Theorem 4.4]. In particular, this implies

[TABLE]

where $\mathbb{P}_{\!\textsc{r}},\mathbb{P}_{\!\textsc{sd}}$ and $\mathbb{P}_{\!\textsc{u}}$ are the class-operators of reduced, subdirect, and ultraproducts [14, Theorem 4.7]. Now, it is not hard to see that $(\mathbb{P}_{\!\textsc{sd}}\mathbb{S}(\mathsf{M}))^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}\subseteq(\mathbb{P}_{\!\textsc{sd}}((\mathbb{S}(\mathsf{M}))^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}))^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}\subseteq\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$. Hence we obtain

[TABLE]

Recall that if $\vdash$ is protoalgebraic, then $\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$ is closed under $\mathbb{P}_{\!\textsc{sd}}$ [14, Theorem 6.17] (see also [9, 11, 13]). Together with the fact that $(\mathbb{S}(\mathsf{M}))^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}\subseteq\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$, this implies that if $\vdash$ is protoalgebraic, then

[TABLE]

establishing the claim.

From the claim it follows that if $\vdash$ is protoalgebraic, then $\vdash$ is truth-equational if and only if there is a set of equations $\bm{\tau}(x)$ such that for all $\langle\bm{B},F\rangle\in\mathbb{S}(\mathsf{M})$ and $b\in B$:

[TABLE]

This easily implies that condition 3 holds. ∎

Lemma 2.2**.**

Let $\vdash$ be the logic determined by a finite set of finite matrices $\mathsf{M}$. Then $\vdash$ is truth-equational if and only if there is a set of equations $\bm{\tau}(x)$ such that for every $\langle\bm{B},G\rangle\in\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$, where $\bm{B}$ is one-generated, and every $\langle\bm{A},F\rangle\in\mathsf{M}$ we have

[TABLE]

In this case, we can take $\bm{\tau}(x)$ to be the set of equations $\varepsilon\thickapprox\delta$ such that

[TABLE]

Proof.

We claim that if $\varepsilon(x)\thickapprox\delta(x)$ is an equation such that $\varepsilon^{\bm{A}/\bm{\varOmega}^{\bm{A}}F}(a/\bm{\varOmega}^{\bm{A}}F)=\delta^{\bm{A}/\bm{\varOmega}^{\bm{A}}F}(a/\bm{\varOmega}^{\bm{A}}F)$ for all $a\in F$ and $\langle\bm{A},F\rangle\in\mathsf{M}$, then

[TABLE]

To prove this, observe that $\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$ can be seen as a class of first-order structures in the algebraic language of $\vdash$ extended with a unary predicate symbol $P(x)$. More precisely, a matrix $\langle\bm{B},G\rangle\in\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$ can be regarded as a first-order structure given by the algebra $\bm{B}$, equipped with the interpretation of $P(x)$ given by the set $G\subseteq B$.

Now, consider a matrix $\langle\bm{B},G\rangle\in\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$, and an equation $\varepsilon\thickapprox\delta$ such that $\varepsilon^{\bm{A}/\bm{\varOmega}^{\bm{A}}F}(a/\bm{\varOmega}^{\bm{A}}F)=\delta^{\bm{A}/\bm{\varOmega}^{\bm{A}}F}(a/\bm{\varOmega}^{\bm{A}}F)$ for all $a\in F$ and $\langle\bm{A},F\rangle\in\mathsf{M}$. We have

[TABLE]

Moreover, as in (3), we have

[TABLE]

Hence $\langle\bm{B},G\rangle$ can be identified with a matrix of the form $\langle\bm{C}/\bm{\varOmega}^{\bm{C}}H,H/\bm{\varOmega}^{\bm{C}}H\rangle$ for some $\langle\bm{C},H\rangle\in\mathbb{P}_{\!\textsc{sd}}\mathbb{S}(\mathsf{M})$.

Then consider an arbitrary element $c\in C$ such that $c/\bm{\varOmega}^{\bm{C}}H\in H/\bm{\varOmega}^{\bm{C}}H$. Since the sentence in (4) is preserved by $\mathbb{P}_{\!\textsc{sd}}$ and $\mathbb{S}$, it holds in $\langle\bm{C},H\rangle$ as well. Together with the fact that $c\in H$, this implies that $\varepsilon^{\bm{C}}(c)=\delta^{\bm{C}}(c)$. Hence we conclude that $\bm{C}/\bm{\varOmega}^{\bm{C}}H\vDash\varepsilon(c/\bm{\varOmega}^{\bm{C}}H)\thickapprox\delta(c/\bm{\varOmega}^{\bm{C}}H)$, establishing the claim.

Now, we move to the proof of the main statement. Indeed, it is enough to prove the “if” part. To this end, suppose that there is a set of equations $\bm{\tau}(x)$ satisfying the assumptions. Then consider an arbitrary matrix $\langle\bm{B},G\rangle\in\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$. In order to prove that $\vdash$ is truth-equational, it will be enough to show that

[TABLE]

From the assumption we know that $F\subseteq\{a\in A:\bm{A}/\bm{\varOmega}^{\bm{A}}F\vDash\bm{\tau}(a/\bm{\varOmega}^{\bm{A}}F)\}$ for every $\langle\bm{A},F\rangle\in\mathsf{M}$. Together with the claim, this implies that $G\subseteq\{b\in B\colon\bm{B}\vDash\bm{\tau}(b)\}$. Conversely, consider $b\in B$ such that $\bm{B}\vDash\bm{\tau}(b)$. Then consider the subalgebra $\bm{C}$ of $\bm{B}$ generated by $b$. As the congruence $(C\times C)\cap\bm{\varOmega}^{\bm{B}}G$ is compatible with $G\cap C$, we obtain

[TABLE]

Together with the fact that $\bm{B}\vDash\bm{\tau}(b)$, this implies

[TABLE]

Now, observe that $\langle\bm{C}/\bm{\varOmega}^{\bm{C}}(G\cap C),(G\cap C)/\bm{\varOmega}^{\bm{C}}(G\cap C)\rangle$ is a reduced model of $\vdash$, and that $\bm{C}/\bm{\varOmega}^{\bm{C}}(G\cap C)$ is one-generated. Hence we can apply the assumption to (5), obtaining

[TABLE]

Since $\bm{\varOmega}^{\bm{C}}(G\cap C)$ is compatible with $G\cap C$, we get that $b\in G\cap C\subseteq G$. Hence we conclude that

[TABLE]

and, therefore, that $\vdash$ is truth equational.

To conclude the proof, suppose that there is a set of equations $\bm{\tau}(x)$ satisfying the condition in the statement. Moreover, let $\bm{\tau}^{\prime}(x)$ be the set of equations $\varepsilon\thickapprox\delta$ such that $\varepsilon^{\bm{A}/\bm{\varOmega}^{\bm{A}}F}(a/\bm{\varOmega}^{\bm{A}}F)=\delta^{\bm{A}/\bm{\varOmega}^{\bm{A}}F}(a/\bm{\varOmega}^{\bm{A}}F)$, for all $a\in F$ and $\langle\bm{A},F\rangle\in\mathsf{M}$. Since $F\subseteq\{a\in A\colon\bm{A}/\bm{\varOmega}^{\bm{A}}F\vDash\bm{\tau}(a\bm{\varOmega}^{\bm{A}}F)\}$ for all $\langle\bm{A},F\rangle\in\mathsf{M}$, we obtain that $\bm{\tau}(x)\subseteq\bm{\tau}^{\prime}(x)$. In particular, this implies that for every $\langle\bm{B},G\rangle\in\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$ such that $\bm{B}$ is one-generated,

[TABLE]

The reverse inclusion follows from the claim at the beginning of the proof. ∎

We will also make use of the following technical lemma:111I am indebted to the referee of my [29] for suggesting a simplification in the proof of Lemma 2.2.

Lemma 2.3**.**

Let $\vdash$ be the logic determined by a reduced matrix $\langle\bm{A},F\rangle$.

If $\bm{A}$ is trivial, then $\vdash$ is weakly algebraizable if and only if $F=A$. 2. 2.

If $\bm{A}$ is non-trivial and all its basic operations are constants, then $\vdash$ is not weakly algebraizable. 3. 3.

If $\bm{A}$ is trivial, then $\vdash$ is truth-equational if and only if $F=A$. 4. 4.

If $\bm{A}$ is non-trivial and all its basic operations are constants, then $\vdash$ is truth-equational if and only if there is a constant ${\bf a}$ which is interpreted inside $F$.

Proof.

1. Observe that if $\bm{A}$ is trivial, then $\vdash$ is either the inconsistent logic, i.e. the logic whose set of tautologies coincides with the set of all formulas, or the almost inconsistent logic, i.e. the logic with empty set of tautologies but such that $\varphi\vdash\psi$ for all formulas $\varphi$ and $\psi$. More in detail, $\vdash$ is inconsistent when $F=A$, and it is almost inconsistent when $F=\emptyset$. From condition 3 of Theorem 2.1 it follows that the inconsistent logic is weakly algebraizable, while the almost inconsistent one is not.

2. Suppose that $\bm{A}$ is non-trivial and that all its basic operations are constants. Since all operations of $\bm{A}$ are constants, the Leibniz congruence of $\langle\bm{A},F\rangle$ has only two blocks, i.e. $F$ and $A\smallsetminus F$. Together with the fact that $\langle\bm{A},F\rangle$ is reduced and that $\bm{A}$ non-trivial, this implies that $\bm{A}$ is a two element algebra, say with universe $\{0,1\}$, and $F=\{1\}$. Hence $\vdash$ is determined by $\langle\bm{A},\{1\}\rangle$.

Suppose towards a contradiction that $\vdash$ is weakly algebraizable. Then there is a set of formulas $\varDelta(x,y)$ as in condition 1 of Theorem 2.1. In particular, this means that

[TABLE]

Due to the poorness of the language of $\bm{A}$, we have that $\varDelta(x,y)$ can contain only constants ${\bf a},{\bf b},{\bf c}\dots$ and the variables $x,y$. Now, since $\varDelta(x,x)$ is a set of tautologies of $\vdash$ and $\vdash$ is determined by $\langle\bm{A},\{1\}\rangle$, we have that ${\bf a}\notin\varDelta(x,y)$ for each constant ${\bf a}$ which is interpreted to [math]. Similarly, as $x$ and $y$ can be interpreted as [math] and $\varDelta(x,x)$ is a set of tautologies, we obtain $x,y\notin\varDelta(x,y)$. Then $\varDelta(x,y)$ is a set of constants that are interpreted to $1$. Hence $\varDelta(x,y)$ is a set of tautologies of $\vdash$, since $\vdash$ is determined by $\langle\bm{A},\{1\}\rangle$. This means that the rule $x,\varDelta(x,y)\vdash y$ specializes to $x\vdash y$, which is easily seen to fail in $\langle\bm{A},\{1\}\rangle$.

3. Suppose that $\bm{A}$ is trivial. If $F=A$, then all reduced models of $\vdash$ are isomorphic to $\langle\bm{A},F\rangle$. Hence $\vdash$ is truth-equational with $\bm{\tau}=\emptyset$. Then suppose that $F=\emptyset$. Observe that there cannot be a set of equations $\bm{\tau}$ whose set of solutions in $\bm{A}$ is empty. Hence $\vdash$ is not truth-equational.

4. Suppose that $\bm{A}$ is non-trivial. As motivated in the proof of condition 2, $\bm{A}$ is a two element algebra, say with universe $\{0,1\}$, and $F=\{1\}$. If no constant symbol of $\bm{A}$ is interpreted to $1$, then $F$ cannot be defined as in (2). Hence $\vdash$ is not truth-equational. On the other hand, if there is a constant ${\bf a}$ which is interpreted to $1$, then $\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$ is the class of isomorphic copies of $\langle\bm{A},F\rangle$ and of the matrix $\langle\bm{B},B\rangle$, where $\bm{B}$ is the trivial algebra. This means that $\vdash$ is truth-equational with $\bm{\tau}(x)\coloneqq\{x\thickapprox{\bf a}\}$. ∎

Recall that if $\bm{A}$ is an algebra, the free $n$-generated algebra $\bm{Tm}(x_{1},\dots,x_{n})$ in the variety generated by $\bm{A}$ is isomorphic to the subalgebra of $\bm{A}^{(A^{n})}$ generated by the projections (see [5] if necessary). Sometimes we tacitly identify the elements of the free algebra $\bm{Tm}(x_{1},\dots,x_{n})$ (i.e. the equivalence classes of formulas with variables among $x_{1},\dots,x_{n}$ that have the same interpretation in $\bm{A}$) with particular formulas $\varphi(x_{1},\dots,x_{n})$ that represent them.

Lemma 2.4**.**

Let $\langle\bm{A},F\rangle$ be a finite reduced matrix, and $\bm{Tm}(x)$, $\bm{Tm}(x,y)$ respectively the free one-generated and the free two-generated algebras over the variety generated by $\bm{A}$. Consider also the following sets of formulas and equations

[TABLE]

The following conditions hold for the logic $\vdash$ determined by $\langle\bm{A},F\rangle$.

$\vdash$* is protoalgebraic iff $\varDelta$ satisfies the requirement in condition 1 of Theorem 2.1.* 2. 2.

$\vdash$* is equivalential iff $\varDelta$ satisfies the requirement in condition 2 of Theorem 2.1.* 3. 3.

$\vdash$* is weakly algebraizable (resp. algebraizable) iff $\vdash$ is protoalgebraic (resp. equivalential) and $\bm{\tau}$ satisfies the requirement in condition 3 of Theorem 2.1.* 4. 4.

$\vdash$* is truth-equational iff $\bm{\tau}$ satisfies the requirement in Lemma 2.2.*

Proof.

1. We have to prove that $\vdash$ is protoalgebraic if and only if $\emptyset\vdash\varDelta(x,x)$ and $x,\varDelta(x,y)\vdash y$. The “if” part is a consequence of Theorem 2.1(1). To prove the “only if” part, suppose that $\vdash$ is protoalgebraic. By condition 1 of Theorem 2.1 there is a set of formulas $\varDelta^{\prime}(x,y)$ such that $\emptyset\vdash\varDelta^{\prime}(x,x)$ and $x,\varDelta^{\prime}(x,y)\vdash y$. Since the logic $\vdash$ is determined by $\langle\bm{A},F\rangle$, we can assume w.l.o.g. that $\varDelta^{\prime}\subseteq Tm(x,y)$. Together with $\emptyset\vdash\varDelta^{\prime}(x,x)$ and the definition of $\varDelta$, this implies $\varDelta^{\prime}\subseteq\varDelta$. Bearing in mind that $x,\varDelta^{\prime}(x,y)\vdash y$, we conclude that $x,\varDelta(x,y)\vdash y$. Finally, the fact that $\emptyset\vdash\varDelta(x,x)$ is an immediate consequence of the definition of $\varDelta$.

2. The “if” part of the statement is a consequence of Theorem 2.1(2). To prove the “only if” part, suppose that $\vdash$ is equivalential. By condition 2 of Theorem 2.1 there is a set $\varDelta^{\prime}(x,y)$ such that

[TABLE]

for every basic $n$-ary operation $f$. To conclude the proof, it will be enough to show that the sets $\varDelta(x,y)$ and $\varDelta^{\prime}(x,y)$ are interderivable in $\vdash$.

As in the proof of 1, we can assume w.l.o.g. that $\varDelta^{\prime}\subseteq\varDelta$. Therefore it only remains to show that $\varDelta^{\prime}(x,y)\vdash\varphi$ for every $\varphi\in\varDelta$. To this end, consider $a,b\in A$ such that $\varDelta^{\prime\bm{A}}(a,b)\subseteq F$. By the last part of condition 2 of Theorem 2.1, this implies $\langle a,b\rangle\in\bm{\varOmega}^{\bm{A}}F$. Since $\langle\bm{A},F\rangle$ is reduced, we conclude that $a=b$. Together with the definition of $\varDelta$, this implies $\varDelta^{\bm{A}}(a,b)=\varDelta^{\bm{A}}(a,a)\subseteq F$. Since $\vdash$ is the logic determined by $\langle\bm{A},F\rangle$, we conclude that $\varDelta^{\prime}(x,y)\vdash\varphi$ for all $\varphi\in\varDelta(x,y)$.

4. The “if” part of the statement is a consequence of Lemma 2.2. To prove the “only if” part, suppose that $\vdash$ is truth-equational. From the definition of $\bm{\tau}$ and the fact that $\langle\bm{A},F\rangle$ is reduced it follows that

[TABLE]

Then consider $\langle\bm{B},G\rangle\in\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$ such that $\bm{B}$ is one-generated. It only remains to prove that for every $b\in B$,

[TABLE]

To this end, consider a matrix $\langle\bm{B},G\rangle\in\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$ such that $\bm{B}$ is one-generated. Moreover, let $\bm{\tau}^{\prime}$ be the set of equations $\varepsilon(x)\thickapprox\delta(x)$ such that $\varepsilon^{\bm{A}}(a)=\delta^{\bm{A}}(a)$ for every $a\in F$. Since $\vdash$ is truth-equational, we can apply the last part of the statement of Lemma 2.2 and the fact that $\langle\bm{A},F\rangle$ is reduced obtaining that for every $b\in B$,

[TABLE]

Now, as in (3), $\bm{B}$ belongs to the variety generated by $\bm{A}$. As a consequence,

[TABLE]

for every $b\in B$. Together with (7), this implies (6) as desired.

3. We detail the case of weakly algebraizable logics only. The “if” part of the statement is a consequence of Theorem 2.1(3). To prove the “only if” part, suppose that $\vdash$ is weakly algebraizable. Clearly, $\vdash$ is protoalgebraic. Moreover, since $\vdash$ is truth-equational, we can apply point 4 yielding that $\bm{\tau}$ satisfies the conditions in Lemma 2.2. This clearly implies that $\bm{\tau}$ satisfies the (weaker) requirement in Theorem 2.1(3). ∎

3. Upper bounds

We begin by establishing some upper bound to the computational complexity of the problem of classifying logics determined by a finite reduced matrix of finite type into the Leibniz hierarchy of Figure 1. To this end, let us explain how we represent the inputs of this problem, that is how we represent finite matrices $\langle\bm{A},F\rangle$. The finite set $A$ could be represented by its cardinality, say $n$ (and $A$ can be taken to be $\{1,\dots,n\}$). A $k$-ary operation can be represented as a $k$-dimensional array of elements of $A$, i.e. a sequence of $n^{k}$ elements of $A$. Finally, $F$ can be represent by a natural number $m\leqslant n$, indicating that $F=\{k\in\omega:1\leqslant k\leqslant m\}$ (observe that $F=\emptyset$, when $m=0$).

The next result identifies upper bounds to the complexity of the problem of determining whether the logic of a finite reduced matrix is algebraizable:

Lemma 3.1**.**

The problem of determining whether the logic of a finite reduced matrix of finite type is algebraizable (resp. equivalential, protoalgebraic, weakly algebraizable) is in EXPTIME.

Proof.

We detail the proof for the case of weakly algebraizable logics. Consider a finite reduced matrix $\langle\bm{A},F\rangle$ of finite type, and let $\vdash$ be the logic it defines. Moreover, let $\varDelta$ and $\bm{\tau}$ be the sets defined in Lemma 2.4. In order to determine whether $\vdash$ is weakly algebraizable or not, it is enough to check whether $\varDelta$ and $\bm{\tau}$ satisfy, respectively, the requirement in condition 1 and 3 of Theorem 2.1 (see conditions 1 and 3 of Lemma 2.4 if necessary). This task can be done mechanically, since the free algebras $\bm{Tm}(x)$ and $\bm{Tm}(x,y)$ in the variety generated by $\bm{A}$ are finite and of size at most $|A^{A^{2}}|$.

It only remains to show that this test can be carried on in exponential time. To this end, let us describe it in more detail. The algorithm starts reading the input $\langle\bm{A},F\rangle$. If it reads that $\bm{A}$ is trivial, then it checks whether $F$ is empty or not and provides an output according to point 1 of Lemma 2.3. If $\bm{A}$ is non-trivial, then the algorithm starts checking whether $\bm{A}$ has a basic operation, which is not a constant. If this is not the case, then the algorithm establishes that $\vdash$ is not weakly algebraizable according to point 2 of Lemma 2.3. This process takes time $O(n)$, where $n$ is the length of the input.

If the algorithm does not have halted yet, then $\bm{A}$ is non-trivial and has a basic operation, which is not a constant. In particular, this means that the length $n$ of the input dominates the cardinality of $\bm{A}$. First we need to construct the sets $Tm(x)$ and $Tm(x,y)$ respectively of all unary and binary term-functions of $\bm{A}$. This task amounts to that of constructing the one-generated and the two-generated free algebras of the variety generated by $\bm{A}$ (which are isomorphic to subalgebras of $\bm{A}^{A}$ and $\bm{A}^{(A^{2})}$, respectively). Since $n$ dominates the cardinality of $\bm{A}$, the time needed in the construction of $Tm(x)$ and $Tm(x,y)$ can be bounded exponentially in $n$. Thus the sets $\varDelta$ and $\bm{\tau}$ can be constructed in exponential time in $n$.

By Lemma 2.4(1), $\vdash$ is protoalgebraic if and only if $\varDelta$ satisfies the right-hand side of condition 1 of Theorem 2.1. Then the algorithm checks if this is the case or not (which can be done in exponential time). Accordingly, if $\vdash$ is not protoalgebraic, the algorithm stops and provides a negative answer.

If $\vdash$ is protoalgebraic, then by Lemma 2.4(3) the logic $\vdash$ is weakly algebraizable if and only if $\bm{\tau}$ satisfies the requirement in the display of condition 3 of Theorem 2.1. To this end, we construct all substructures $\langle\bm{B},G\rangle$ of $\langle\bm{A},F\rangle$ (which can be done in exponential time). For each such submatrix $\langle\bm{B},G\rangle$, the Leibniz congruence $\bm{\varOmega}^{\bm{B}}G$ can be computed in $n\log n$ time.222This is justified as follows. First observe that the matrix $\langle\bm{B},G\rangle$ can be transformed into an automaton $\langle\bm{B}^{+},G\rangle$, where $\bm{B}^{+}$ is the algebra with universe $B$ and whose basic operations are the unary functions of the form $f^{\bm{B}}(b_{1},\dots,b_{n},x,b_{n+1},\dots,b_{m})$ for some $\vec{b}\in B$ and some basic operation $f$ of $\bm{B}$. Observe that the length of $\langle\bm{B}^{+},G\rangle$ is essentially the same of $\langle\bm{B},G\rangle$, i.e. $n$. Now, it is known that the task of computing the Leibniz congruence $\bm{\varOmega}^{\bm{B}}G$ amounts to that of minimizing the number of states of the automaton $\langle\bm{B}^{+},G\rangle$. Since the time needed to solve the latter task is bounded above by $n\log n$ [23], we are done. Finally, for every $\langle\bm{B},G\rangle$, checking the requirement in the display of condition 3 of Theorem 2.1 is an easy task. If this requirement holds, then the algorithm provides a positive answer, otherwise it provides a negative one.

A similar argument shows that the problem of determining whether the logic of a finite reduced matrix of finite type is equivalential (resp. protoalgebraic, algebraizable) belongs to EXPTIME. ∎

The next result identifies upper bounds to the complexity of determining whether the logic of a finite reduced matrix is truth-equational:

Lemma 3.2**.**

The problem of determining whether the logic of a finite reduced matrix of finite type is truth-equational is in ${\bf 2}$-EXPTIME.

Proof.

Let $\langle\bm{A},F\rangle$ be a finite reduced matrix of finite type, and let $\vdash$ be the logic it determines. Let also $\bm{\tau}$ be the set of equations in the statement of Lemma 2.4. In order to determine whether $\vdash$ is truth-equational or not, it is enough to check whether $\bm{\tau}$ satisfies the requirement in Lemma 2.2 (see conditions 4 of Lemma 2.4 if necessary).

We proceed to explain why this task can be done mechanically. First observe that the free one-generated algebra $\bm{Tm}(x)$ in the variety generated by $\bm{A}$, and the set $\bm{\tau}$ can be constructed mechanically as in the proof of Lemma 3.1. Then we construct all sets $\varGamma\subseteq Tm(x)$ such that $\langle\bm{Tm}(x),\varGamma\rangle$ is a model of $\vdash$. Then, we check whether for every such $\varGamma$ we have that

[TABLE]

Observe that the above equality can be checked mechanically, since $\bm{Tm}(x)$ is a finite algebra. The test says that $\vdash$ is truth-equational, if the above condition holds, and it says that $\vdash$ is not truth-equational otherwise.

The fact that this test works as expected is guaranteed by the following argument. As remarked in the proof of Lemma 2.2, we have that

[TABLE]

In particular, this means that the algebraic reducts of $\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$ belong to the variety generated by $\bm{A}$. This observations has two consequences. On the one hand, it means that the free one-generated algebra of the variety generated by the algebraic reducts of $\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$ is indeed $\bm{Tm}(x)$. On the other hand, it implies that the reduced models $\langle\bm{B},G\rangle$ of $\vdash$ such that $\bm{B}$ is one-generated are (up to isomorphism) the ones of the form $\langle\bm{Tm}(x)/\bm{\varOmega}^{\bm{Tm}(x)}\varGamma,\varGamma/\bm{\varOmega}^{\bm{Tm}(x)}\varGamma\rangle$ where $\varGamma\subseteq Tm(x)$ is such that $\langle\bm{Tm}(x),\varGamma\rangle$ is a model of $\vdash$. Hence our test amounts to checking whether $\bm{\tau}$ satisfies the requirement in the statement of Lemma 2.2.

It only remains to show that this test can be carried on in double exponential time. To this end, let us describe it in more detail. The algorithm starts reading the input $\langle\bm{A},F\rangle$. If it reads that $\bm{A}$ is trivial, then it checks whether $F$ is empty or not, and provides an output according to condition 3 of Lemma 2.3. If $\bm{A}$ is non-trivial, then the algorithm starts checking whether all a basic operations of $\bm{A}$ are constants. If this is the case, then the algorithm checks whether at least one of them is interpreted inside $F$ and provides an output according to condition 4 of Lemma 2.3. This process takes time $O(n)$, where $n$ is the length of the input $\langle\bm{A},F\rangle$.

If the algorithm does not have halted yet, then $\bm{A}$ is non-trivial and has a basic operation, which is not a constant. In particular, this means that the length $n$ of the input dominates the cardinality of $\bm{A}$. From now on we just apply the algorithm described at the beginning of the proof. First observe that $\bm{\tau}$ and $\bm{Tm}(x)$ can be constructed in exponential time in $n$, as in the proof of Lemma 3.1.

Then we need to construct all sets $\varGamma\subseteq Tm(x)$ such that $\langle\bm{Tm}(x),\varGamma\rangle$ is a model of $\vdash$. This computation requires a number of constructions of order

[TABLE]

since the number of subsets $\varGamma\subseteq Tm(x)$ is bounded above by $2^{n^{n}}$, and for each of $\varGamma\subseteq Tm(x)$ we have to check that every formula $\varphi\in Tm(x)$ (there are at most $n^{n}$ of them) such that $\varGamma\vdash\varphi$ belongs to $\varGamma$ (checking whether $\varGamma\vdash\varphi$ involves at most $n$ assignments of the variable $x$ in $\bm{A}$, since $n$ dominates the cardinality of $A$). Since all these constructions can be carried on in polynomial time in the length $n$ of the input, we conclude that constructing all the sets $\varGamma\subseteq Tm(x)$ such that $\langle\bm{Tm}(x),\varGamma\rangle$ is a model of $\vdash$ takes at most double exponential time in $n$.

Let $\langle\bm{Tm}(x),\varGamma\rangle$ be a model of $\vdash$. As shown in the proof of Lemma 3.1, the Leibniz congruence $\bm{\varOmega}^{\bm{Tm}(x)}\varGamma$ can be computed in $m\log m$ time in the length of $\bm{\varOmega}^{\bm{Tm}(x)}\varGamma$, which is bounded by $2^{p(n)}$ for some polynomial $p(n)$. Bearing this in mind, the time needed in the construction of $\bm{\varOmega}^{\bm{Tm}(x)}\varGamma$ is bounded above by $2^{q(n)}$ for some polynomial $q(n)$. Finally, for every $\varGamma$ and $\varphi$, checking condition (8) is an easy task. The analysis done so far shows that the time needed in the whole computation can be bounded above by $2^{2^{t(n)}}$ for some polynomial $t(n)$. ∎

A logic is said to be strongly finite when it is determined by a finite set of finite matrices of finite type.333In some works the assumption of the finiteness of the type is dropped. The next result provides upper bounds to the problem of classifying strongly finite logics in the Leibniz hierarchy of Figure 1.

Corollary 3.3**.**

The problem of determining whether the logic of a finite set of finite matrices of finite type is algebraizable (resp. equivalential, protoalgebraic, weakly algebraizable) is in EXPTIME. The analogous problem for truth-equationality is in 2-EXPTIME.

Proof.

The proof is a straightforward adaptation of those of Lemmas 3.1 and 3.2. The only significant difference is that, in this case, the input is a set of matrices $\mathsf{M}$ which are not necessarily reduced. For this reason, we need to replace the set $\mathsf{M}$ with the set of reductions of its members. This amounts to compute some Leibniz congruences, and can be done efficiently (as explain in the proof of Lemma 3.1). ∎

4. Two fundamental constructions

In this section $\bm{A}$ is a fixed non-trivial algebra with basic operations $\mathcal{F}$, and $h$ is a unary function on $A$. For sake of simplicity, we assume that $\mathcal{F}$ contains no constant symbols. Our goal is to define two algebras $\bm{A}^{\natural}$ and $\bm{A}^{\flat}$ related to $\bm{A}$. The construction of these algebras presents some relation with the ones introduced in [21] and [17] to prove hardness results related to the study of type sets in tame congruence theory [22] and to the study of Maltsev conditions [19, 36].

We begin by the definition of $\bm{A}^{\natural}$. The universe of $\bm{A}^{\natural}$ is given by eight disjoint copies $A_{1},\dots,A_{8}$ of $A$. Given an element $a\in A$, we will denote by $a^{i}$ its copy in $A_{i}$. In this sense an arbitrary finite set of elements in $A^{\natural}$ can be denoted as $\{a_{1}^{m_{1}},\dots,a_{n}^{m_{n}}\}$ for some $a_{1},\dots,a_{n}\in A$ and $m_{1},\dots,m_{n}\leqslant 8$. The basic operations of $\bm{A}^{\natural}$ are the ones in $\mathcal{F}$ plus a new ternary operation $\heartsuit$ and a new unary operation $\square$. Their interpretation is defined as follows. Given an $n$-ary operation $f\in\mathcal{F}$ and $a_{1}^{m_{1}}\dots,a_{n}^{m_{n}}\in A^{\natural}$, we set

[TABLE]

Observe that all the operations $f^{\bm{A}^{\natural}}$ with $f\in\mathcal{F}$ give values in $A_{5}$. Given $a^{m},b^{n},c^{k}\in A^{\natural}$, we set

[TABLE]

Given $a^{m}\in A^{\natural}$, we set

[TABLE]

Then we turn to define the algebra $\bm{A}^{\flat}$. The universe of $\bm{A}^{\flat}$ is given by two disjoint copies $A_{1},A_{2}$ of $A$ plus two fresh elements $\{0,1\}$. The basic operation of $\bm{A}^{\flat}$ are the ones in $\mathcal{F}$ plus a new binary operation $+$, a new unary operation $\square^{a}$ for every $a\in A$, and a new constant symbol $\bm{1}$. Their interpretation is defined as follows. The constant $\bm{1}$ denotes the element $1$. Given an $n$-ary operation $f\in\mathcal{F}$ and $b_{1},\dots,b_{n}\in A^{\flat}$, we set

[TABLE]

Moreover, for every $a,b\in A^{\flat}$ we set

[TABLE]

Finally, for every $a\in A$ and $b\in A^{\flat}$ we set

[TABLE]

Now, consider the matrices $\langle\bm{A}^{\natural},F^{\natural}\rangle$ and $\langle\bm{A}^{\flat},G^{\flat}\rangle$ where

[TABLE]

Lemma 4.1**.**

The matrices $\langle\bm{A}^{\natural},F^{\natural}\rangle$ and $\langle\bm{A}^{\flat},G^{\flat}\rangle$ are reduced.

Proof.

Observe that, to prove that an arbitrary matrix $\langle\bm{B},H\rangle$ is reduced, it is enough to show that for every pair of different elements $a,b\in B$ there is a unary polynomial function $p(x)$ such that

[TABLE]

To prove that (9) holds for $\langle\bm{A}^{\natural},F^{\natural}\rangle$ we reason as follows. Consider two distinct elements $a^{n},b^{m}\in A^{\natural}$. Then consider the unary polynomial function

[TABLE]

It is clear that $p(a^{n})\in F^{\natural}$, while $p(b^{m})\notin F^{\natural}$. Hence $\langle\bm{A}^{\natural},F^{\natural}\rangle$ is reduced.

Then we turn to prove that (9) holds for $\langle\bm{A}^{\flat},G^{\flat}\rangle$ too. To this end, consider two different $a,b\in A^{\flat}$. If $a\in G^{\flat}$ and $b\notin G^{\flat}$, then we are done. Then suppose that either $a,b\in G^{\flat}$ or $a,b\notin G^{\flat}$. First consider the case where $a,b\notin G^{\flat}$. We can assume w.l.o.g. that $a=c^{2}$ for some $c\in A$. Then we have that $\square^{c}(a)=c^{1}\in G^{\flat}$, while $\square^{c}(b)=b\notin G^{\flat}$. Then suppose that $a,b\in G^{\flat}$. W.l.o.g. we have the following cases:

$a=1$ and $b\neq 1$. 2. 2.

$1\notin\{a,b\}$.

1. Since $\bm{A}$ is non-trivial, there is $c\in A$ such that $b\neq c^{1}$. Then observe that $\square^{c}(a)=0\notin G^{\flat}$, while $\square^{c}(b)=b\in G^{\flat}$.

2. Then observe that $a=c^{1}$ and $b=d^{1}$ for some different $c,d\in A$. We have that $\square^{c}(a)=c^{2}\notin G^{\flat}$, while $\square^{c}(b)=b\in G^{\flat}$. ∎

Lemma 4.2**.**

There is an algorithm that transform inputs $\langle\bm{A},h\rangle$ of $\textsf{Gen-Clo}^{1}_{3}$ into matrices $\langle\bm{A}^{\natural},F^{\natural}\rangle$ (resp. $\langle\bm{A}^{\flat},G^{\flat}\rangle$) and runs in polynomial time in the length of the input.

Proof.

We detail the case of $\langle\bm{A}^{\natural},F^{\natural}\rangle$ only. Observe that a typical input of $\textsf{Gen-Clo}^{1}_{3}$ is a pair $\langle\bm{A},h\rangle$, where $\bm{A}$ is an algebra without constant symbols. Therefore it makes sense to transform it into a matrix of the form $\langle\bm{A}^{\natural},F^{\natural}\rangle$. Now, it is clear that this translation can be given an algorithmic form. Therefore, it only remains to prove that it runs in polynomial time. The only non-trivial part is that the length of the output $\langle\bm{A}^{\natural},F^{\natural}\rangle$ should be bounded by a polynomial in the length $n$ of the input $\langle\bm{A},h\rangle$.  Since $h$ is unary, we know that $n$ dominates the cardinality of $\bm{A}$. Moreover, $\bm{A}$ has at most $n$ basic operations, all of arity at most $3$. Thus $\bm{A}^{\natural}$ is an algebra of cardinality at most $8n$, with at most $n+2$ basic operations, all of arity at most $3$. Hence the length of $\bm{A}^{\natural}$ is bounded above by $8n+(n+2)\cdot(8n)^{3}$. Thus the length of $\langle\bm{A}^{\natural},F^{\natural}\rangle$ is bounded by $8n+(n+2)\cdot(8n)^{3}+8n$. ∎

5. Hardness results

In this section we prove that the problem of determining whether the logic of a finite reduced matrix of finite type belongs to any level of the Leibniz hierarchy of Figure 1 is hard for EXPTIME. To this end, we will make use of the following purely algebraic decision problem related to clones [3, 28]:

1. •

$\textsf{Gen-clo}^{1}_{3}$: Given a finite non-trivial algebra $\bm{A}$ with finitely many basic operations $\mathcal{F}$, whose arities belong to the set $\{1,2,3\}$, and a unary operation $h$ on $A$ different from the identity, is $h$ in the clone of $\bm{A}$?

It is clear that $\textsf{Gen-clo}^{1}_{3}$ is decidable by means of a procedure which runs in exponential time. Remarkably, this procedure is the best possible [4, Theorem 3.7]:444Observe that [4, Theorem 3.7] states that a slightly different problem is complete for EXPTIME. But the proof given there shows that the same result holds for $\textsf{Gen-clo}^{1}_{3}$.

Theorem 5.1**.**

The problem $\textsf{Gen-clo}^{1}_{3}$ is complete for EXPTIME.

The proof of the next lemma relies on a series of technical results and one definition contained in the Appendix.

Lemma 5.2**.**

Let $\bm{A}$ be a non-trivial algebra without constant symbols, $h$ be a unary operation on $A$ other than the identity, and $\vdash$ be the logic determined by the matrix $\langle\bm{A}^{\natural},F^{\natural}\rangle$. The following conditions are equivalent:

1. (i)

$\vdash$* is algebraizable.* 2. (ii)

$\vdash$* is weakly algebraizable.* 3. (iii)

$\vdash$* is equivalential.* 4. (iv)

$\vdash$* is protoalgebraic.* 5. (v)

$h$* is in the clone of $\bm{A}$.*

Proof.

The implications (i)$\Rightarrow$(ii), (i)$\Rightarrow$(iii), (ii)$\Rightarrow$(iv) and (iii)$\Rightarrow$(iv) are straightforward. (v)$\Rightarrow$(i): Let $\varphi(x)$ be a term of $\bm{A}$ representing $h$ on $A$. Since $h$ is not the identity, we have that $\varphi(x)\neq x$. We consider the same term in the algebra $\bm{A}^{\natural}$. Then consider the following sets:

[TABLE]

Bearing in mind that $\varphi(x)\neq x$, it is an easy exercise to check that for every $a,b\in A^{\natural}$ we have that

[TABLE]

By condition 3 of Theorem 2.1 we conclude that $\vdash$ is algebraizable.

(iv)$\Rightarrow$(v): Suppose that $\vdash$ is protoalgebraic. This means that there is a set $\varDelta(x,y)$ satisfying the conditions in point 1 of Theorem 2.1. Since $\vdash$ is neither inconsistent nor almost-inconsistent, we know that $\varDelta\neq\emptyset$ and that no variable belongs to $\varDelta$. Pick any element $a\in A$. We know that $\{a^{1}\}\cup\varDelta(a^{1},a^{1})\subseteq F$, since $\emptyset\vdash\varDelta(x,x)$. Together with the fact that $x,\varDelta(x,y)\vdash y$ and that $a^{3}\notin F^{\natural}$, this implies that there is $\varphi(x,y)\in\varDelta$ such that $\varphi(a^{1},a^{1})\in F^{\natural}$ and $\varphi(a^{1},a^{3})\notin F$.

Observe that $\emptyset\vdash\varphi(x,x)$. In particular, we have that $\varphi(a^{3},a^{3})\in F^{\natural}$. Together with the definition of $\bm{A}^{\natural}$, this implies that $\varphi(x,y)=\square^{m}\heartsuit(\psi_{1},\psi_{2},\psi_{3})$ for some $m\in\omega$ and formulas $\psi_{1},\psi_{2}$ and $\psi_{3}$. We can assume w.l.o.g. that $m=0$, since $\square x\vdash x$ and $x\vdash\square x$. The fact that $\varphi(x,x)$ is a tautology of $\vdash$ implies that

[TABLE]

Again looking at the definition of $\bm{A}^{\natural}$, this implies that $\psi_{2}=\square^{2k}f(\varepsilon_{1},\dots,\varepsilon_{n})$ for some $f\in\mathcal{F}$, formulas $\varepsilon_{i}$ and $k\in\omega$. In particular, we can assume w.l.o.g. that $k=0$, since $\bm{A}^{\natural}\vDash\square^{2k}f(\varepsilon_{1},\dots,\varepsilon_{n})\thickapprox f(\varepsilon_{1},\dots,\varepsilon_{n})$. To every formulas $\varepsilon_{i}$ we associate a new formula $\delta_{i}$ written only with the symbols of $\mathcal{F}$. This is done as follows: first we delete from $\varepsilon_{i}$ all occurrences of $\square$, and then we replace every occurrence of $\heartsuit(\chi_{1},\chi_{2},\chi_{3})$ by $\chi_{1}$. This concludes the definition of $\delta_{i}$. Observe that for every $b,c\in A^{\natural}$ there is $a\in A$ such that

[TABLE]

In particular, this implies that for every $b,c\in A^{\natural}$ we have

[TABLE]

Thus we can assume w.l.o.g. that $\psi_{2}=f(\delta_{1},\dots,\delta_{n})$.

Now, recall that $\varphi(a^{1},a^{1})\in F$, while $\varphi(a^{1},a^{3})\notin F$. In particular, we have that $\varphi(a^{1},a^{1})\neq\varphi(a^{1},a^{3})$. Then we can apply Lemma 6.7, obtaining that $\varphi(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$. Together with Lemmas 6.4 and 6.3 this implies that

[TABLE]

Pick $b^{n}\in A^{\natural}$. In particular, we have that $\psi_{1}(b^{n})=b^{m}$ for some $m\leqslant 8$. Together with condition (10) this implies that

[TABLE]

Recall that $f(\delta_{1},\dots,\delta_{n})$ is a formula written only with symbols in $\mathcal{F}$. Hence we obtain that

[TABLE]

for every $b\in A$. This means that the term $f(\delta_{1},\dots,\delta_{n})(x,x)$ represents $h$ in $\bm{A}$, i.e. $h$ belongs to the clone of $\bm{A}$. ∎

Let $\bm{\tau}$ be a set of equations in variable $x$. A class of algebras $\mathsf{K}$ is a $\bm{\tau}$-algebraic semantics for a logic $\vdash$ [8, 10, 33] if for every set of formulas $\varGamma\cup\{\varphi\}$, we have:

[TABLE]

where $\vDash_{\mathsf{K}}$ is the equational consequence relative to $\mathsf{K}$. In what follows we will make use of the following result [33, Proposition 39]:

Theorem 5.3**.**

Let $\vdash$ be a logic with a $\bm{\tau}$-algebraic semantics. Suppose that $\bm{\tau}$ contains an equation $\varepsilon\thickapprox\delta$ such that $\delta(x)\vdash x$ and $\emptyset\vdash\varepsilon(x)$. Then $\vdash$ is truth-equational by means of $\delta(x)\thickapprox\varepsilon(x)$.

Lemma 5.4**.**

Let $\bm{A}$ be a non-trivial algebra without constant symbols, $h$ be a unary operation of $A$, and $\vdash$ be the logic determined by the matrix $\langle\bm{A}^{\flat},G^{\flat}\rangle$. $\vdash$ is truth-equational if and only if $h$ is in the clone of $\bm{A}$.

Proof.

We begin by the “if” part. Let $t(x)$ be the term that represents $h$ in $\bm{A}$. Then define $\delta\coloneqq x+t(x)$ and $\varepsilon\coloneqq\bm{1}$. Moreover, set $\bm{\tau}\coloneqq\{\delta(x)\thickapprox\varepsilon(x)\}$. Observe that the set of equations $\bm{\tau}$ defines $G^{\flat}$ in $\bm{A}^{\flat}$. Thus the class $\mathsf{K}=\{\bm{A}^{\flat}\}$ is a $\bm{\tau}$-algebraic semantics for $\vdash$. Moreover, observe that $\delta(x)\vdash x$ and $\emptyset\vdash\varepsilon(x)$. Therefore we can apply 5.3 yielding that $\vdash$ is truth-equational.

Then we turn our attention to the “only if” part. Suppose that $\vdash$ is truth-equational. Observe that the matrix $\langle\bm{A}^{\flat},G^{\flat}\rangle$ is reduced by Lemma 4.1. Then we can use the technique described in the proof of Lemma 3.2 to produce a set of equations $\bm{\tau}$ that satisfies condition (2), namely

[TABLE]

Since $\langle\bm{A}^{\flat},G^{\flat}\rangle$ is reduced and $0\in G^{\flat}$, there is an equation $\varepsilon\thickapprox\delta\in\bm{\tau}$ such that $\varepsilon(0)\neq\delta(0)$. Looking at the definition of the basic operations of $\bm{A}^{\flat}$ we obtain that for every formula $\gamma(x)$, if $x$ really occurs in $\gamma$, then $\gamma(0)=0$. Then either $x$ does not occur in $\varepsilon$ or $x$ does not occur in $\delta$. We assume w.l.o.g. that $x$ does not occur in $\varepsilon$. This means that $\varepsilon$ is a closed term, i.e. a term of the form $t(\bm{1},\dots,\bm{1})$ for some term $t(x_{1},\dots,x_{n})$. In particular, we have that $\bm{A}^{\flat}\vDash t(\bm{1},\dots,\bm{1})\thickapprox\bm{1}$. Together with the definition of $\bm{\tau}$, this implies that the equation $\delta(x)\thickapprox\bm{1}$ belongs to $\bm{\tau}$.

Now, we claim that the symbol $\square^{a}$ does not appear in $\delta(x)$, for every $a\in A$. To prove this, we will show by induction on the construction of $\delta$ that if the operation $\square^{a}$ appears in $\delta$, then $\delta(1)=0$. The case where $\delta$ is a variable is satisfied. Then suppose that $\delta=f(\varphi_{1},\dots,\varphi_{n})$ for some $f\in\mathcal{F}$ and that $\square^{a}$ appears in $\delta$. Then $\square^{a}$ appears in some $\varphi_{i}$. By the inductive hypothesis we have that $\varphi_{i}(1)=0$. Hence we conclude that

[TABLE]

The case where $\delta=\varphi+\psi$ is handled analogously. Finally, consider the case where $\delta=\square^{a}\varphi$. Observe that $\varphi(1)\in\{0,1\}$, since $\{0,1\}$ is the universe of a subalgebra of $\bm{A}^{\flat}$. Then $\square^{a}(\varphi(1))=0$ as desired. This concludes the inductive proof. Now, recall that $1\in G^{\flat}$ and, therefore, that $\delta(1)=1$. Hence we conclude that $\square^{a}$ does not appear in $\delta$, for every $a\in A$.

We are in the following situation: there is an equation $\delta\thickapprox\bm{1}$ in $\bm{\tau}$ which satisfies the following requirements:

$\square^{a}$ does not appear in $\delta$. 2. 2.

$\delta$ is neither a closed term nor a variable.

The second condition above follows from the fact that $\delta(0)\neq 1$ and that $\delta(a)=1$ for all $a\in A_{1}$. Conditions 1 and 2 imply that the principal symbol of $\delta$ must be either $f\in\mathcal{F}$ or $+$. If it is $f\in\mathcal{F}$, then $\delta=f(\varphi_{1},\dots,\varphi_{n})$ for some formulas $\varphi_{1},\dots,\varphi_{n}$. Looking at the definition of $f$ in $\bm{A}^{\flat}$, one sees that $\varphi_{i}(a)=1$ for every $a\in G^{\flat}$. In particular, this means that all the equations $\varphi_{i}\thickapprox\bm{1}$ belong to $\bm{\tau}$. Moreover, the fact that $\varphi_{i}(a)=1$ for all $a\in A_{1}$ implies that $\varphi_{i}$ is not a variable. Finally, there must be at least one formula $\psi=\varphi_{i}$, which is not a closed term. Then this formula $\psi$ satisfies conditions 1 and 2 and, moreover, the equation $\psi\thickapprox\bm{1}$ belongs to $\bm{\tau}$. Then consider the case where the principal symbol of $\delta$ is $+$, i.e. $\delta=\varphi+\psi$ for some terms $\varphi$ and $\psi$. Suppose that $\varphi$ is not a variable. The fact that the symbol $\square^{a}$ does not appear in $\varphi$ for every $a\in A$ implies that $\varphi(a)\in A_{2}\cup\{0,1\}$ for every $a\in A^{\flat}$. Together with the fact that $\delta(a)=1$ for every $a\in G^{\flat}$, this implies that $\varphi(a)=1=\psi(a)$ for every $a\in G^{\flat}$. This means that both the equations $\varphi\thickapprox\bm{1}$ and $\psi\thickapprox\bm{1}$ belong to $\bm{\tau}$. Suppose that $\varphi$ does not satisfy condition 2. Since $\varphi$ cannot be a variable (since $\varphi(a)=1$ for all $a\in A_{1}$), we conclude that $\varphi$ is the constant $\bm{1}$. Since $\delta$ is not a closed term, this implies that $\psi$ is not a closed term. Moreover, $\psi$ cannot be a variable (since $\varphi(a)=1$ for all $a\in A_{1}$). Hence we conclude that $\psi$ satisfies condition 2. Thus $\psi$ satisfies conditions 1 and 2 and, moreover, the equation $\psi\thickapprox\bm{1}$ belongs to $\bm{\tau}$. Until now we have shown that either $\delta$ is of the form of $x+\psi$ or we can extract from it a proper subformula $\gamma$ which again satisfies conditions 1 and 2, and the equation $\gamma\thickapprox\bm{1}$ belongs to $\bm{\tau}$. The same argument shows that either $\gamma$ is of the form $x+\psi$ or we can extract from it a proper subformula $\gamma^{\prime}$, which satisfies conditions 1 and 2, and the equation $\gamma^{\prime}\thickapprox\bm{1}$ belongs to $\bm{\tau}$. Iterating this process we obtain a formula $x+\psi(x)\thickapprox\bm{1}$ which belongs $\bm{\tau}$ and in which the symbols $\square^{a}$ do not occur.

Consider any element $a^{1}\in A_{1}$. Since $a^{1}\in G^{\flat}$, we have that $a^{1}+\psi(a^{1})=1$. This means that $\psi(a^{1})=h(a)^{2}$. In particular, observe that if the symbols $+$ or $\bm{1}$ appear in $\psi$, then we would have that $\psi(a^{1})\in\{0,1\}$, which is not the case. Thus the symbols $+$, $\bm{1}$ and $\square^{a}$ do not occur in $\psi$. This means that $\psi$ is written with symbols among $\mathcal{F}$. Then for every $a\in A$ we have that

[TABLE]

Hence $\psi$ represents $h$ in $\bm{A}$, i.e. $h$ belongs to the clone of $\bm{A}$ as desired. ∎

We are now ready to state the main result of the paper:

Theorem 5.5**.**

Let $\mathsf{K}$ be a level in the Leibniz hierarchy of Figure 1. The problem of determining whether the logic of a finite reduced matrix of finite type belongs to $\mathsf{K}$ is hard for EXPTIME.

Proof.

Let $\mathsf{K}$ be a level in the Leibniz hierarchy of Figure 1. By Lemmas 5.2 and 5.4 there is a many-one reduction of $\textsf{Gen-Clo}^{1}_{3}$ to the problem of determining whether the logic of a finite reduced matrix of finite type belongs to $\mathsf{K}$. By Lemma 4.2 this reduction runs in polynomial time. Together with Theorem 5.1, this implies that the problem of determining whether the logic of a finite reduced matrix of finite type belongs to $\mathsf{K}$ is hard for EXPTIME. ∎

Corollary 5.6**.**

Let $\mathsf{K}$ be any level in the Leibniz hierarchy of Figure 1 different from the one of truth-equational logics. The problem of determining whether the logic of a finite reduced matrix of finite type belongs to $\mathsf{K}$ is complete for EXPTIME.

Proof.

This is a combination of Lemma 3.1 and Theorem 5.5. ∎

Remarkably, the methods developed in this work can be adapted to prove hardness results for other classes of logics studied in abstract algebraic logic. To exemplify this phenomenon, recall that a logic $\vdash$ is order algebraizable [32, 35] if there are a set $\varDelta(x,y)$ of formulas and a set $\bm{\tau}(x)$ of inequalities such that for every $\langle\bm{A},F\rangle\in\mathsf{Mod}^{\bm{\mathchoice{\textstyle*}{\textstyle*}{\textstyle*}{\scriptstyle*}}}(\vdash)$ the relation $\leqslant_{\bm{A}}^{F}$ defined for every $a,b\in A$ as

[TABLE]

is a partial order, and for every $a\in A$

[TABLE]

Corollary 5.7**.**

The problem of determining whether the logic of a finite reduced matrix of finite type is order algebraizable is complete for EXPTIME.

Sketch of the proof..

The class of order algebraizable logics has a syntactic characterization [35, Theorem 7.1]. Applying an argument similar to the one described in the proof of Lemma 3.1 to this characterization, it is possible to show that the problem of determining whether the logic of a finite reduced matrix of finite type is order algebraizable belongs to EXPTIME. To prove that this problem is hard for EXPTIME, we reason as follows. First observe that every order algebraizable logic is is equivalential, and that every algebraizable logic is order algebraizable. Then we can add the fact that $\vdash$ is order algebraizable to the list of equivalent conditions in the statement of Lemma 5.2. This yields the desired hardness result. ∎

We conclude with a list of open problems on the decidability and computational complexity of the hierarchies of abstract algebraic logic.

Problem 1*.*

Is the problem of determining whether the logic of a finite reduced matrix of finite type is truth-equational in EXPTIME? Observe Theorem 5.5 shows that this problem is hard for EXPTIME.

Problem 2*.*

Is the problem of determining whether the logic of a finite reduced matrix of finite type has an algebraic semantics decidable? And if so, then which is its computational complexity?

Problem 3*.*

The problem of determining whether the logic of a finite reduced matrix of finite type is assertional [1] is easily seen to be decidable. More interestingly, which is its computational complexity? Similar questions can be risen about other classes of logics in the Leibniz hierarchy.

Problem 4*.*

In this work we focussed on logics determined by arbitrary finite reduced matrices of finite type. Are the hardness results still true if we restrict our attention to finite reduced matrices $\langle\bm{A},F\rangle$ of finite type such that $F$ is a singleton?

Problem 5*.*

Are there reasonable assumptions (on matrices) under which the problem of classifying the logic of a finite reduced matrix of finite type in the Leibniz hierarchy becomes tractable?

Problem 6*.*

Investigate the decidability and complexity of determining whether the logic of a finite reduced matrix of finite type belongs to a given level of the Frege hierarchy of abstract algebraic logic.

Acknowledgements.

Thanks are due to Carles Noguera for rising the question about the computational complexity of the problem of classifying logics in the Leibniz hierarchy, and for providing very useful comments on early versions of the paper, which contributed to improve the presentation. We also also very grateful to the anonymous referee for a variety of helpful observations, including a correction to point 3 of Theorem 2.1. The author was supported by the grant GBP$202/12/$G$061$ of the Czech Science Foundation, and by project CZ.$02$.$2$.$69$/[math].[math]/[math].[math]/$17\_050$/$0008361$, OPVVV MŠMT, MSCA-IF Lidskeé zdroje v teoretickeé informatice.

6. Appendix

Through this section we assume that $\bm{A}$ is a fixed non-trivial algebra without constant symbols, and $\bm{A}^{\natural}$ is the algebra associated with it as in Section 4. The subformula tree of a formula $\varphi$ of $\bm{A}^{\natural}$ is defined by recursion on the construction of $\varphi$ as follows. The subformula tree of a variable $x$ is the one-element tree, whose unique node is labelled by $x$. Then the subformula tree of a complex formula $\varphi$ is obtained as follows. Suppose that $\varphi=g(\psi_{1},\dots,\psi_{n})$ for some basic $n$-ary symbol $g$ and formulas $\psi_{1},\dots,\psi_{n}$. First we pick the disjoint union of the subformula trees of $\psi_{1},\dots,\psi_{n}$, and we relabel the root of the subformula tree of $\psi_{i}$ by $\langle\psi_{i},i\rangle$. Second we add to these trees a common root labelled by $\varphi$.

Definition 6.1**.**

A formula $\varphi$ of $\bm{A}^{\natural}$ has the tree property when every node of the subformula tree of $\varphi$, which is labelled by a formula whose principal symbol belongs to $\mathcal{F}$ (plus possibly a natural number), is preceded or equal to a point which has a label of the form $\langle\beta,2\rangle$ whose immediate predecessor is labelled by $\heartsuit(\alpha,\beta,\gamma)$ or $\langle\heartsuit(\alpha,\beta,\gamma),n\rangle$ for some $n\in\omega$.

Example 6.2**.**

Since the definition of tree property is quite technical, we proceed to explain it through some basic examples. For the sake of simplicity, suppose that $\mathcal{F}$ contains only a unary symbol $f(x)$. The formulas

[TABLE]

have the tree property. On the other hand, the formula $\heartsuit(f(x),f(x),z)$ does not have the tree property. To explain why, observe that its subformula tree looks as follows:

[TABLE]

It is not hard to see that the occurrence of $\langle f(x),1\rangle$ in the lefter branch makes the tree property fail. ∎

Lemma 6.3**.**

If $\varphi(x_{1},\dots,x_{n})$ has the tree property, then for every $b^{n}\in A^{\natural}$ there is $m\leqslant 8$ such that

[TABLE]

Moreover, if $i\in\{1,3,4\}$, then $\varphi(b^{i},\dots,b^{i})\in\{b^{1},b^{3},b^{4}\}$.

Proof.

We reason by induction on the construction of $\varphi$. If $\varphi$ is a variable, then the result holds vacuously. Then consider the case where $\varphi$ is a complex formula. If $\varphi=f(\psi_{1},\dots,\psi_{n})$ for some $f\in\mathcal{F}$, then clearly $\varphi$ does not have the tree property. Then consider the case where $\varphi=\square\psi$. Then clearly also $\psi$ has the tree property. Consider $b^{n}\in A^{\natural}$. By inductive hypothesis there is $m\leqslant 8$ such that $\psi(b^{n},\dots,b^{n})=b^{m}$. Together with the definition of $\square$, this implies that

[TABLE]

Finally, consider the case where $\varphi=\heartsuit(\psi_{1},\psi_{2},\psi_{3})$. Clearly $\psi_{1}$ and $\psi_{3}$ must have the tree property. We focus only on $\psi_{1}$. Consider $b^{n}\in A^{\natural}$. By inductive hypothesis there is $m\leqslant 8$ such that $\psi_{1}(b^{n},\dots,b^{n})=b^{m}$. Together with the definition of $\heartsuit$, this implies that

[TABLE]

This concludes the inductive argument.

The last part of the statement (the one starting with Moreover…) is also proved by a simple induction. ∎

Lemma 6.4**.**

Let $\varphi(x,y)$ be a formula and $a\in A$. $\varphi(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$ if and only if $\varphi$ has the tree property.

Proof.

The direction from left to right is proved by induction on the construction of $\varphi$. The case where $\varphi$ is a variable is clear. Then suppose that $\varphi$ is a complex formula. If $\varphi=f(\psi_{1},\dots,\psi_{n})$ for some $f\in\mathcal{F}$, then $\varphi(a^{1},a^{3})$ belongs to $A_{5}$, which is disjoint from $A_{1}\cup A_{3}\cup A_{4}$. Then suppose that $\varphi=\square\psi$. From $\square\psi(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$ and the definition of $\square$, we can infer that $\psi(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$. By the inductive hypothesis we obtain that $\psi$ has the tree property. In particular, this is implies that $\varphi$ has the tree property too. Then consider the case where $\varphi=\heartsuit(\psi_{1},\psi_{2},\psi_{3})$. From the fact that $\varphi(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$, we can infer that $\psi_{1}(a^{1},a^{3}),\psi_{3}(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$. By the inductive hypothesis, this means that both $\psi_{1}$ and $\psi_{3}$ have the tree property. In particular, this implies that $\heartsuit(\psi_{1},\psi_{2},\psi_{3})$ has the tree property too.

The direction from right to left also follows from a simple induction. ∎

Lemma 6.5**.**

For every formula $\psi(x,\vec{y})$, $\vec{c}\in A^{\natural}$, and $a\in A$, there is $b\in A$ and $n,m\leqslant 8$ such that $\psi(a^{1},\vec{c})=b^{n}$ and $\psi(a^{3},\vec{c})=b^{m}$.

Proof.

This follows from a simple induction on the construction of $\psi$, using the definition of the basic operations of $\bm{A}^{\natural}$. ∎

As a consequence we obtain the following:

Corollary 6.6**.**

Let $f\in\mathcal{F}$ be $n$-ary and $\varphi_{1}(x,\vec{y}),\dots,\varphi_{n}(x,\vec{y})$ be terms of $\bm{A}^{\natural}$. For every $a\in A$ and $\vec{c}\in A^{\natural}$ we have

[TABLE]

Proof.

By Lemma 6.5 there are $b_{1},\dots,b_{n}\in A$ and $k_{1},\dots,k_{n},m_{1},\dots,m_{n}\leqslant 8$ such that

[TABLE]

This implies that

[TABLE]

concluding the proof. ∎

Lemma 6.7**.**

Let $\varphi(x,y)$ be a formula and $a\in A$. If $\varphi(a^{1},a^{3})\neq\varphi(a^{1},a^{1})$, then $\varphi(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$.

Proof.

We reason by induction on the construction of $\varphi$. The case where it is a variable is satisfied. Then suppose that $\varphi$ is a complex formula. If $\varphi=f(\psi_{1},\dots,\psi_{n})$ for some $f\in\mathcal{F}$, then by Corollary 6.6 we obtain that $\varphi(a^{1},a^{3})=\varphi(a^{1},a^{1})$, which is false. Then suppose that $\varphi=\square\psi$. From $\square\psi(a^{1},a^{3})\neq\psi(a^{1},a^{1})$ it follows that $\psi(a^{1},a^{3})\neq\psi(a^{1},a^{1})$. By inductive hypothesis we obtain that $\psi(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$. Together with the definition of $\square$, this implies that $\varphi(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$ as well. It only remains to consider the case where $\varphi=\heartsuit(\psi_{1},\psi_{2},\psi_{3})$. From the fact that $\varphi(a^{1},a^{3})\neq\varphi(a^{1},a^{1})$ it follows that one of the following conditions holds:

$\psi_{1}(a^{1},a^{3})\neq\psi_{1}(a^{1},a^{1})$. 2. 2.

$\psi_{2}(a^{1},a^{3})\neq\psi_{2}(a^{1},a^{1})$ and 1 does not hold. 3. 3.

$\psi_{3}(a^{1},a^{3})\neq\psi_{3}(a^{1},a^{1})$ and neither 1 not 2 hold.

We consider these cases separately:

1. By the inductive hypothesis we have that $\psi_{1}(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$. If $\psi_{3}(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$, then by definition of $\heartsuit$ we conclude that $\varphi(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$ and we are done. Then suppose towards a contradiction that $\psi_{3}(a^{1},a^{3})\notin A_{1}\cup A_{3}\cup A_{4}$. By Lemma 6.4 we know that $\psi_{3}$ does not have the tree property. Together with the definition o $\bm{A}^{\natural}$, this implies that $\psi_{3}(a^{1},a^{1})\notin A_{1}\cup A_{3}\cup A_{4}$ too. Moreover, by Lemma 6.4 we know that $\psi_{1}$ has the tree property. Together with Lemma 6.3 this implies that

[TABLE]

Thus we obtain that

[TABLE]

contradicting the fact that $\varphi(a^{1},a^{3})\neq\varphi(a^{1},a^{1})$.

2. We will show that this case leads to a contradiction, that is to say that it never happens. If $\psi_{2}(a^{1},a^{3})\neq\psi_{2}(a^{1},a^{1})$, then by inductive hypothesis this means that $\psi_{2}(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$. By Lemma 6.4 we know that $\psi_{2}$ has the tree property and by Lemma 6.3 that $\psi_{2}(a^{1},a^{1})\in A_{1}\cup A_{3}\cup A_{4}$ as well. Consider $b\in A$ and $n\leqslant 8$ such that $\psi_{1}(a^{1},a^{1})=\psi_{1}(a^{1},c^{3})=b^{n}$. By definition of $\heartsuit$ we have that

[TABLE]

[TABLE]

Since $\psi_{1}(a^{1},a^{1})=\psi_{1}(a^{1},a^{3})$ by assumption and $\varphi(a^{1},a^{1})\neq\varphi(a^{1},a^{3})$, we have that $\psi_{3}(a^{1},a^{1})\neq\psi_{3}(a^{1},a^{3})$. By inductive hypothesis this means that $\psi_{3}(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$. By Lemmas 6.4 and 6.4 we obtain that $\psi_{3}(a^{1},a^{1})\in A_{1}\cup A_{3}\cup A_{4}$ too. But this implies that

[TABLE]

contradicting the fact that $\varphi(a^{1},a^{1})\neq\varphi(a^{1},a^{3})$.

3. By inductive hypothesis we have that $\psi_{3}(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$. Suppose towards a contradiction that $\varphi(a^{1},a^{3})\notin A_{1}\cup A_{3}\cup A_{4}$. Then we have that $\psi_{1}(a^{1},a^{3})\notin A_{1}\cup A_{3}\cup A_{4}$. Consider $b\in A$ and $n\leqslant 8$ such that $b^{n}=\psi_{1}(a^{1},a^{3})$. By the definition of $\heartsuit$ we have that $\varphi(a^{1},a^{3})=b^{7}$. On the other hand, observe that applying Lemmas 6.4 and 6.3 to the fact that $\psi_{3}(a^{1},a^{3})\in A_{1}\cup A_{3}\cup A_{4}$, we obtain that $\psi_{3}(a^{1},a^{1})\in A_{1}\cup A_{3}\cup A_{4}$ as well. Together with the fact that $\psi_{1}(a^{1},a^{1})=\psi_{1}(a^{1},a^{3})\notin A_{1}\cup A_{3}\cup A_{4}$, this implies that $\varphi(a^{1},a^{1})=b^{7}$. But this contradicts the fact that $\varphi(a^{1},a^{1})\neq\varphi(a^{1},a^{3})$. ∎