## ON THE COMPLEXITY OF THE LEIBNIZ HIERARCHY

## TOMMASO MORASCHINI

A bstract . 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 .

## 1 . I ntroduction

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 K of the Leibniz hierarchy of Figure 1 we consider the following problems:

- 1 . Is the logic determined by a given finite Hilbert calculus in K ?

2 . Is the logic determined by a given finite matrix in 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 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 . T he L eibniz 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 〈 A , F 〉 , where A is an algebra and F ⊆ A . A congruence q of A is compatible with F ⊆ A , when F is a union of blocks of q . The largest congruence of A compatible with F (which always exists) is denoted by W A F and is called the Leibniz congruence of A w.r.t. F . A matrix 〈 A , F 〉 is reduced when W A F is the identity relation. The reduction of 〈 A , F 〉 is the matrix 〈 A / W A F F , / W A F 〉 . The last matrix is always reduced. Given a class of matrices K , we denote by K ∗ the class of isomorphic copies of the reductions of members of K , and by S ( K ) the class of substructures of members of K .

A logic glyph[turnstileleft] 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 glyph[turnstileleft] is finitary if for every set of formulas G ∪{ } j ,

$$\Gamma \vdash \varphi \Longleftrightarrow \Delta \vdash \varphi \text{ for some finite } \Delta \subseteq \Gamma.$$

Every class M of matrices determines a logic glyph[turnstileleft] M as follows:

$$\Gamma \vdash _ { M } \varphi \Longleftrightarrow \text{ for every evaluation $f$, if $f[\Gamma] \subseteq F$, then $f(\varphi) \in F$.}$$

Observe that a matrix and its reduction determine the same logic. A matrix 〈 A , F 〉 is a model of a logic glyph[turnstileleft] when glyph[turnstileleft] ⊆glyph[turnstileleft] 〈 A , F 〉 . We denote by Mod ∗ ( glyph[turnstileleft] ) the class of reduced models of glyph[turnstileleft] .

The main classes in the Leibniz hierarchy can de defined as follows. A logic glyph[turnstileleft] is protoalgebraic if there is a set of formulas D ( x y z , , glyph[vector] ) such that for every model 〈 A , F 〉 of glyph[turnstileleft] and every a b , ∈ A we have:

$$\langle a, b \rangle \in \Omega ^ { A } F \Longleftrightarrow \Delta ( a, b, \vec { c } ) \subseteq F \text{ for all } \vec { c } \in A.$$

A logic is equivalential if there exists a set of formulas D ( x y , ) without parameters glyph[vector] z , which satisfies condition ( 1 ).

A logic glyph[turnstileleft] is truth equational if there is a set of equations t ( x ) such that for every 〈 A , F 〉 ∈ Mod ∗ ( glyph[turnstileleft] ) we have

$$F = \{ a \in A \, \colon A \models \tau ( a ) \}.$$

|

|

"

"

"

![image](https://ac.marcodsn.me/arxiv-markdown-images/1908.00924v1-figure-a0cb8ff6-8119-42ca-bbeb-6d700fa5cc53.jpg)

"

|

|

"

"

F igure 1 . The main classes in the Leibniz hierarchy.

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 glyph[turnstileleft] be the logic determined by a finite set of finite matrices M .

- 1 . glyph[turnstileleft] is protoalgebraic if and only if there is a set of formulas D ( x y , ) (in variables x and y) such that ˘ glyph[turnstileleft] D ( x x , ) and x , D ( x y , ) glyph[turnstileleft] y.
- 2 . glyph[turnstileleft] is equivalential if and only if there is a set of formulas D ( x y , ) satisfying the conditions of point 1 and such for every basic n-ary operation f

$$\Delta ( x _ { 1 }, y _ { 1 } ) \cup \dots \cup \Delta ( x _ { n }, y _ { n } ) \vdash \Delta ( f ( x _ { 1 }, \dots, x _ { n } ), f ( y _ { 1 }, \dots, y _ { n } ) ).$$

Moreover, in this case D satisfies condition ( 1 ) for every model of glyph[turnstileleft] .

- 3 . glyph[turnstileleft] is weakly algebraizable (resp. algebraizable) iff it is protoalgebraic (resp. equivalential) and there is a set of equations t ( x ) such that for all 〈 B , F 〉 ∈ S ( M ) and b ∈ B:

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

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 glyph[turnstileleft] is protoalgebraic, then Mod ∗ ( glyph[turnstileleft] ) = P sd (( S ( M )) ∗ ) . To prove this, observe that glyph[turnstileleft] is finitary logic, since M is a finite set of finite matrices [ 14 , Theorem 4 4 . ]. In particular, this implies

$$\text{Mod} ^ { * } ( \vdash ) = ( \mathbb { S P } _ { R } ( M ) ) ^ { * } = ( \mathbb { P } _ { s D } \mathbb { S P } _ { U } ( M ) ) ^ { * } = ( \mathbb { P } _ { s D } \mathbb { S } ( M ) ) ^ { * }, \quad ( 3 )$$

where P r , P sd and P u are the class-operators of reduced, subdirect, and ultraproducts [ 14 , Theorem 4 7 . ]. Now, it is not hard to see that ( P sd S ( M )) ∗ ⊆ ( P sd (( S ( M )) ∗ )) ∗ ⊆ Mod ∗ ( glyph[turnstileleft] ) . Hence we obtain

$$\text{Mod} ^ { * } ( \vdash ) = ( \mathbb { P } _ { \text{sD} } ( ( \mathbb { S } ( M ) ) ^ { * } ) ) ^ { * }.$$

Recall that if glyph[turnstileleft] is protoalgebraic, then Mod ∗ ( glyph[turnstileleft] ) is closed under P sd [ 14 , Theorem 6 17 . ] (see also [ 9 , 11 , 13 ]). Together with the fact that ( S ( M )) ∗ ⊆

Mod ∗ ( glyph[turnstileleft] ) , this implies that if glyph[turnstileleft] is protoalgebraic, then

$$\text{Mod} ^ { * } ( \vdash ) = ( \mathbb { P } _ { s D } ( ( \mathbb { S } ( M ) ) ^ { * } ) ) ^ { * } = \mathbb { P } _ { s D } ( ( \mathbb { S } ( M ) ) ^ { * } ),$$

establishing the claim.

From the claim it follows that if glyph[turnstileleft] is protoalgebraic, then glyph[turnstileleft] is truthequational if and only if there is a set of equations t ( x ) such that for all 〈 B , F 〉 ∈ S ( M ) and b ∈ B :

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

This easily implies that condition 3 holds.

glyph[squaremultiply]

Lemma 2 2 . . Let glyph[turnstileleft] be the logic determined by a finite set of finite matrices M . Then glyph[turnstileleft] is truth-equational if and only if there is a set of equations t ( x ) such that for every 〈 B , G 〉 ∈ Mod ∗ ( glyph[turnstileleft] ) , where B is one-generated, and every 〈 A , F 〉 ∈ M we have

$$G = \{ b \in B \, \colon B \models \tau ( b ) \} \, a n d \, F \subseteq \{ a \in A \, \colon A / \Omega ^ { A } F \models \tau ( a / \Omega ^ { A } F ) \}.$$

In this case, we can take t ( x ) to be the set of equations # ≈ d such that

$$\varepsilon ^ { A / \Omega ^ { A } F } ( a / \Omega ^ { A } F ) = \delta ^ { A / \Omega ^ { A } F } ( a / \Omega ^ { A } F ), \, \text{for all } a \in F \, \text{and } \langle A, F \rangle \in \mathbf M.$$

Proof. Weclaim that if # ( x ) ≈ d ( x ) is an equation such that # A / W A F ( a / W A F ) = d A / W A F ( a / W A F ) for all a ∈ F and 〈 A , F 〉 ∈ M , then

$$\varepsilon ^ { B } ( b ) = \delta ^ { B } ( b ) \text{ for every } \langle B, G \rangle \in \text{Mod} ^ { * } ( \vdash ) \text{ and } b \in G.$$

To prove this, observe that Mod ∗ ( glyph[turnstileleft] ) can be seen as a class of firstorder structures in the algebraic language of glyph[turnstileleft] extended with a unary predicate symbol P x ( ) . More precisely, a matrix 〈 B , G 〉 ∈ Mod ∗ ( glyph[turnstileleft] ) can be regarded as a first-order structure given by the algebra B , equipped with the interpretation of P x ( ) given by the set G ⊆ B .

Now, consider a matrix 〈 B , G 〉 ∈ Mod ∗ ( glyph[turnstileleft] ) , and an equation # ≈ d such that # A / W A F ( a / W A F ) = d A / W A F ( a / W A F ) for all a ∈ F and 〈 A , F 〉 ∈ M . We have

$$\mathbf M \models \forall x ( P ( x ) \to \varepsilon ( x ) \approx \delta ( x ) ).$$

Moreover, as in ( 3 ), we have

$$\text{Mod} ^ { * } ( \vdash ) = ( \mathbb { P } _ { \text{SD} } \mathbb { S } ( M ) ) ^ { * }.$$

Hence 〈 B , G 〉 can be identified with a matrix of the form 〈 C / W C H H , / W C H 〉 for some 〈 C , H 〉 ∈ P sd S ( M ) .

Then consider an arbitrary element c ∈ C such that c / W C H ∈ H / W C H . Since the sentence in ( 4 ) is preserved by P sd and S , it holds in 〈 C , H 〉 as well. Together with the fact that c ∈ H , this implies that # C ( c ) = d C ( c ) . Hence we conclude that C / W C H glyph[satisfies] # ( c / W C H ) ≈ d ( c / W 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 t ( x )

satisfying the assumptions. Then consider an arbitrary matrix 〈 B , G 〉 ∈ Mod ∗ ( glyph[turnstileleft] ) . In order to prove that glyph[turnstileleft] is truth-equational, it will be enough to show that

$$G = \{ b \in B \, \colon B \models \tau ( b ) \}.$$

From the assumption we know that F ⊆ { a ∈ A : A / W A F glyph[satisfies] t ( a / W A F ) } for every 〈 A , F 〉 ∈ M . Together with the claim, this implies that G ⊆ { b ∈ B : B glyph[satisfies] t ( b ) } . Conversely, consider b ∈ B such that B glyph[satisfies] t ( b ) . Then consider the subalgebra C of B generated by b . As the congruence ( C × C ) ∩ W B G is compatible with G ∩ C , we obtain

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

Together with the fact that B glyph[satisfies] t ( b ) , this implies

$$C / \mathfrak { m } ^ { c } ( G \cap C ) \models \tau ( b / \mathfrak { m } ^ { c } ( G \cap C ) ).$$

Now, observe that 〈 C / W C ( G ∩ C ) , ( G ∩ C ) / W C ( G ∩ C ) 〉 is a reduced model of glyph[turnstileleft] , and that C / W C ( G ∩ C ) is one-generated. Hence we can apply the assumption to ( 5 ), obtaining

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

Since W C ( G ∩ C ) is compatible with G ∩ C , we get that b ∈ G ∩ C ⊆ G . Hence we conclude that

$$G \supseteq \{ b \in B \, \colon B \models \tau ( b ) \}$$

and, therefore, that glyph[turnstileleft] is truth equational.

To conclude the proof, suppose that there is a set of equations t ( x ) satisfying the condition in the statement. Moreover, let t ′ ( x ) be the set of equations # ≈ d such that # A / W A F ( a / W A F ) = d A / W A F ( a / W A F ) , for all a ∈ F and 〈 A , F 〉 ∈ M . Since F ⊆ { a ∈ A : A / W A F glyph[satisfies] t ( a W A F ) } for all 〈 A , F 〉 ∈ M , we obtain that t ( x ) ⊆ t ′ ( x ) . In particular, this implies that for every 〈 B , G 〉 ∈ Mod ∗ ( glyph[turnstileleft] ) such that B is one-generated,

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

The reverse inclusion follows from the claim at the beginning of the proof. glyph[squaremultiply]

We will also make use of the following technical lemma: 1

Lemma 2 3 . . Let glyph[turnstileleft] be the logic determined by a reduced matrix 〈 A , F . 〉

- 1 . If A is trivial, then glyph[turnstileleft] is weakly algebraizable if and only if F = A.
- 2 . If A is non-trivial and all its basic operations are constants, then glyph[turnstileleft] is not weakly algebraizable.
- 3 . If A is trivial, then glyph[turnstileleft] is truth-equational if and only if F = A.
- 4 . If A is non-trivial and all its basic operations are constants, then glyph[turnstileleft] is truthequational if and only if there is a constant a which is interpreted inside F.

1 I am indebted to the referee of my [ 29 ] for suggesting a simplification in the proof of Lemma 2 2 . .

- Proof. 1 . Observe that if A is trivial, then glyph[turnstileleft] 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 j glyph[turnstileleft] y for all formulas j and y . More in detail, glyph[turnstileleft] is inconsistent when F = A , and it is almost inconsistent when F = ˘ . 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 A is non-trivial and that all its basic operations are constants. Since all operations of A are constants, the Leibniz congruence of 〈 A , F 〉 has only two blocks, i.e. F and A glyph[integerdivide] F . Together with the fact that 〈 A , F 〉 is reduced and that A non-trivial, this implies that A is a two element algebra, say with universe { 0, 1 } , and F = { 1 } . Hence glyph[turnstileleft] is determined by 〈 A , { 1 }〉 .

Suppose towards a contradiction that glyph[turnstileleft] is weakly algebraizable. Then there is a set of formulas D ( x y , ) as in condition 1 of Theorem 2 1 . . In particular, this means that

$$\emptyset \vdash \Delta ( x, x ) \text{ and } x, \Delta ( x, y ) \vdash y.$$

Due to the poorness of the language of A , we have that D ( x y , ) can contain only constants a b c , , . . . and the variables x y , . Now, since D ( x x , ) is a set of tautologies of glyph[turnstileleft] and glyph[turnstileleft] is determined by 〈 A , { 1 }〉 , we have that a / ∈ D ( x y , ) for each constant a which is interpreted to 0. Similarly, as x and y can be interpreted as 0 and D ( x x , ) is a set of tautologies, we obtain x y , / ∈ D ( x y , ) . Then D ( x y , ) is a set of constants that are interpreted to 1. Hence D ( x y , ) is a set of tautologies of glyph[turnstileleft] , since glyph[turnstileleft] is determined by 〈 A , { 1 }〉 . This means that the rule x , D ( x y , ) glyph[turnstileleft] y specializes to x glyph[turnstileleft] y , which is easily seen to fail in 〈 A , { 1 }〉 .

- 3 . Suppose that A is trivial. If F = A , then all reduced models of glyph[turnstileleft] are isomorphic to 〈 A , F 〉 . Hence glyph[turnstileleft] is truth-equational with t = ˘ . Then suppose that F = ˘ . Observe that there cannot be a set of equations t whose set of solutions in A is empty. Hence glyph[turnstileleft] is not truth-equational.
- 4 . Suppose that A is non-trivial. As motivated in the proof of condition 2 , A is a two element algebra, say with universe { 0, 1 } , and F = { 1 } . If no constant symbol of A is interpreted to 1, then F cannot be defined as in ( 2 ). Hence glyph[turnstileleft] is not truth-equational. On the other hand, if there is a constant a which is interpreted to 1, then Mod ∗ ( glyph[turnstileleft] ) is the class of isomorphic copies of 〈 A , F 〉 and of the matrix 〈 B , B 〉 , where B is the trivial algebra. This means that glyph[turnstileleft] is truth-equational with t ( x ) : = { x ≈ a } . glyph[squaremultiply]

Recall that if A is an algebra, the free n -generated algebra Tm ( x 1, . . . , xn ) in the variety generated by A is isomorphic to the subalgebra of A ( A n ) generated by the projections (see [ 5 ] if necessary). Sometimes we tacitly identify the elements of the free algebra Tm ( x 1, . . . , xn ) (i.e. the equivalence classes of formulas with variables among x 1, . . . , xn that have the same

interpretation in A ) with particular formulas j ( x 1, . . . , xn ) that represent them.

Lemma 2 4 . . Let 〈 A , F 〉 be a finite reduced matrix, and Tm ( x , ) Tm ( x y , ) respectively the free one-generated and the free two-generated algebras over the variety generated by A . Consider also the following sets of formulas and equations

$$\Delta ( x, y ) \coloneqq & \{ \varphi \in T m ( x, y ) \colon \varphi ^ { A } ( a, a ) \in F, \, \text{for all} \, a \in A \}$$

$$\tau ( x ) \coloneqq & \{ \varepsilon \approx \delta \colon \varepsilon, \delta \in T m ( x ) \, a n d \, \varepsilon ^ { A } ( a ) = \delta ^ { A } ( a ), \, \text{for all } a \in F \}.$$

$$A \} \\ \cdot f o r \, a l l \, a \in F \}.$$

The following conditions hold for the logic glyph[turnstileleft] determined by 〈 A , F . 〉

- 1 . glyph[turnstileleft] is protoalgebraic iff D satisfies the requirement in condition 1 of Theorem 2 1 . .
- 2 . glyph[turnstileleft] is equivalential iff D satisfies the requirement in condition 2 of Theorem 2 1 . .
- 3 . glyph[turnstileleft] is weakly algebraizable (resp. algebraizable) iff glyph[turnstileleft] is protoalgebraic (resp. equivalential) and t satisfies the requirement in condition 3 of Theorem 2 1 . .
- 4 . glyph[turnstileleft] is truth-equational iff t satisfies the requirement in Lemma 2 2 . .

Proof. 1 . We have to prove that glyph[turnstileleft] is protoalgebraic if and only if ˘ glyph[turnstileleft] D ( x x , ) and x , D ( x y , ) glyph[turnstileleft] y . The 'if' part is a consequence of Theorem 2 1 1 . ( ). To prove the 'only if' part, suppose that glyph[turnstileleft] is protoalgebraic. By condition 1 of Theorem 2 1 . there is a set of formulas D ′ ( x y , ) such that ˘ glyph[turnstileleft] D ′ ( x x , ) and x , D ′ ( x y , ) glyph[turnstileleft] y . Since the logic glyph[turnstileleft] is determined by 〈 A , F 〉 , we can assume w.l.o.g. that D ′ ⊆ Tm x y ( , ) . Together with ˘ glyph[turnstileleft] D ′ ( x x , ) and the definition of D , this implies D ′ ⊆ D . Bearing in mind that x , D ′ ( x y , ) glyph[turnstileleft] y , we conclude that x , D ( x y , ) glyph[turnstileleft] y . Finally, the fact that ˘ glyph[turnstileleft] D ( x x , ) is an immediate consequence of the definition of D .

2 . The 'if' part of the statement is a consequence of Theorem 2 1 2 . ( ). To prove the 'only if' part, suppose that glyph[turnstileleft] is equivalential. By condition 2 of Theorem 2 1 . there is a set D ′ ( x y , ) such that

$$\emptyset & \vdash \Delta ^ { \prime } ( x, x ) \quad \ x, \Delta ^ { \prime } ( x, y ) \vdash y \\ \Delta ^ { \prime } ( x _ { 1 }, y _ { 1 } ) \cup \cdots \cup \Delta ( x _ { n }, y _ { n } ) \vdash \Delta ^ { \prime } ( f ( x _ { 1 }, \dots, x _ { n } ), f ( y _ { 1 }, \dots, y _ { n } ) )$$

for every basic n -ary operation f . To conclude the proof, it will be enough to show that the sets D ( x y , ) and D ′ ( x y , ) are interderivable in glyph[turnstileleft] .

As in the proof of 1 , we can assume w.l.o.g. that D ′ ⊆ D . Therefore it only remains to show that D ′ ( x y , ) glyph[turnstileleft] j for every j ∈ D . To this end, consider a b , ∈ A such that D ′ A ( a b , ) ⊆ F . By the last part of condition 2 of Theorem 2 1 . , this implies 〈 a b , 〉 ∈ W A F . Since 〈 A , F 〉 is reduced, we conclude that a = b . Together with the definition of D , this implies D A ( a b , ) = D A ( a , a ) ⊆ F . Since glyph[turnstileleft] is the logic determined by 〈 A , F 〉 , we conclude that D ′ ( x y , ) glyph[turnstileleft] j for all j ∈ D ( x y , ) .

- 4 . The 'if' part of the statement is a consequence of Lemma 2 2 . . To prove the 'only if' part, suppose that glyph[turnstileleft] is truth-equational. From the definition of t and the fact that 〈 A , F 〉 is reduced it follows that

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

Then consider 〈 B , G 〉 ∈ Mod ∗ ( glyph[turnstileleft] ) such that B is one-generated. It only remains to prove that for every b ∈ B ,

$$b \in G \Longleftrightarrow B \models \tau ( b ).$$

To this end, consider a matrix 〈 B , G 〉 ∈ Mod ∗ ( glyph[turnstileleft] ) such that B is onegenerated. Moreover, let t ′ be the set of equations # ( x ) ≈ d ( x ) such that # A ( a ) = d A ( a ) for every a ∈ F . Since glyph[turnstileleft] is truth-equational, we can apply the last part of the statement of Lemma 2 2 . and the fact that 〈 A , F 〉 is reduced obtaining that for every b ∈ B ,

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

Now, as in ( 3 ), B belongs to the variety generated by A . As a consequence,

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

for every b ∈ 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 glyph[turnstileleft] is weakly algebraizable. Clearly, glyph[turnstileleft] is protoalgebraic. Moreover, since glyph[turnstileleft] is truth-equational, we can apply point 4 yielding that t satisfies the conditions in Lemma 2 2 . . This clearly implies that t satisfies the (weaker) requirement in Theorem 2 1 3 . ( ). glyph[squaremultiply]

## 3 . U pper 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 〈 A , F 〉 . The finite set A could be represented by its cardinality, say n (and A can be taken to be { 1, . . . , 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 glyph[lessorequalslant] n , indicating that F = { k ∈ w : 1 glyph[lessorequalslant] k glyph[lessorequalslant] m } (observe that F = ˘ , 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 〈 A , F 〉 of finite type, and let glyph[turnstileleft] be the logic it defines. Moreover, let D and t be the sets defined in Lemma 2 4 . . In order to determine whether glyph[turnstileleft] is weakly algebraizable or not, it is enough to check whether D and t 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 Tm ( x ) and Tm ( x y , ) in the variety generated by 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 〈 A , F 〉 . If it reads that 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 A is non-trivial, then the algorithm starts checking whether A has a basic operation, which is not a constant. If this is not the case, then the algorithm establishes that glyph[turnstileleft] 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 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 A . First we need to construct the sets Tm x ( ) and Tm x y ( , ) respectively of all unary and binary term-functions of A . This task amounts to that of constructing the one-generated and the two-generated free algebras of the variety generated by A (which are isomorphic to subalgebras of A A and A ( A 2 ) , respectively). Since n dominates the cardinality of A , the time needed in the construction of Tm x ( ) and Tm x y ( , ) can be bounded exponentially in n . Thus the sets D and t can be constructed in exponential time in n .

By Lemma 2 4 1 . ( ), glyph[turnstileleft] is protoalgebraic if and only if D satisfies the righthand 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 glyph[turnstileleft] is not protoalgebraic, the algorithm stops and provides a negative answer.

If glyph[turnstileleft] is protoalgebraic, then by Lemma 2 4 3 . ( ) the logic glyph[turnstileleft] is weakly algebraizable if and only if t satisfies the requirement in the display of condition 3 of Theorem 2 1 . . To this end, we construct all substructures 〈 B , G 〉 of 〈 A , F 〉 (which can be done in exponential time). For each such submatrix 〈 B , G 〉 , the Leibniz congruence W B G can be computed in n log n time. 2 Finally, for every 〈 B , G 〉 , 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 . glyph[squaremultiply]

2 This is justified as follows. First observe that the matrix 〈 B , G 〉 can be transformed into an automaton 〈 B + , G 〉 , where B + is the algebra with universe B and whose basic operations are the unary functions of the form f B ( b 1 , . . . , bn , x bn , + 1 , . . . , bm ) for some glyph[vector] b ∈ B and some basic operation f of B . Observe that the length of 〈 B + , G 〉 is essentially the same of 〈 B , G 〉 , i.e. n . Now, it is known that the task of computing the Leibniz congruence W B G amounts to that of minimizing the number of states of the automaton 〈 B + , G 〉 . Since the time needed to solve the latter task is bounded above by n log n [ 23 ], we are done.

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 2 -EXPTIME .

Proof. Let 〈 A , F 〉 be a finite reduced matrix of finite type, and let glyph[turnstileleft] be the logic it determines. Let also t be the set of equations in the statement of Lemma 2 4 . . In order to determine whether glyph[turnstileleft] is truth-equational or not, it is enough to check whether t 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 Tm ( x ) in the variety generated by A , and the set t can be constructed mechanically as in the proof of Lemma 3 1 . . Then we construct all sets G ⊆ Tm x ( ) such that 〈 Tm ( x ) , G 〉 is a model of glyph[turnstileleft] . Then, we check whether for every such G we have that

$$\Gamma / \Omega ^ { T m ( x ) } \Gamma = \{ \varphi / \Omega ^ { T m ( x ) } \Gamma \in T m ( x ) / \Omega ^ { T m ( x ) } \Gamma \colon \tau ( \varphi ) \subseteq \Omega ^ { T m ( x ) } \Gamma \}. \ \ ( 8 )$$

Observe that the above equality can be checked mechanically, since Tm ( x ) is a finite algebra. The test says that glyph[turnstileleft] is truth-equational, if the above condition holds, and it says that glyph[turnstileleft] 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

$$\text{Mod} ^ { * } ( \vdash ) = ( \mathbb { P } _ { \text{sD} } \mathbb { S } ( \langle A, F \rangle ) ) ^ { * }.$$

In particular, this means that the algebraic reducts of Mod ∗ ( glyph[turnstileleft] ) belong to the variety generated by 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 Mod ∗ ( glyph[turnstileleft] ) is indeed Tm ( x ) . On the other hand, it implies that the reduced models 〈 B , G 〉 of glyph[turnstileleft] such that B is one-generated are (up to isomorphism) the ones of the form 〈 Tm ( x ) / W Tm ( x ) G G , / W Tm ( x ) G 〉 where G ⊆ Tm x ( ) is such that 〈 Tm ( x ) , G 〉 is a model of glyph[turnstileleft] . Hence our test amounts to checking whether t 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 〈 A , F 〉 . If it reads that 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 A is non-trivial, then the algorithm starts checking whether all a basic operations of 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 〈 A , F 〉 .

If the algorithm does not have halted yet, then 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 A . From now on we just

apply the algorithm described at the beginning of the proof. First observe that t and 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 G ⊆ Tm x ( ) such that 〈 Tm ( x ) , G 〉 is a model of glyph[turnstileleft] . This computation requires a number of constructions of order

$$2 ^ { n ^ { n } } \cdot n ^ { n } \cdot n \leqslant 2 ^ { 2 ^ { n ^ { 2 } + 2 n + n } }$$

since the number of subsets G ⊆ Tm x ( ) is bounded above by 2 n n , and for each of G ⊆ Tm x ( ) we have to check that every formula j ∈ Tm x ( ) (there are at most n n of them) such that G glyph[turnstileleft] j belongs to G (checking whether G glyph[turnstileleft] j involves at most n assignments of the variable x in 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 G ⊆ Tm x ( ) such that 〈 Tm ( x ) , G 〉 is a model of glyph[turnstileleft] takes at most double exponential time in n .

Let 〈 Tm ( x ) , G 〉 be a model of glyph[turnstileleft] . As shown in the proof of Lemma 3 1 . , the Leibniz congruence W Tm ( x ) G can be computed in m log m time in the length of W Tm ( x ) G , which is bounded by 2 p n ( ) for some polynomial p n ( ) . Bearing this in mind, the time needed in the construction of W Tm ( x ) G is bounded above by 2 q n ( ) for some polynomial q n ( ) . Finally, for every G and j , 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 ) . glyph[squaremultiply]

A logic is said to be strongly finite when it is determined by a finite set of finite matrices of finite type. 3 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 M which are not necessarily reduced. For this reason, we need to replace the set 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 . ). glyph[squaremultiply]

## 4 . T wo fundamental constructions

In this section A is a fixed non-trivial algebra with basic operations F , and h is a unary function on A . For sake of simplicity, we assume that F

3 In some works the assumption of the finiteness of the type is dropped.

contains no constant symbols. Our goal is to define two algebras A glyph[natural] and A glyph[flat] related to 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 A glyph[natural] . The universe of A glyph[natural] is given by eight disjoint copies A 1, . . . , A 8 of A . Given an element a ∈ A , we will denote by a i its copy in Ai . In this sense an arbitrary finite set of elements in A glyph[natural] can be denoted as { a m 1 1 , . . . , an mn } for some a 1, . . . , an ∈ A and m 1, . . . , mn glyph[lessorequalslant] 8. The basic operations of A glyph[natural] are the ones in F plus a new ternary operation ♥ and a new unary operation glyph[square] . Their interpretation is defined as follows. Given an n -ary operation f ∈ F and a m 1 1 . . . , an mn ∈ A glyph[natural] , we set

$$f ( a _ { 1 } ^ { m _ { 1 } } \dots, a _ { n } ^ { m _ { n } } ) \coloneqq f ^ { A } ( a _ { 1 }, \dots, a _ { n } ) ^ { 5 }.$$

Observe that all the operations f A glyph[natural] with f ∈ F give values in A 5. Given a m , b n , c k ∈ A glyph[natural] , we set glyph[negationslash]

glyph[negationslash]

glyph[negationslash]

$$\bigvee ( a ^ { m }, b ^ { n }, c ^ { k } ) \coloneqq \begin{cases} \begin{array} { c c } a ^ { 1 } & \text{if $a^{m}=c^{k}$ and $h(a)^{5}=b^{n}$ and $m\in\{1,3,4\}$} \\ a ^ { 2 } & \text{if $a^{m}=c^{k}$ and $h(a)^{5}=b^{n}$ and $m\in\{2,5,6,7,8\}$} \\ a ^ { 4 } & \text{if $m,k\in\{1,3,4\}$ and (either $a^{m}\neq c^{k}$ or $h(a)^{5}\neq b^{n})$} \\ a ^ { 7 } & \text{if $\{m,k\}\cap\{2,5,6,7,8\} \neq \emptyset$ and} \\ & (either $a^{m}\neq c^{k}$ or $h(a)^{5}\neq b^{n})$.} \end{cases}$$

glyph[negationslash]

Given a m ∈ A glyph[natural] , we set

$$\Box ( a ^ { m } ) \coloneqq \begin{cases} \ a ^ { m } & \text{if $m=1$ or $m=2$} \\ \ a ^ { m - 1 } & \text{if $m$ is even and $m\geqslant3$} \\ \ a ^ { m + 1 } & \text{if $m$ is odd and $m\geqslant3$.} \end{cases}$$

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

$$f ( b _ { 1 }, \dots, b _ { n } ) \coloneqq \begin{cases} \begin{array} { c } f ^ { A } ( a _ { 1 }, \dots, a _ { n } ) ^ { 2 } & \text{if $b_{i} \in \{a_{i}^{1}, a_{i}^{2}} \}$ for all $i \leqslant n$} \\ 1 & \text{if $b_{1} = \dots = b_{n} = 1$} \\ 0 & \text{otherwise.} \end{array} \end{cases}$$

Moreover, for every a b , ∈ A glyph[flat] we set

$$a + b \coloneqq \begin{cases} \ 1 & \text{either $a=b=1$ or} \\ & ( a = c ^ { 1 } \text{ for some $c\in A$ and $b=h(c)^{2})$} \\ 0 & \text{otherwise.} \end{cases}$$

Finally, for every a ∈ A and b ∈ A glyph[flat] we set

$$\Box ^ { a } ( b ) \coloneqq \begin{cases} \begin{array} { c c c c } b & \text{if $b\in (A_{1}\cup A_{2})\smallsetminus \{a^{1},a^{2}\}$} \\ a^{2} & \text{if $b=a^{1}$} \\ a^{1} & \text{if $b=a^{2}$} \\ 0 & \text{if $b\in \{0,1\}$}. \end{array} \end{cases}$$

Now, consider the matrices 〈 A glyph[natural] , F glyph[natural] 〉 and 〈 A glyph[flat] , G glyph[flat] 〉 where

$$F ^ { \natural } \coloneqq A _ { 1 } \cup A _ { 2 } \text{ and } G ^ { \natural } \coloneqq A _ { 1 } \cup \{ 1 \}.$$

Lemma 4 1 . . The matrices 〈 A glyph[natural] , F glyph[natural] 〉 and 〈 A glyph[flat] , G glyph[flat] 〉 are reduced.

Proof. Observe that, to prove that an arbitrary matrix 〈 B , H 〉 is reduced, it is enough to show that for every pair of different elements a b , ∈ B there is a unary polynomial function p x ( ) such that

$$\text{either} \left ( p ( a ) \in H \text{ and } p ( b ) \notin H \right ) \text{or} \left ( p ( a ) \notin H \text{ and } p ( b ) \in H \right ).$$

To prove that ( 9 ) holds for 〈 A glyph[natural] , F glyph[natural] 〉 we reason as follows. Consider two distinct elements a n , b m ∈ A glyph[natural] . Then consider the unary polynomial function

$$p ( x ) \coloneqq \bigotimes ( x, h ( a ) ^ { 5 }, a ^ { n } ).$$

It is clear that p a n ( ) ∈ F glyph[natural] , while p b m ( ) / ∈ F glyph[natural] . Hence 〈 A glyph[natural] , F glyph[natural] 〉 is reduced.

Then we turn to prove that ( 9 ) holds for 〈 A glyph[flat] , G glyph[flat] 〉 too. To this end, consider two different a b , ∈ A glyph[flat] . If a ∈ G glyph[flat] and b / ∈ G glyph[flat] , then we are done. Then suppose that either a b , ∈ G glyph[flat] or a b , / ∈ G glyph[flat] . First consider the case where a b , / ∈ G glyph[flat] . We can assume w.l.o.g. that a = c 2 for some c ∈ A . Then we have that glyph[square] c ( a ) = c 1 ∈ G glyph[flat] , while glyph[square] c ( b ) = b / ∈ G glyph[flat] . Then suppose that a b , ∈ G glyph[flat] . W.l.o.g. we have the following cases:

1

.

a

=

1 and

b

glyph[negationslash]

=

1.

## 2 . 1 / ∈ { a b , } .

glyph[negationslash]

- 1 . Since A is non-trivial, there is c ∈ A such that b = c 1 . Then observe that glyph[square] c ( a ) = 0 / ∈ G glyph[flat] , while glyph[square] c ( b ) = b ∈ G glyph[flat] .
- 2 . Then observe that a = c 1 and b = d 1 for some different c , d ∈ A . We have that glyph[square] c ( a ) = c 2 / ∈ G glyph[flat] , while glyph[square] c ( b ) = b ∈ G glyph[flat] . glyph[squaremultiply]

Lemma 4 2 . . There is an algorithm that transform inputs 〈 A , h 〉 of Gen-Clo 1 3 into matrices 〈 A glyph[natural] , F glyph[natural] 〉 (resp. 〈 A glyph[flat] , G glyph[flat] 〉 ) and runs in polynomial time in the length of the input.

Proof. We detail the case of 〈 A glyph[natural] , F glyph[natural] 〉 only. Observe that a typical input of Gen-Clo 1 3 is a pair 〈 A , h 〉 , where A is an algebra without constant symbols. Therefore it makes sense to transform it into a matrix of the form 〈 A glyph[natural] , F glyph[natural] 〉 . 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 〈 A glyph[natural] , F glyph[natural] 〉 should be bounded by a polynomial in the length n of the input 〈 A , h 〉 . Since h is

unary, we know that n dominates the cardinality of A . Moreover, A has at most n basic operations, all of arity at most 3. Thus A glyph[natural] is an algebra of cardinality at most 8 n , with at most n + 2 basic operations, all of arity at most 3. Hence the length of A glyph[natural] is bounded above by 8 n +( n + ) 2 · ( 8 n ) 3 . Thus the length of 〈 A glyph[natural] , F glyph[natural] 〉 is bounded by 8 n +( n + ) 2 · ( 8 n ) 3 + 8 n . glyph[squaremultiply]

## 5 . H ardness 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 ]:

- · Gen-clo 1 3 : Given a finite non-trivial algebra A with finitely many basic operations 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 A ?

It is clear that 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 . ]: 4

## Theorem 5 1 . . The problem 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 A be a non-trivial algebra without constant symbols, h be a unary operation on A other than the identity, and glyph[turnstileleft] be the logic determined by the matrix 〈 A glyph[natural] , F glyph[natural] 〉 . The following conditions are equivalent:

- (i) glyph[turnstileleft] is algebraizable.
- (ii) glyph[turnstileleft] is weakly algebraizable.
- (iii) glyph[turnstileleft] is equivalential.
- (iv) glyph[turnstileleft] is protoalgebraic.
- (v) h is in the clone of A .

glyph[negationslash]

Proof. The implications (i) ⇒ (ii), (i) ⇒ (iii), (ii) ⇒ (iv) and (iii) ⇒ (iv) are straightforward. (v) ⇒ (i): Let j ( x ) be a term of A representing h on A . Since h is not the identity, we have that j ( x ) = x . We consider the same term in the algebra A glyph[natural] . Then consider the following sets:

$$\tau ( x ) \coloneqq \{ x \approx \Box x \} \text{ and } \Delta ( x, y ) \coloneqq \{ \mathcal { N } ( x, \varphi ( x ), y ) \}.$$

glyph[negationslash]

Bearing in mind that j ( x ) = x , it is an easy exercise to check that for every a b , ∈ A glyph[natural] we have that

$$a \in F ^ { \natural } & \Longleftrightarrow A ^ { \natural } \models \tau ( a ) \\ a = b & \Longleftrightarrow \Delta ( a, b ) \subseteq F ^ { \natural }.$$

$$\cdot$$

4 Observe 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 Gen-clo 1 3 .

By condition 3 of Theorem 2 1 . we conclude that glyph[turnstileleft] is algebraizable.

glyph[negationslash]

(iv) ⇒ (v): Suppose that glyph[turnstileleft] is protoalgebraic. This means that there is a set D ( x y , ) satisfying the conditions in point 1 of Theorem 2 1 . . Since glyph[turnstileleft] is neither inconsistent nor almost-inconsistent, we know that D = ˘ and that no variable belongs to D . Pick any element a ∈ A . We know that { a 1 } ∪ D ( a 1 , a 1 ) ⊆ F , since ˘ glyph[turnstileleft] D ( x x , ) . Together with the fact that x , D ( x y , ) glyph[turnstileleft] y and that a 3 / ∈ F glyph[natural] , this implies that there is j ( x y , ) ∈ D such that j ( a 1 , a 1 ) ∈ F glyph[natural] and j ( a 1 , a 3 ) / ∈ F .

Observe that ˘ glyph[turnstileleft] j ( x x , ) . In particular, we have that j ( a 3 , a 3 ) ∈ F glyph[natural] . Together with the definition of A glyph[natural] , this implies that j ( x y , ) = glyph[square] m ♥ ( y 1, y 2, y 3 ) for some m ∈ w and formulas y 1, y 2 and y 3. We can assume w.l.o.g. that m = 0, since glyph[square] x glyph[turnstileleft] x and x glyph[turnstileleft] glyph[square] x . The fact that j ( x x , ) is a tautology of glyph[turnstileleft] implies that

$$\text{For every } b \in A ^ { \natural }, \text{if } c ^ { n } = \psi _ { 1 } ( b, b ), \text{then } \psi _ { 2 } ( b, b ) = h ( c ) ^ { 5 }. \quad ( 1 0 )$$

Again looking at the definition of A glyph[natural] , this implies that y 2 = glyph[square] 2 k f ( # 1, . . . , # n ) for some f ∈ F , formulas # i and k ∈ w . In particular, we can assume w.l.o.g. that k = 0, since A glyph[natural] glyph[satisfies] glyph[square] 2 k f ( # 1, . . . , # n ) ≈ f ( # 1, . . . , # n ) . To every formulas # i we associate a new formula d i written only with the symbols of F . This is done as follows: first we delete from # i all occurrences of glyph[square] , and then we replace every occurrence of ♥ ( c 1, c 2, c 3 ) by c 1. This concludes the definition of d i . Observe that for every b c , ∈ A glyph[natural] there is a ∈ A such that

$$\varepsilon _ { i } ( b, c ), \delta _ { i } ( b, c ) \in \{ a ^ { 1 }, \dots, a ^ { 8 } \}.$$

In particular, this implies that for every b c , ∈ A glyph[natural] we have

$$f ( \varepsilon _ { 1 }, \dots, \varepsilon _ { n } ) ( b, c ) = f ( \delta _ { 1 }, \dots, \delta _ { n } ) ( b, c ).$$

Thus we can assume w.l.o.g. that y 2 = f ( d 1, . . . , d n ) .

glyph[negationslash]

Now, recall that j ( a 1 , a 1 ) ∈ F , while j ( a 1 , a 3 ) / ∈ F . In particular, we have that j ( a 1 , a 1 ) = j ( a 1 , a 3 ) . Then we can apply Lemma 6 7 . , obtaining that j ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4. Together with Lemmas 6 4 . and 6 3 . this implies that

$$\varphi ( b ^ { n }, b ^ { n } ) \in \{ b ^ { 1 }, \dots, b ^ { 8 } \} \text{ for every } b ^ { n } \in A ^ { \natural }.$$

Pick b n ∈ A glyph[natural] . In particular, we have that y 1 ( b n ) = b m for some m glyph[lessorequalslant] 8. Together with condition ( 10 ) this implies that

$$\psi _ { 2 } ( b ^ { n }, b ^ { n } ) = f ( \delta _ { 1 }, \dots, \delta _ { n } ) ( b ^ { n }, b ^ { n } ) = h ( b ) ^ { 5 }.$$

Recall that f ( d 1, . . . , d n ) is a formula written only with symbols in F . Hence we obtain that

$$f ( \delta _ { 1 }, \dots, \delta _ { n } ) ^ { A } ( b, b ) = h ( b )$$

for every b ∈ A . This means that the term f ( d 1, . . . , d n )( x x , ) represents h in A , i.e. h belongs to the clone of A . glyph[squaremultiply]

Let t be a set of equations in variable x . A class of algebras K is a t -algebraic semantics for a logic glyph[turnstileleft] [ 8 , 10 , 33 ] if for every set of formulas G ∪{ } j , we have:

$$\Gamma \vdash \varphi \Longleftrightarrow \tau ( \Gamma ) \, \mathbb { \vdash } _ { K } \, \tau ( \varphi )$$

where glyph[satisfies] K is the equational consequence relative to K . In what follows we will make use of the following result [ 33 , Proposition 39 ]:

Theorem 5 3 . . Let glyph[turnstileleft] be a logic with a t -algebraic semantics. Suppose that t contains an equation # ≈ d such that d ( x ) glyph[turnstileleft] x and ˘ glyph[turnstileleft] # ( x . ) Then glyph[turnstileleft] is truth-equational by means of d ( x ) ≈ # ( x . )

Lemma 5 4 . . Let A be a non-trivial algebra without constant symbols, h be a unary operation of A, and glyph[turnstileleft] be the logic determined by the matrix 〈 A glyph[flat] , G glyph[flat] 〉 . glyph[turnstileleft] is truth-equational if and only if h is in the clone of A .

Proof. We begin by the 'if' part. Let t ( x ) be the term that represents h in A . Then define d : = x + ( ) t x and # : = 1 . Moreover, set t : = { d ( x ) ≈ # ( x ) } . Observe that the set of equations t defines G glyph[flat] in A glyph[flat] . Thus the class K = { A glyph[flat] } is a t -algebraic semantics for glyph[turnstileleft] . Moreover, observe that d ( x ) glyph[turnstileleft] x and ˘ glyph[turnstileleft] # ( x ) . Therefore we can apply 5 3 . yielding that glyph[turnstileleft] is truth-equational.

Then we turn our attention to the 'only if' part. Suppose that glyph[turnstileleft] is truth-equational. Observe that the matrix 〈 A glyph[flat] , G glyph[flat] 〉 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 t that satisfies condition ( 2 ), namely

$$\tau \coloneqq \{ \varepsilon ( x ) \approx \delta ( x ) \, \colon \varepsilon ( a ) = \delta ( a ) \text{ for every } a \in G ^ { \flat } \}.$$

glyph[negationslash]

Since 〈 A glyph[flat] , G glyph[flat] 〉 is reduced and 0 ∈ G glyph[flat] , there is an equation # ≈ d ∈ t such that # ( 0 ) = d ( 0 . Looking at the definition of the basic operations of ) A glyph[flat] we obtain that for every formula g ( x ) , if x really occurs in g , then g ( 0 ) = 0. Then either x does not occur in # or x does not occur in d . We assume w.l.o.g. that x does not occur in # . This means that # is a closed term, i.e. a term of the form t ( 1 , . . . , 1 ) for some term t ( x 1, . . . , xn ) . In particular, we have that A glyph[flat] glyph[satisfies] t ( 1 , . . . , 1 ) ≈ 1 . Together with the definition of t , this implies that the equation d ( x ) ≈ 1 belongs to t .

Now, we claim that the symbol glyph[square] a does not appear in d ( x ) , for every a ∈ A . To prove this, we will show by induction on the construction of d that if the operation glyph[square] a appears in d , then d ( 1 ) = 0. The case where d is a variable is satisfied. Then suppose that d = f ( j 1, . . . , j n ) for some f ∈ F and that glyph[square] a appears in d . Then glyph[square] a appears in some j i . By the inductive hypothesis we have that j i ( 1 ) = 0. Hence we conclude that

$$\delta ( 1 ) = f ( \varphi _ { 1 } ( a ), \dots, \varphi _ { i - 1 } ( 1 ), 0, \varphi _ { i + 1 } ( 1 ), \dots, \varphi _ { n } ( 1 ) ) = 0.$$

The case where d = j + y is handled analogously. Finally, consider the case where d = glyph[square] a j . Observe that j ( 1 ) ∈ { 0, 1 } , since { 0, 1 } is the universe of a subalgebra of A glyph[flat] . Then glyph[square] a ( j ( 1 )) = 0 as desired. This concludes the

inductive proof. Now, recall that 1 ∈ G glyph[flat] and, therefore, that d ( 1 ) = 1. Hence we conclude that glyph[square] a does not appear in d , for every a ∈ A .

We are in the following situation: there is an equation d ≈ 1 in t which satisfies the following requirements:

- 1 . glyph[square] a does not appear in d .
- 2 . d is neither a closed term nor a variable.

glyph[negationslash]

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

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

$$\psi ^ { A } ( a ) ^ { 2 } = \psi ( a ^ { 1 } ) = h ( a ) ^ { 2 }.$$

Hence y represents h in A , i.e. h belongs to the clone of A as desired. glyph[squaremultiply]

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

Theorem 5 5 . . Let 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 K is hard for EXPTIME .

Proof. Let 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 Gen-Clo 1 3 to the problem of determining whether the logic of a finite reduced matrix of finite type belongs to 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 K is hard for EXPTIME . glyph[squaremultiply]

Corollary 5 6 . . Let 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 K is complete for EXPTIME .

Proof. This is a combination of Lemma 3 1 . and Theorem 5 5 . . glyph[squaremultiply]

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 glyph[turnstileleft] is order algebraizable [ 32 , 35 ] if there are a set D ( x y , ) of formulas and a set t ( x ) of inequalities such that for every 〈 A , F 〉 ∈ Mod ∗ ( glyph[turnstileleft] ) the relation glyph[lessorequalslant] F A defined for every a b , ∈ A as

$$a \leqslant _ { A } ^ { F } b \Longleftrightarrow \Delta ( a, b ) \subseteq F$$

is a partial order, and for every a ∈ A

$$a \in F \Longleftrightarrow \langle A, \leqslant _ { A } ^ { F } \rangle \models \tau ( a ).$$

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 glyph[turnstileleft] is order algebraizable to the list of equivalent conditions in the statement of Lemma 5 2 . . This yields the desired hardness result. glyph[squaremultiply]

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 〈 A , F 〉 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 GBP202/12/G061 of the Czech Science Foundation, and by project CZ.02.2.69/0.0/0.0/17 050/0008361, OPVVV Mˇ SMT, MSCA-IF Lidske´ e zdroje v teoreticke´ e informatice.

## 6 . A ppendix

Through this section we assume that A is a fixed non-trivial algebra without constant symbols, and A glyph[natural] is the algebra associated with it as in Section 4 . The subformula tree of a formula j of A glyph[natural] is defined by recursion on the construction of j 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 j is obtained as follows. Suppose that j = g ( y 1, . . . , y n ) for some basic n -ary symbol g and formulas y 1, . . . , y n . First we pick the disjoint union of the subformula trees of y 1, . . . , y n , and we relabel the root of the subformula tree of y i by 〈 y i , i 〉 . Second we add to these trees a common root labelled by j .

Definition 6 1 . . A formula j of A glyph[natural] has the tree property when every node of the subformula tree of j , which is labelled by a formula whose principal symbol belongs to F (plus possibly a natural number), is preceded or equal

to a point which has a label of the form 〈 b , 2 〉 whose immediate predecessor is labelled by ♥ ( a b g , , ) or 〈♥ ( a b g , , ) , n 〉 for some n ∈ w .

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 F contains only a unary symbol f ( x ) . The formulas

$$\bigvee ( x, \Box f ( x ), y ) \text{ and } \bigvee ( \Box z, \bigvee ( f ( z ), f ( f ( x ) ), y ), z )$$

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

![image](https://ac.marcodsn.me/arxiv-markdown-images/1908.00924v1-figure-7e4c107a-72cc-48e2-9e93-b14bbad235a0.jpg)

It is not hard to see that the occurrence of 〈 f ( x ) , 1 〉 in the lefter branch makes the tree property fail. glyph[squaremultiply]

Lemma 6 3 . . If j ( x 1, . . . , xn ) has the tree property, then for every b n ∈ A there glyph[natural] is m glyph[lessorequalslant] 8 such that

$$\varphi ( b ^ { n }, \dots, b ^ { n } ) = b ^ { m }.$$

Moreover, if i ∈ { 1, 3, 4 } , then j ( b i , . . . , b i ) ∈ { b 1 , b 3 , b 4 } .

Proof. We reason by induction on the construction of j . If j is a variable, then the result holds vacuously. Then consider the case where j is a complex formula. If j = f ( y 1, . . . , y n ) for some f ∈ F , then clearly j does not have the tree property. Then consider the case where j = glyph[square] y . Then clearly also y has the tree property. Consider b n ∈ A glyph[natural] . By inductive hypothesis there is m glyph[lessorequalslant] 8 such that y ( b n , . . . , b n ) = b m . Together with the definition of glyph[square] , this implies that

$$\varphi ( b ^ { n }, \dots, b ^ { n } ) = \Box \psi ( b ^ { n }, \dots, b ^ { n } ) = \Box b ^ { m } \in \{ b ^ { 1 }, \dots, b ^ { 8 } \}.$$

Finally, consider the case where j = ♥ ( y 1, y 2, y 3 ) . Clearly y 1 and y 3 must have the tree property. We focus only on y 1. Consider b n ∈ A glyph[natural] . By inductive hypothesis there is m glyph[lessorequalslant] 8 such that y 1 ( b n , . . . , b n ) = b m . Together with the definition of ♥ , this implies that

$$\bigotimes ( \psi _ { 1 }, \psi _ { 2 }, \psi _ { 3 } ) ( b ^ { n }, \dots, b ^ { n } ) \in \{ b ^ { 1 }, \dots, b ^ { 8 } \}.$$

This concludes the inductive argument.

The last part of the statement (the one starting with Moreover... ) is also proved by a simple induction. glyph[squaremultiply]

Lemma 6 4 . . Let j ( x y , ) be a formula and a ∈ A. j ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A if 4 and only if j has the tree property.

Proof. The direction from left to right is proved by induction on the construction of j . The case where j is a variable is clear. Then suppose that j is a complex formula. If j = f ( y 1, . . . , y n ) for some f ∈ F , then j ( a 1 , a 3 ) belongs to A 5, which is disjoint from A 1 ∪ A 3 ∪ A 4. Then suppose that j = glyph[square] y . From glyph[square] y ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4 and the definition of glyph[square] , we can infer that y ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4. By the inductive hypothesis we obtain that y has the tree property. In particular, this is implies that j has the tree property too. Then consider the case where j = ♥ ( y 1, y 2, y 3 ) . From the fact that j ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4, we can infer that y 1 ( a 1 , a 3 ) , y 3 ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4. By the inductive hypothesis, this means that both y 1 and y 3 have the tree property. In particular, this implies that ♥ ( y 1, y 2, y 3 ) has the tree property too.

The direction from right to left also follows from a simple induction. glyph[squaremultiply]

Lemma 6 5 . . For every formula y ( x y , c , glyph[vector] ) glyph[vector] ∈ A , and a glyph[natural] ∈ A, there is b ∈ A and n m , glyph[lessorequalslant] 8 such that y ( a 1 , glyph[vector] c ) = b n and y ( a 3 , glyph[vector] c ) = b m .

Proof. This follows from a simple induction on the construction of y , using the definition of the basic operations of A glyph[natural] . glyph[squaremultiply]

As a consequence we obtain the following:

Corollary 6 6 . . Let f ∈ F be n-ary and j 1 ( x y , glyph[vector] ) , . . . , j n ( x y , glyph[vector] ) be terms of A glyph[natural] . For every a ∈ A and c glyph[vector] ∈ A we have glyph[natural]

$$f ( \varphi _ { 1 }, \dots, \varphi _ { n } ) ( a ^ { 1 }, \vec { c } ) = f ( \varphi _ { 1 }, \dots, \varphi _ { n } ) ( a ^ { 3 }, \vec { c } ).$$

Proof. By Lemma 6 5 . there are b 1, . . . , bn ∈ A and k 1, . . . , kn , m 1, . . . , mn glyph[lessorequalslant] 8 such that

$$\varphi _ { i } ( a ^ { 1 }, \vec { c } ) = b _ { i } ^ { m _ { i } } \text{ and } \varphi _ { i } ( a ^ { 3 }, \vec { c } ) = b _ { i } ^ { k _ { i } }.$$

This implies that

$$\text{es that} \\ f ( \varphi _ { 1 }, \dots, \varphi _ { n } ) ( a ^ { 1 }, \vec { c } ) & = f ( b _ { 1 } ^ { m _ { 1 } }, \dots, b _ { n } ^ { m _ { n } } ) \\ & = f ^ { A } ( b _ { 1 }, \dots, b _ { n } ) ^ { 5 } \\ & = f ( b _ { 1 } ^ { k _ { 1 } }, \dots, b _ { n } ^ { k _ { n } } ) \\ & = f ( \varphi _ { 1 }, \dots, \varphi _ { n } ) ( a ^ { 3 }, \vec { c } ) \\ \sigma \text{ the nroof}$$

concluding the proof.

glyph[squaremultiply]

glyph[negationslash]

Lemma 6 7 . . Let j ( x y , ) be a formula and a ∈ A. If j ( a 1 , a 3 ) = j ( a 1 , a 1 ) , then j ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A . 4

glyph[negationslash]

glyph[negationslash]

Proof. We reason by induction on the construction of j . The case where it is a variable is satisfied. Then suppose that j is a complex formula. If j = f ( y 1, . . . , y n ) for some f ∈ F , then by Corollary 6 6 . we obtain that j ( a 1 , a 3 ) = j ( a 1 , a 1 ) , which is false. Then suppose that j = glyph[square] y . From glyph[square] y ( a 1 , a 3 ) = y ( a 1 , a 1 ) it follows that y ( a 1 , a 3 ) = y ( a 1 , a 1 ) . By inductive hypothesis we obtain that y ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4. Together with the

glyph[negationslash]

definition of glyph[square] , this implies that j ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4 as well. It only remains to consider the case where j = ♥ ( y 1, y 2, y 3 ) . From the fact that j ( a 1 , a 3 ) = j ( a 1 , a 1 ) it follows that one of the following conditions holds:

glyph[negationslash]

- 1 . y 1 ( a 1 , a 3 ) = y 1 ( a 1 , a 1 ) .

glyph[negationslash]

- 2 . y 2 ( a 1 , a 3 ) = y 2 ( a 1 , a 1 ) and 1 does not hold.

glyph[negationslash]

- 3 . y 3 ( a 1 , a 3 ) = y 3 ( a 1 , a 1 ) and neither 1 not 2 hold.

We consider these cases separately:

- 1 . By the inductive hypothesis we have that y 1 ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4. If y 3 ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4, then by definition of ♥ we conclude that j ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4 and we are done. Then suppose towards a contradiction that y 3 ( a 1 , a 3 ) / ∈ A 1 ∪ A 3 ∪ A 4. By Lemma 6 4 . we know that y 3 does not have the tree property. Together with the definition o A glyph[natural] , this implies that y 3 ( a 1 , a 1 ) / ∈ A 1 ∪ A 3 ∪ A 4 too. Moreover, by Lemma 6 4 . we know that y 1 has the tree property. Together with Lemma 6 3 . this implies that

$$\psi _ { 1 } ( a ^ { 1 }, a ^ { 1 } ), \psi _ { 1 } ( a ^ { 1 }, a ^ { 3 } ) \in \{ a ^ { 1 }, a ^ { 3 }, a ^ { 4 } \}.$$

Thus we obtain that

$$\bigvee ( \psi _ { 1 }, \psi _ { 2 }, \psi _ { 3 } ) ( a ^ { 1 }, a ^ { 3 } ) = a ^ { 7 } = \bigvee ( \psi _ { 1 }, \psi _ { 2 }, \psi _ { 3 } ) ( a ^ { 1 }, a ^ { 1 } )$$

glyph[negationslash]

contradicting the fact that j ( a 1 , a 3 ) = j ( a 1 , a 1 ) .

glyph[negationslash]

2 . We will show that this case leads to a contradiction, that is to say that it never happens. If y 2 ( a 1 , a 3 ) = y 2 ( a 1 , a 1 ) , then by inductive hypothesis this means that y 2 ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4. By Lemma 6 4 . we know that y 2 has the tree property and by Lemma 6 3 . that y 2 ( a 1 , a 1 ) ∈ A 1 ∪ A 3 ∪ A 4 as well. Consider b ∈ A and n glyph[lessorequalslant] 8 such that y 1 ( a 1 , a 1 ) = y 1 ( a 1 , c 3 ) = b n . By definition of ♥ we have that

$$\varphi ( a ^ { 1 }, a ^ { 1 } ) = \begin{cases} \ b ^ { 4 } & \text{if $\psi_{1}(a^{1},a^{1}),\psi_{3}(a^{1},a^{1}) \in A_{1}\cup A_{3}\cup A_{4}$} \\ \ b ^ { 7 } & \text{otherwise.} \end{cases}$$

$$\varphi ( a ^ { 1 }, a ^ { 3 } ) = \begin{cases} \ b ^ { 4 } & \text{if $\psi_{1}(a^{1},a^{3}),\psi_{3}(a^{1},a^{3}) \in A_{1}\cup A_{3}\cup A_{4}$} \\ \ b ^ { 7 } & \text{otherwise.} \end{cases}$$

glyph[negationslash]

glyph[negationslash]

Since y 1 ( a 1 , a 1 ) = y 1 ( a 1 , a 3 ) by assumption and j ( a 1 , a 1 ) = j ( a 1 , a 3 ) , we have that y 3 ( a 1 , a 1 ) = y 3 ( a 1 , a 3 ) . By inductive hypothesis this means that y 3 ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4. By Lemmas 6 4 . and 6 4 . we obtain that y 3 ( a 1 , a 1 ) ∈ A 1 ∪ A 3 ∪ A 4 too. But this implies that

$$\varphi ( a ^ { 1 }, a ^ { 1 } ) = a ^ { 4 } = \varphi ( a ^ { 1 }, a ^ { 3 } )$$

glyph[negationslash]

contradicting the fact that j ( a 1 , a 1 ) = j ( a 1 , a 3 ) .

- 3 . By inductive hypothesis we have that y 3 ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4. Suppose towards a contradiction that j ( a 1 , a 3 ) / ∈ A 1 ∪ A 3 ∪ A 4. Then we have that y 1 ( a 1 , a 3 ) / ∈ A 1 ∪ A 3 ∪ A 4. Consider b ∈ A and n glyph[lessorequalslant] 8 such that b n = y 1 ( a 1 , a 3 ) . By the definition of ♥ we have that j ( a 1 , a 3 ) = b 7 . On the other hand, observe that applying Lemmas 6 4 . and 6 3 . to the fact that

glyph[negationslash]

y 3 ( a 1 , a 3 ) ∈ A 1 ∪ A 3 ∪ A 4, we obtain that y 3 ( a 1 , a 1 ) ∈ A 1 ∪ A 3 ∪ A 4 as well. Together with the fact that y 1 ( a 1 , a 1 ) = y 1 ( a 1 , a 3 ) / ∈ A 1 ∪ A 3 ∪ A 4, this implies that j ( a 1 , a 1 ) = b 7 . But this contradicts the fact that j ( a 1 , a 1 ) = j ( a 1 , a 3 ) . glyph[squaremultiply]

## R eferences

- [ 1 ] H. Albuquerque, J. M. Font, R. Jansana, and T. Moraschini. Assertional logics, truthequational logics, and the hierarchies of abstract algebraic logic. In J. Czelakowski, editor, Don Pigozzi on Abstract Algebraic Logic and Universal Algebra , volume 16 of Outstanding Contributions . Springer-Verlag, 2018 .
- [ 2 ] S. Arora and B. Barak. Computational Complexity: A Modern Approach . Cambridge University Press, 2009 .
- [ 3 ] C. Bergman. Universal Algebra: Fundamentals and Selected Topics . Chapman &amp; Hall Pure and Applied Mathematics. Chapman and Hall/CRC, 2011 .
- [ 4 ] C. Bergman, D. Juedes, and G. Slutzki. Computational complexity of term-equivalence. International Journal of Algebra and Computation , 9 1 ( ): 113 128 -, 1999 .
- [ 5 ] J. Berman. The structure of free algebras. In Structural theory of automata, semigroups, and universal algebra , volume 207 of NATO Sci. Ser. II Math. Phys. Chem. , pages 47 76 -. Springer, Dordrecht, 2005 .
- [ 6 ] W. J. Blok and B. J´nsson. Algebraic structures for logic. A course given at the o 2 3 rd Holiday Mathematics Symposium, New Mexico State University, 1999 .
- [ 7 ] W. J. Blok and B. J´nsson. Equivalence of consequence operations. o Studia Logica , 83 1 ( -3 ): 91 -110 , 2006 .
- [ 8 ] W. J. Blok and D. Pigozzi. Algebraizable logics , volume 396 of Mem. Amer. Math. Soc. A.M.S., Providence, January 1989 .
- [ 9 ] W. J. Blok and D. Pigozzi. Algebraic semantics for universal Horn logic without equality. pages 1 -56 . Heldermann, Berlin, 1992 .
- [ 10 ] W. J. Blok and J. Rebagliato. Algebraic semantics for deductive systems. Studia Logica, Special Issue on Abstract Algebraic Logic, Part II , 74 5 ( ): 153 180 -, 2003 .
- [ 11 ] J. Czelakowski. Reduced products of logical matrices. Studia Logica , 39 19 : -43 , 1980 .
- [ 12 ] J. Czelakowski. Protoalgebraic logics , volume 10 of Trends in Logic-Studia Logica Library . Kluwer Academic Publishers, Dordrecht, 2001 .
- [ 13 ] P. Dellunde and R. Jansana. Some characterization theorems for infinitary universal Horn logic without equality. The Journal of Symbolic Logic , 61 4 ( ): 1242 1260 -, 1996 .
- [ 14 ] J. M. Font. Abstract Algebraic Logic - An Introductory Textbook , volume 60 of Studies in Logic - Mathematical Logic and Foundations . College Publications, London, 2016 .
- [ 15 ] J. M. Font and R. Jansana. A general algebraic semantics for sentential logics , volume 7 of Lecture Notes in Logic . A.S.L., second edition 2017 edition, 2009 . First edition 1996 . Electronic version freely available through Project Euclid at projecteuclid.org/ euclid.lnl/1235416965 .
- [ 16 ] J. M. Font, R. Jansana, and D. Pigozzi. A survey on abstract algebraic logic. Studia Logica, Special Issue on Abstract Algebraic Logic, Part II , 74 1 ( - ): 2 13 -97 , 2003 . With an 'Update' in 91 ( 2009 ), 125 130 -.
- [ 17 ] R. Freese and M. A. Valeriote. On the complexity of some Maltsev conditions. International Journal of Algebra and Computation , 19 1 ( ): 41 -77 , 2009 .
- [ 18 ] O. C. Garc´ ıa and W. Taylor. The lattice of interpretability types of varieties , volume 50 . Mem. Amer. Math. Soc., 1984 .
- [ 19 ] G. Gr¨ atzer. Two Mal'cev-Type Theorems in Universal Algebra. Journal of Combinatorial Theory , 8 334 : -342 , 1970 .
- [ 20 ] J. Hartmanis and R. E. Stearns. On the computational complexity of algorithms. Transactions of the Americal Mathematical Society , 117 285 : -306 , 1965 .

## TOMMASO MORASCHINI

- [ 21 ] D. Hobby. Finding type sets is NP-hard. International Journal of Algebra and Computation , 1 4 ( ): 437 444 -, 1991 .
- [ 22 ] D. Hobby and R. McKenzie. The structure of finite algebras , volume 76 of Contemporary Mathematics . American Mathematical Society, Providence, RI, 1988 .
- [ 23 ] J. Hopcroft. An n log n algorithm for minimizing states in a finite automaton. Theory of machines and computations , Proc. Internat. Sympos., Technion, Haifa, 1971 , 189 196 -.
- [ 24 ] R. Jansana and T. Moraschini. The poset of all logics I: interpretations and lattice structure. Manuscript, 2019 . Available online at http://uivty.cs.cas.cz/ ~ moraschini/ files/submitted/poset-all-logics-1.pdf .
- [ 25 ] R. Jansana and T. Moraschini. The poset of all logics II: Leibniz classes and hierarchy. Manuscript, 2019 .
- [ 26 ] R. Jansana and T. Moraschini. The poset of all logics III: finitely presentable logics. Manuscript, 2019 .
- [ 27 ] K. A. Kearnes and E. W. Kiss. The shape of congruences lattices , volume 222 of Mem. Amer. Math. Soc. Ameican Mathematical Society, 2013 . Monograph.
- [ 28 ] R. N. McKenzie, G. F. McNulty, and W. F. Taylor. Algebras, lattices, varieties. Vol. I . The Wadsworth &amp; Brooks/Cole Mathematics Series. Wadsworth &amp; Brooks/Cole Advanced Books &amp; Software, Monterey, CA, 1987 .
- [ 29 ] T. Moraschini. A computational glimpse at the Leibniz and Frege hierarchies. Annals of Pure and Applied Logic , 169 1 ( ): 1 -20 , January 2018 .
- [ 30 ] T. Moraschini. A study of the truth predicates of matrix semantics. Review of Symbolic Logic , 11 4 ( ): 780 804 -, 2018 .
- [ 31 ] C. H. Papadimitriou. Computational complexity . Addison-Wesley Publishing Company, Reading, MA, 1994 .
- [ 32 ] J. G. Raftery. Correspondences between Gentzen and Hilbert systems. The Journal of Symbolic Logic , 71 3 ( ): 903 957 -, 2006 .
- [ 33 ] J. G. Raftery. The equational definability of truth predicates. Reports on Mathematical Logic , ( 41 ): 95 -149 , 2006 .
- [ 34 ] J. G. Raftery. A perspective on the algebra of logic. Quaestiones Mathematicae , 34 275 : -325 , 2011 .
- [ 35 ] J. G. Raftery. Order algebraizable logics. Annals of Pure and Applied Logic , 164 3 ( ): 251 283 -, 2013 .
- [ 36 ] W. Taylor. Characterizing Mal'cev conditions. Algebra Universalis , 3 351 : -397 , 1973 .

I nstitute of C omputer S cience , A cademy of S ciences of C zech R epublic , P od V odarenskou vezi ´ ˇ ˇ´ 271/2, 182 07 P rague 8, C zech R epublic

E-mail address : moraschini@cs.cas.cz
T. Moraschini
On the complexity of the Leibniz hierarchy
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.