## A COMPUTATIONAL GLIMPSE AT THE LEIBNIZ AND FREGE HIERARCHIES

## TOMMASO MORASCHINI

A bstract . In this paper we consider, from a computational point of view, the problem of classifying logics within the Leibniz and Frege hierarchies typical of abstract algebraic logic. The main result states that, for logics presented syntactically, this problem is in general undecidable. More precisely, we show that there is no algorithm that classifies the logic of a finite consistent Hilbert calculus in the Leibniz and in the Frege hierarchies.

Dedicated to Professor Josep Maria Font on the occasion of his retirement

## 1 . I ntroduction

Abstract algebraic logic (AAL for short) is a field that studies uniformly propositional logics [ 14 , 11 , 15 , 16 ]. One of its main achievements is the development of the so-called Leibniz and Frege hierarchies in which propositional logics are classified according to two different criteria. More precisely, the Leibniz hierarchy provides a taxonomy that classifies propositional systems accordingly to the way their notions of logical equivalence and of truth can be defined. Roughly speaking, the location of a logic inside the Leibniz hierarchy reflects the strength of the relation that it enjoys with its algebraic counterpart. In this sense, the Leibniz hierarchy revealed to be a useful framework where to express general transfer theorems between metalogical and algebraic properties. This is the case for example for superintuitionistic logics [ 10 ], where the Beth definability property corresponds to the fact that epimorphisms are surjective [ 5 , 4 , 21 , 22 ], and the deductive interpolation corresponds to the amalgamation property [ 12 , 21 , 24 ]. On the other hand, the Frege hierarchy offers a classification of logics according to general replacement principles. Remarkably, some of these replacement properties can be formulated semantically by asking that the different elements in a model of the logic are separated by a deductive filter. This is what happens for example in superintuitionistic logics, whose algebraic semantics is given by varieties of Heyting algebras where logical filters are just lattice filters.

The aim of this paper is to investigate the computational aspects of the problem of classifying syntactically presented logics in the Leibniz and Frege hierarchies. More precisely, we will consider the following problem:

- · Let K be a level of the Leibniz (resp. Frege) hierarchy. Is it possible to decide whether the logic of a given finite consistent Hilbert calculus in a finite language belongs to K ?

It turns out that in general the answer is negative both for the Leibniz and the Frege hierarchies. To show the first case, we reduce Hilbert's tenth problem on Diophantine equations to the problem of classifying the logic of a (finite consistent) Hilbert calculus in the Leibniz hierarchy, thus obtaining that also the last one is undecidable (Theorem 4 10 . ). In the process we will also describe and axiomatize a new logic, whose deductions mimic the equational theory of commutative rings with unity (Theorem 4 6 . ). In order to prove that also the problem of classifying the logic of a (finite and consistent) Hilbert calculus in the Frege hierarchy is undecidable, we rely on the undecidability of the equational theory of relation algebras in a single variable [ 26 ]. Remarkably, our proof shows that this classification problem remains undecidable even if we restrict our attention to Hilbert calculi that determine a finitary algebraizable logic (Theorem 5 3 . ).

## 2 . P reliminaries

Here we present a brief survey of the main definitions and results of abstract algebraic logic we will make use of along the article; a systematic exposition can be found for example in [ 6 , 7 , 11 , 14 , 15 , 16 ].

A closure operator over a set A is a monotone function C : P ( A ) →P ( A ) such that X ⊆ C X ( ) = C C X ( ( ) ) for every X ∈ P ( A ) , and a closure system on A is a family C ⊆ P ( A ) closed under arbitrary intersections and such that A ∈ C . It is well known that the closed sets (fixed points) of a closure operator form a closure system and that given a closure system C one can define a closure operator C by letting C X ( ) = ⋂ { Y ∈ C | X ⊆ Y } for every X ∈ P ( A ) . These transformations are indeed inverse to one another. Therefore definitions and results established for closure operators transfer naturally to closure systems and vice-versa. Let C ⊆ P ( A ) be a closure system on A . We say that an element a ∈ A is a theorem of C if a ∈ ⋂ C .

Fixed an algebraic type L and a set X , we denote by Fm X ( ) the set of formulas over L built up with variables in X and by Fm ( X ) the corresponding absolutely free algebra. In particular we fix a countable set Var of variables x y z , , , etc., and we write Fm and Fm instead of Fm Var ( ) and Fm ( Var ) . Moreover, given a formula j ∈ Fm , we write j ( x z , glyph[vector] ) if the variables of j are among x and glyph[vector] z and x does not appear in glyph[vector] z . From now on we assume that we are working with a fixed algebraic type.

By a logic L we understand a closure operator C L : P ( Fm ) → P ( Fm ) which is structural in the sense that s C L ⊆ C L s for every endomorphism (i.e. substitution) s : Fm → Fm . Given G ∪ { j } ⊆ Fm we write G glyph[turnstileleft] L j instead of j ∈ C L ( G ) . Moreover, given G ∪ { j y , } ⊆ Fm , we denote by G j , glyph[turnstileright] glyph[turnstileleft] L y G , the fact that both G j , glyph[turnstileleft] L y and G y , glyph[turnstileleft] L j are true. Given two logics L and L ′ , we write L glyph[lessorequalslant] L ′ if C L ( G ) ⊆ C L ′ ( G ) for every G ⊆ Fm .

A logic L is consistent when there is a formula j such that ˘ glyph[notturnstile] L j . Since L always denotes an arbitrary logic, we skip, in the formulation of our results, assumptions like 'let L be a logic'.

A logic L is finitary if for every G ∪ { j } ⊆ Fm such that j ∈ C L ( G ) , there is a finite subset G ′ ⊆ G such that j ∈ C L ( G ′ ) . In this paper, we will focus only on finitary logics. A rule is an expression of the form G glyph[turnstileleft] j , where G ∪{ } j is a finite set of formulas. Given two finite sets of formulas G and G ′ , the expression G glyph[turnstileright] glyph[turnstileleft] G ′ is an abbreviation for the rules G glyph[turnstileleft] j and G ′ glyph[turnstileleft] y for every j ∈ G ′ and y ∈ G . A Hilbert calculus is a set of rules. It is well known that every Hilbert calculus determines a finitary logic and, vice-versa, that every finitary logic is determined by a Hilbert calculus. An Hilbert calculus is consistent , when so is the logic it determines. For the notion of proof in a Hilbert calculus we refer the reader to [ 11 , pag. 28 ].

We denote algebras with bold capital letters A B C , , , etc. (with universes A B C , , , etc. respectively). We skip assumptions like 'let A be an algebra' in the formulation of our results. Given an algebra A , we denote its congruence lattice by Con A . The identity relation on A is denoted by Id A . Given q ∈ Con A , we denote the natural surjection onto the quotient by pq : A → A / . A congruence q q ∈ Con A is compatible with a set F ⊆ A if for every a b , ∈ A

$$\text{if $\langle a,b\rangle\in\theta$ and $a\in F$, then $b\in F$.}$$

Given F ⊆ A , there exists always that largest congruence on A compatible with F [ 14 , Theorem 4 20 . ]. We denote it by W A F and call it the Leibniz congruence of F on A . The Leibniz congruence can be characterized in terms of the indiscernibility of elements with respect to filters in the following way [ 14 , Theorem 4 23 . ]. Given an algebra A , a function p : A n → A is a polynomial function if there are a natural number m , a formula j ( x 1, . . . , xn + m ) , and elements b 1, . . . , bm ∈ A such that

$$p ( a _ { 1 }, \dots, a _ { n } ) = \varphi ^ { A } ( a _ { 1 }, \dots, a _ { n }, b _ { 1 }, \dots, b _ { m } )$$

for every a 1, . . . , an ∈ A . Observe that the notation j ( x 1, . . . , xn + m ) means just that the variables really occurring in j are among, but are not necessarily all, the elements of { x 1, . . . , xn + m } . We denote by Pol A the set of all polynomial functions of A .

Lemma 2 1 . . Let A be an algebra, F ⊆ A and a b , ∈ A. 〈 a b , 〉 ∈ W A F if and only if for every unary p ∈ Pol A ,

$$p ( a ) \in F \Longleftrightarrow p ( b ) \in F.$$

A matrix is a pair 〈 A , F 〉 such that F ⊆ A . The set F is called the filter or the truth set of the matrix. A matrix 〈 A , F 〉 is reduced if W A F = Id A .

Given a logic L and an algebra A , we say that a set F ⊆ A is a deductive filter of L over A when

$$\text{if } \Gamma \vdash _ { \mathcal { L } } \varphi, \text{ then for every homomorphism } h \colon F m \to A, \\ \text{ if } h [ \Gamma ] \subseteq F, \text{ then } h ( \varphi ) \in F$$

for every G ∪{ } ⊆ j Fm . We denote by F L i A the set of deductive filters of L over A , which turns out to be a closure system [ 14 , Proposition 2 22 . ]. Thus, we denote by Fi A L ( ) · the closure operator of L -filter generation over the algebra A . The class of reduced models of a given a logic L is the following:

$$\text{Mod} ^ { * } \mathcal { L } \coloneqq \{ \langle A, F \rangle \, \colon F \in \mathcal { F } i _ { \mathcal { L } } A \text{ and } \mathfrak { Q } ^ { A } F = \text{Id} _ { A } \}.$$

Given an algebra A , a logic L and a set F ⊆ A , the congruence

$$\widetilde { \Omega } _ { \mathcal { L } } ^ { A } F \coloneqq \bigcap \{ \Omega ^ { A } G \, \colon G \in \mathcal { F } i _ { \mathcal { L } } A \text{ and } F \subseteq G \}$$

is called the Suszko congruence of F over A (relative to L ). The Suszko congruence allows to associate a special class of algebras with a given logic L as follows:

$$\text{Alg} \mathcal { L } \coloneqq \{ A \, \colon \, \text{there is } F \in \mathcal { F } i _ { \mathcal { L } } A \, \text{such that } \widetilde { \mathcal { O } } ^ { A } _ { \mathcal { L } } F = \text{Id} _ { A } \}.$$

## 3 . T he hierarchies of AAL

One of the main achievements of abstract algebraic logic is the development of the so-called Leibniz and Frege hierarchies , in which propositional logics L are classified by means of properties that reflect the strength (or weakness) of the relation that they enjoy with Alg L . We begin by describing the main classes of logics that constitute the Leibniz hierarchy (see Figure 1 , where arrows denote the inclusion relation). In order to follow a uniform approach we chose to do this from a semantic point of view, even if some of these concepts were originally defined in some different ways. The main idea, which lies behind the development of the Leibniz hierarchy, is that propositional logics can be characterized by means of two basic features: the fact that logical equivalence (which is identified with the Leibniz congruence) is definable by means of formulas, and the fact that the truth sets in Mod ∗ L are definable either implicitly or by means of equations.

A logic L is protoalgebraic if there is a set of formulas r ( x y z , , glyph[vector] ) in two variables x and y (possibly) with parameters glyph[vector] z such that for every algebra A , every F ∈ F L i A and every a b , ∈ A

$$\langle a, b \rangle \in \mathfrak { Q } ^ { A } F \Longleftrightarrow \rho ^ { A } ( a, b, \vec { c } ) \subseteq F \text{ for every } \vec { c } \in A.$$

In this case r ( x y z , , glyph[vector] ) is a set of congruence formulas with parameters for L . Analogously, a logic is called equivalential if there is set of formulas r ( x y , ) in two variables and without parameters which satisfies ( 1 ). In this case r ( x y z , , glyph[vector] ) is called a set of congruence formulas for L . Protoalgebraic logics can be characterized syntactically as follows [ 14 , Proposition 6 7 .

|

|

"

"

|

|

|

|

"

"

|

|

"

"

"

"

|

|

"

"

|

|

"

"

"

"

|

|

"

![image](https://ac.marcodsn.me/arxiv-markdown-images/1908.00922v1-figure-c4ed6fe3-c410-4c27-a799-28e71c28db62.jpg)

"

F igure 1 . The Leibniz hierarchy.

and Theorem 6 57 . ]. A set of formulas in two variables r ( x y , ) is a set of protoimplication formulas for a logic L if the following conditions hold:

$$\emptyset \vdash _ { \mathcal { L } } \rho ( x, x )$$

$$x, \rho ( x, y ) \vdash _ { \mathcal { L } } y$$

Theorem 3 1 . . A logic L is protoalgebraic if and only if it has a set of protoimplication formulas.

Truth is equationally definable in a class of matrices M if there is a set t ( x ) of equations in variable x such that for every 〈 A , F 〉 ∈ M ,

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

Truth is implicitly definable in a class of matrices M if the matrices in M are determined by their algebraic reducts, in the sense that if 〈 A , F 〉 , 〈 A , G 〉 ∈ M , then F = G . Clearly equational definability implies implicit definability. A logic L is truth-equational if truth is equationally definable in Mod ∗ L .

A logic L is weakly algebraizable if it is both protoalgebraic and truthequational. It is algebraizable if it is both equivalential and truth-equational. Algebraizable logics enjoy the following syntactic characterization [ 14 , Theorem 3 21 . ]:

"

"

Theorem 3 2 . . A logic L is algebraizable if and only if there are a set of equations t ( x ) and a set of formulas r ( x y , ) such that:

$$\varnothing \vdash _ { \mathcal { L } } \rho ( x, x )$$

$$x, \rho ( x, y ) \vdash _ { \mathcal { L } } y$$

$$\bigcup _ { i \leqslant n } \rho ( x _ { i }, y _ { i } ) \vdash _ { \mathcal { L } } \rho ( \lambda x _ { 1 } \dots x _ { n }, \lambda y _ { 1 } \dots y _ { n } )$$

$$x \dashv \vdash _ { \mathcal { L } } \{ \varphi ( \varepsilon, \delta ) \colon \varphi ( x, y ) \in \rho \, a n d \, \varepsilon \approx \delta \in \tau \} \quad \quad ( A _ { 3 } )$$

for every n-ary function symbol l . In this case r ( x y , ) a set of congruence formulas for L .

Lemma 3 3 . . Let L be an algebraizable logic with set of congruence formulas r ( x y . For every , ) j y , ∈ Fm, we have

$$\emptyset \vdash _ { \mathcal { L } } \rho ( \varphi, \psi ) \Longleftrightarrow \text{Al} \mathfrak { g L } \models \varphi \approx \psi.$$

A logic L is assertional if there is a class K of algebras with a constant term 1 such that for every G ∪{ } ⊆ j Fm ,

$$\Gamma \vdash _ { \mathcal { L } } \varphi \Longleftrightarrow & \text{ for every $A\in K$ and homomorphism $h\colon Fm\to A$}, \\ & \text{ if $h[\Gamma]\subseteq \{1\}$, then $h(\varphi)=1$}.$$

A logic L is regularly ( weakly ) algebraizable if it is assertional and (weakly) algebraizable. Regularly algebraizable logics enjoy a syntactic characterization [ 14 , Theorem 3 52 . ].

Lemma 3 4 . . Let L be an algebraizable logic. L is regularly algebraizable if and only if

$$x, y \vdash _ { \mathcal { L } } \rho ( x, y )$$

for some (or, equivalently, every) of its sets of congruence formulas r ( x y . , )

Finally a logic L is finitely equivalential (resp. finitely algebraizable, finitely regularly algebraizable ) if it is equivalential (resp. algebraizable, regularly algebraizable) and it has a finite set of congruence formulas.

Now we turn to describe briefly the structure of the other hierarchy typical of abstract algebraic logic, namely the Frege hierarchy (see Figure 2 , where arrows denote the inclusion relation). In this hierarchy logics are classified by means of general replacement properties, but we choose here to define them by the most convenient equivalent characterization. A logic L is selfextensional if the relation glyph[turnstileright] glyph[turnstileleft] L is a congruence on Fm . In particular, we will make use of the following easy observation [ 15 , Proposition 2 43 . ].

Lemma 3 5 . . Let L be selfextensional and a b , ∈ Fm. If a glyph[turnstileright] glyph[turnstileleft] L b , then Alg L glyph[satisfies] a ≈ b .

A logic L is fully selfextensional if for every A ∈ Alg L and a b , ∈ A :

$$\text{if } F i _ { \mathcal { L } } ^ { A } \{ a \} = F i _ { \mathcal { L } } ^ { A } \{ b \}, \text{ then } a = b.$$

|

"

"

|

"

![image](https://ac.marcodsn.me/arxiv-markdown-images/1908.00922v1-figure-568b7514-8d86-4761-baf5-6de15f9ac37a.jpg)

"

|

|

F igure 2 . The Frege hierarchy.

Fully selfextensional logics are also selfextensional, while the converse is not true in general [ 2 ]. A logic L is Fregean if for every n -ary function symbol l and formulas G ∪{ a 1, . . . , a n , b 1, . . . , b n } ⊆ Fm , if G a , i glyph[turnstileright] glyph[turnstileleft] L b i , G for every i glyph[lessorequalslant] n , then G l a , ( 1, . . . , a n ) glyph[turnstileright] glyph[turnstileleft] L l b ( 1, . . . , b n ) , G . Finally L is fully Fregean if for every algebra A ∈ Alg L and every F ∈ F L i A we have that

$$\Phi \text{ if } F i _ { \mathcal { L } } ^ { A } ( F \cup \{ a \} ) = F i _ { \mathcal { L } } ^ { A } ( F \cup \{ b \} ), \text{ then } \langle a, b \rangle \in \widetilde { \mathbf \Omega } _ { \mathcal { L } } ^ { A } F.$$

## 4 . T he classification problem in the L eibniz hierarchy

We will begin our tour around some computational aspects of abstract algebraic logic by considering the problem of classifying logics in the Leibniz hierarchy. The goal of this part is to prove that the problem of classifying logics determined by a finite consistent Hilbert calculus in a finite language in the Leibniz hierarchy is in general undecidable (Theorem 4 10 . ). Our strategy is the following: for every Diophantine equation p ≈ 0 we define a finite consistent Hilbert calculus L ( p ) such that L ( p ) belongs to a given level of the Leibniz hierarchy if and only if p ≈ 0 has an integer solution (Definition 4 7 . and Theorem 4 8 . ). For the sake of completeness we recall some concepts. An algebra A = 〈 A , + , · , -, 0, 1 〉 of type 〈 2, 2, 1, 0, 0 〉 is a commutative ring if 〈 A , + , -, 0 〉 is an Abelian group, 〈 A , · , 1 〉 is a commutative monoid, and

$$a \cdot ( b + c ) = ( a \cdot b ) + ( a \cdot c )$$

for every a b c , , ∈ A . We denote by CR the variety of commutative rings. The algebra Z : = 〈 Z , + , · , -, 0, 1 〉 , where Z is the collection of integer numbers, is a commutative ring. A Diophantine equation is an equation of the form p z ( 1, . . . , z 1 ) ≈ 0, where p z ( 1, . . . , z 1 ) is a term in the language of commutative rings. Hilbert's tenth problem asked for an algorithm that, given a Diophantine equation, tells us whether it has a solution in Z or not. Matiyasevich showed that such an algorithm does not exist [ 25 ], see also [ 3 ]. In other words, the problem of determining whether a given Diophantine equation has an integer solution is undecidable.

In order to relate this problem to the one of the classification of logics into the Leibniz hierarchy, we will construct a logic that mimics the behaviour of (Diophantine) equations in commutative rings. In [ 17 ] (see also [ 19 ]) a way of doing this for arbitrary varieties is described. More precisely, given a non-trivial variety V , we let L V be the logic determined by the following class of matrices:

$$\{ \langle A, F \rangle \colon A \in \mathbf V \text{ and } F \subseteq A \}.$$

Given G ∪ { j } ⊆ Fm , we will write G glyph[turnstileleft] V j as a shortening for G glyph[turnstileleft] L V j . The following result will be used later on:

Lemma 4 1 . . Let V be a non-trivial variety and G ∪{ } ⊆ j Fm.

- 1 . Alg ∗ L V ⊆ Alg L V = V .
- 2 . L V is fully selfextensional.
- 3 . G glyph[turnstileleft] V j if and only if there is g ∈ G such that V glyph[satisfies] g ≈ j .

Proof. Point 1 and 2 are respectively Theorem 3 5 . and Corollary 3 6 . of [ 17 ]. Point 3 , even if not explicit stated there, is a direct consequence of Lemmas 3 3 . and 3 9 . of [ 17 ]. glyph[squaremultiply]

Digression. Next we are going to axiomatize the logic L CR , but first let us consider the general problem of axiomatizing the logic L V for an arbitrary non-trivial variety V . Suppose that we are given an equational basis S for V . It would be nice to have a natural way of transforming S into an axiomatization of the logic L V . This can be done easily, adapting Birkhoff's Completeness Theorem of equational logic [ 9 , Theorem 14 19 . , Section II], if what we are looking for is a Gentzen system adequate to L V [ 20 , Theorem 1 2 . ]. 1 On the contrary, it is not straightforward to build a nice Hilbert calculus for L V out of S . In particular, the obvious idea of considering the logic axiomatized by the rules a glyph[turnstileright] glyph[turnstileleft] b for all a ≈ b ∈ S does not work in general. For example, it is the case that the logic S determined by the rules

$$x \dashv \vdash x \wedge x \quad x \wedge y \dashv \vdash y \wedge x \quad x \wedge ( y \wedge z ) \dashv \vdash ( x \wedge y ) \wedge z \quad ( z )$$

is not the logic L SL associated with the variety of semilattices SL (cfr. [ 17 , Example 3 8 . ]). This is because the matrix 〈 Z 3, { 1, 2 }〉 , where Z 3 is the additive semigroup of integers modulo 3 , is easily proved to be a reduced model of S . In particular this implies that Z 3 ∈ Alg S and, therefore, that Alg S glyph[negationslash] = SL . Hence S glyph[negationslash] = L SL , by point 1 of Lemma 4 1 . . In order to obtain a complete Hilbert-style axiomatization of L SL one has to add to the rules in ( 2 ) the following ones:

$$\smile & u \wedge x \dashv \vdash u \wedge ( x \wedge x ) \\ u \wedge ( x \wedge y ) \dashv \vdash u \wedge ( y \wedge x ) \\ u \wedge ( x \wedge ( y \wedge z ) ) \dashv \vdash u \wedge ( ( x \wedge y ) \wedge z )$$

1 Even if we won't pursue this here, it is possible to show that there is no Gentzen system fully adequate to L V in the sense of [ 15 ].

This is mainly due to the fact that selfextensionality, which is not easily expressible by means of Hilbert-style rules, fails for S , while L SL is selfextensional by point 2 of Lemma 4 1 . .

Even if it is not straightforward to present an explicit Hilbert-style axiomatization of L V , given a base S for V , one may wonder whether there exists (no matter which one) a finite Hilbert-style axiomatization of L V when S is finite. In the next example we show that in general this is not the case.

Example 4 2 . ( Finite Axiomatizability ) . An algebra A = 〈 A , ·〉 is a commutative magma if · is a binary commutative operation. Clearly the class of commutative magmas forms a finitely based variety, which we denote by CM . We will prove that the logic L CM is not axiomatizable by means of a finite set of Hilbert-style rules. In order to do this, let CM be a finite set of rules holding in L CM . We will show that there is a model of CM that is not a model of L CM . First observe that there is a natural number n that bounds the number of occurrences of (possibly equal) variables in terms appearing in the rules of CM . We can assume, without loss of generality, that n glyph[greaterorequalslant] 2. Then we consider the algebra A = 〈{ 0, 1, 2, . . . , n } ·〉 , equipped with a binary operation such that 1 · 2 : = 2 and 2 · 1 : = 1 and glyph[negationslash]

$$a \cdot b = b \cdot a \coloneqq \begin{cases} a & \text{ if } a \neq n \text{ and } b = 0 \\ 0 & \text{ if } a = n \text{ and } b = 0 \\ a & \text{ if } b = a - 1 \text{ and } a \geq 3 \\ a - 1 & \text{ if } b = a - 2 \text{ and } a \geq 3 \\ 1 & \text{ otherwise } \end{cases}$$

for every a b , ∈ A such that { a b , } glyph[negationslash] = { 1, 2 } .

glyph[negationslash]

We first show that 〈 A , { 0 }〉 is not a model of L CM . Observe that A / ∈ CM , since 1 · 2 = 2 · 1. By point 1 of Lemma 4 1 . we know that it will be enough to prove that 〈 A , { 0 }〉 is a reduced matrix. By point 1 of Lemma 2 1 . this amounts to checking whether for every different a b , ∈ A glyph[integerdivide] { 0 } there is a polynomial function p : A → A such that p a ( ) = 0 if and only if p b ( ) = 0. This is what we do now: consider a pair of different a b , ∈ A glyph[integerdivide] { 0 } . Assume, without loss of generality, that a &lt; b . Then we consider the polynomial function glyph[negationslash]

$$p ( x ) \coloneqq & ( \dots \left ( ( ( \dots ( ( \dots ( ( 1 \cdot 2 ) \cdot 3 ) \cdot \dots ) \cdot a ) \cdot \dots \\ & \dots \cdot ( b - 1 ) ) \cdot x \right ) \cdot ( b + 1 ) ) \cdot \dots \cdot n ) \cdot 0.$$

glyph[negationslash]

It is easy to see that p b ( ) = 0. Then we turn to show that p a ( ) = 0. We consider two cases, whether b -1 &lt; 3 or not. First consider the case in which b -1 &lt; 3. We have that either ( a = 1 and b = 2) or ( a = 1 and b = 3)

or ( a = 2 and b = 3). It is easy to prove that

$$\text{if } a & = 1 \text{ and } b = 2, \text{ then } p ( a ) = n - 1 \\ \text{if } a & = 1 \text{ and } b = 3, \text{ then } p ( a ) = 1 \\ \text{if } a & = 2 \text{ and } b = 3, \text{ then } p ( a ) = 1.$$

Then we turn to the case in which 3 glyph[lessorequalslant] b -1. We have that:

$$p ( a ) = ( \dots ( ( b - 1 \cdot a ) \cdot b + 1 ) \dots \cdot n ) \cdot 0 = \begin{cases} n - 1 & \text{if $a=b-2$} \\ 1 & \text{otherwise.} \end{cases}$$

glyph[negationslash]

Therefore we obtain that p a ( ) = 0. This concludes the proof that 〈 A , { 0 }〉 is not a model of L CM .

Now we turn to prove that 〈 A , { 0 }〉 is a model of CM . Consider a rule G glyph[turnstileleft] j in CM . Suppose that there is a homomorphism h : Fm → A such that h [ G ] ⊆ { } 0 . From point 3 of Lemma 4 1 . we know that there is g ∈ G such that CM glyph[satisfies] g ≈ j . In particular, we have that h ( g ) = 0. We claim that { h ( # ) , h ( d ) } glyph[negationslash] = { 1, 2 } for every subformula # · d of g . Suppose the contrary towards a contradiction. Then there is a subformula # · d of g such that { h ( # ) , h ( d ) } = { 1, 2 } . Since at most n (possibly equal) variables occur in g , and # · d contains at least two of them, we know that if we draw the subformulas tree of g there are at most n -2 nodes g 1 &lt; g 2 &lt; · · · &lt; g n -2 (with g n -2 = g ) strictly above # · d , where &lt; is the strict order of the subformulas tree. From the definition of · it follows that 1 glyph[lessorequalslant] h ( g m ) glyph[lessorequalslant] m + 2 for every m glyph[lessorequalslant] n -2. Therefore we obtain that 1 glyph[lessorequalslant] h ( g ) glyph[lessorequalslant] n , against the assumption that h ( g ) = 0. This concludes the proof of our claim.

Now, recall that CM glyph[satisfies] g ≈ j . It is possible to prove by induction on the length of the proofs of Birkhoff's equational logic that j is obtained from g in the following way. We replace a subformula g 1 · g 2 of g by g 2 · g 1 and denote by g ′ the formula obtained in this way. Then we repeat this process on g ′ . Iterating this construction a finite number of times we reach j . Now, observe that the operation · in A commutes always except for the case in which its arguments exhaust the set { 1, 2 } . This fact, together with our claim and the observation on equational logic, implies that h ( g ) = h ( j ) . In particular, this means that h ( j ) = 0. Hence 〈 A , { 0 }〉 is a model of the rules in CM . glyph[squaremultiply]

## End of digression

The digression shows that the quest for a finite Hilbert-style axiomatization of the logic L CR is not in principle a trivial one: such an axiomatization may even fail to exist, as in the case of commutative magmas of Example 4 2 . . Nevertheless we will provide an explicit and finite Hilbert calculus for the logic L CR (Theorem 4 6 . ).

Definition 4 3 . . Let CR be the following Hilbert calculus (and the logic it determines) in the language of commutative rings:

$$w + ( u \cdot ( ( x \cdot y ) \cdot z ) ) \dashv w + ( u \cdot ( x \cdot ( y \cdot z ) )$$

$$w + ( u \cdot ( x \cdot y ) ) \dashv w + ( u \cdot ( y \cdot x ) )$$

w

+(

u

·

(

x

·

1

))

glyph[turnstileright]

glyph[turnstileleft]

w

+(

u

·

x

)

(C)

$$w + \left ( u \cdot \left ( ( x + y ) + z \right ) \right ) \dashv \vdash w + \left ( u \cdot \left ( x + ( y + z ) \right ) \right )$$

$$w + ( u \cdot ( x + y ) ) \dashv w + ( u \cdot ( y + x ) )$$

$$w + ( u \cdot ( x + 0 ) ) \dashv w + ( u \cdot x )$$

$$w + ( u \cdot ( x + - x ) ) \dashv w + ( u \cdot 0 )$$

$$w + ( u \cdot ( x \cdot ( y + z ) ) ) \dashv w + ( u \cdot ( ( x \cdot y ) + ( x \cdot z ) ) )$$

$$w + ( u \cdot - ( x + y ) ) \dashv w + ( u \cdot ( - x + - y ) )$$

$$w + ( u \cdot - ( x \cdot y ) ) \dashv w + ( u \cdot ( - x \cdot y ) )$$

$$w + ( u \cdot - ( x \cdot y ) ) \dashv \vdash w + ( u \cdot ( x \cdot - y ) )$$

$$0 + x \dashv x$$

$$x + ( 1 \cdot y ) \dashv | x + y$$

The following technical result about the special nature of deductions of CR , will be useful in the subsequent proofs.

Lemma 4 4 . . Let G ∪ { j } ⊆ Fm. If G glyph[turnstileleft] CR j , then there is g ∈ G and a finite sequence of formulas 〈 a 1, a 2, . . . , a n 〉 such that a 1 = g , a n = j and for every m &lt; n there is a rule # glyph[turnstileright] glyph[turnstileleft] d of the calculus CR and a substitution s such that { s# sd , } = { a m , a m + 1 } .

Proof. The result follows from two observations. First, that the calculus CR consists of rules with only one premise. Second, that if a glyph[turnstileleft] b ∈ CR , then b glyph[turnstileleft] a ∈ CR too. glyph[squaremultiply]

Our main goal will be to prove that CR is in fact a finite axiomatization of L CR . To do this we will make use of the following lemma, whose easy proof (contained in the Appendix) involves some tedious calculations. The reader may safely choose to skip it in order keep track of the proof of the main result of the section.

Lemma 4 5 . . The logic CR is selfextensional.

Drawing consequences from the fact that CR is selfextensional, the following result is easy to obtain.

Theorem 4 6 . . The rules CR provide a finite axiomatization of L CR .

Proof. First observe that each of the rules in CR corresponds to an equation, which holds in CR . Together with point 3 of Lemma 4 1 . , this implies that

CR glyph[lessorequalslant] L CR . Now, applying (N) and (O), it is easy to prove that

$$w, applying ( N ) \, \text{and} \, ( O ), \, \text{it is easy to prove } \, \binom { 1 } { ( x \cdot y ) \cdot z \dashv \dashv c _ { \mathcal { R } } \, x \cdot ( y \cdot z ) } \\ x \cdot y \dashv \dashv c _ { \mathcal { R } } \, y \cdot x \\ x \cdot 1 \dashv \dashv c _ { \mathcal { R } } \, x \\ ( x + y ) + z \dashv \dashv c _ { \mathcal { R } } \, x + ( y + z ) \\ x + y \dashv \dashv c _ { \mathcal { R } } \, y + x \\ x + 0 \dashv \dashv c _ { \mathcal { R } } \, x \\ x + - x \dashv \dashv c _ { \mathcal { R } } \, 0 \\ x \cdot ( y + z ) \dashv \dashv c _ { \mathcal { R } } \, ( x \cdot y ) + ( x \cdot z ) \\ \text{featensional by Lemma} \, 4. 5, \, \text{we can apply Ler}$$

Since CR is selfextensional by Lemma 4 5 . , we can apply Lemma 3 5 . obtaining Alg CR ⊆ CR . On the other hand, from point 1 of Lemma 4 1 . and the fact that CR glyph[lessorequalslant] L CR , it follows that CR = Alg L CR ⊆ Alg CR . Therefore we conclude that Alg CR = CR . Since for every A ∈ CR and F ⊆ A the matrix 〈 A , F 〉 is a model of L CR , this implies that L CR glyph[lessorequalslant] CR . Thus we conclude that CR = L CR as desired. glyph[squaremultiply]

Now that we have built the machinery necessary to speak about commutative rings by means of the propositional logic L CR , we turn back to the classification of logics determined by finite Hilbert calculi in the Leibniz hierarchy. We begin by describing a general way of associating a logic with each Diophantine equation.

Definition 4 7 . . Let p z ( 1, . . . , zn ) ≈ 0 be a Diophantine equation and x and y two new different variables. Let L ( p ) be the logic, in the language of commutative rings expanded with a new binary operation symbol ↔ , determined by the following Hilbert calculus:

$$of commutative rings expanded with a new binary operation symbol \leftrightarrow, \\ \text{demand by the following Hilbert calculus} ; \\ \quad & \bigcirc \vdash x \leftrightarrow x & ( R ) \\ x \leftrightarrow y \vdash y \leftrightarrow x & ( S ) \\ x \leftrightarrow y, y \leftrightarrow z \vdash x \leftrightarrow z & ( T ) \\ x \leftrightarrow y \vdash - x \leftrightarrow - y & ( \text{Rep} 1 ) \\ x \leftrightarrow y, z \leftrightarrow u \vdash ( x + z ) \leftrightarrow ( y + u ) & ( \text{Rep} 2 ) \\ x \leftrightarrow y, z \leftrightarrow u \vdash ( x \cdot z ) \leftrightarrow ( y \cdot u ) & ( \text{Rep} 3 ) \\ x \leftrightarrow y, z \leftrightarrow u \vdash ( x \leftrightarrow z ) \leftrightarrow ( y \leftrightarrow u ) & ( \text{Rep} 4 ) \\ p ( z _ { 1 }, \dots, z _ { n } ) \leftrightarrow 0, x, x \leftrightarrow y \vdash y & ( \text{MP} ) \\ p ( z _ { 1 }, \dots, z _ { n } ) \leftrightarrow 0, x \dashv \dashv \leftrightarrow ( x \leftrightarrow x ), p ( z _ { 1 }, \dots, z _ { n } ) \leftrightarrow 0 & ( A _ { 3 } ^ { \prime } ) \\ p ( z _ { 1 }, \dots, z _ { n } ) \leftrightarrow 0, x, y \dashv \leftrightarrow y & ( G ^ { \prime } ) \\ \quad & \bigcirc \vdash \alpha \leftrightarrow \beta & ( \text{CR} ) \\ \text{for every $\alpha \dashv \beta \in \mathcal{CR}.}$$

for every a glyph[turnstileright] glyph[turnstileleft] b ∈ CR .

Observe that L ( p ) is determined by an explicit finite Hilbert calculus in a finite language. It turns out that there is a strong relation between the existence of an integer solution to p z ( 1, . . . , zn ) ≈ 0 and the location of L ( p ) in the Leibniz hierarchy.

Theorem 4 8 . . Let p ( z 1, . . . , zn ) ≈ 0 be a Diophantine equation. The following conditions are equivalent:

- (i) L ( p ) is finitely regularly algebraizable.
- (ii) Truth is implicitly definable in Mod ∗ L ( p . )
- (iii) L ( p ) is protoalgebraic.
- (iv) The equation p ( z 1, . . . , zn ) ≈ 0 has an integer solution.

Proof. Clearly (i) implies (ii) and (iii). Now we turn to prove (ii) ⇒ (iv). We reason by contraposition. Suppose that p z ( 1, . . . , zn ) ≈ 0 has no integer solution. Now choose two different integers s and m . Then let Z be the expansion of Z with a new binary function ↔ defined as follows:

$$a \leftrightarrow b \coloneqq \begin{cases} s & \text{if $a=b$} \\ m & \text{otherwise} \end{cases}$$

for every a b , ∈ Z . Pick k / ∈ { s , m } . It is easy to check that 〈 Z , { }〉 s and 〈 Z , { s , k }〉 are models of L ( p ) , since p z ( 1, . . . , zn ) ≈ 0 has no integer solution. Moreover they are reduced. In order to see this, pick two different a b , ∈ Z and consider the polynomial function q z ( ) : = a ↔ z . We have that q ( a ) = s and that q b ( ) = m / ∈ { s , k } . By point 1 of Lemma 2 1 . we conclude both that 〈 a b , 〉 ∈ / W Z { } s and that 〈 a b , 〉 ∈ / W Z { s , k } . But this means that there are two different reduced models of L ( p ) with the same algebraic reduct and, therefore, that truth is not implicitly definable in Mod ∗ L ( p ) .

Now we prove (iii) ⇒ (iv). Suppose that L ( p ) is protoalgebraic. Then there is a set of protoimplication formulas r ( x y , ) . In particular, we have that x , r ( x y , ) glyph[turnstileleft] L ( p ) y . Then there is a finite proof p of y from the premises in { x }∪ r ( x y , ) . Taking a closer look at the axiomatization of L ( p ) , it is easy to see that either an application of (MP') or of (A 3 ') must occur in p . This is because the other rules yield complex conclusions. In particular, this implies that there is a substitution s such that x , r ( x y , ) glyph[turnstileleft] L ( p ) s p z ( 1, . . . , zn ) ↔ s 0. From Theorem 3 1 . we know that ˘ glyph[turnstileleft] L ( p ) r ( x x , ) . In particular, this means that x glyph[turnstileleft] L ( p ) s s x p z ( 1, . . . , zn ) ↔ s s x 0, where s x is the substitution which sends all variables to x . But observe that every substitution leaves 0 fixed. Therefore we conclude that

$$x \vdash _ { \mathcal { L } ( p ) } \sigma _ { x } \sigma p ( z _ { 1 }, \dots, z _ { n } ) \leftrightarrow 0.$$

Now we consider the algebra Z built in the proof of part (ii) ⇒ (iv). It is easy to check that 〈 Z , { }〉 s is a model of L ( p ) . Therefore, pick an homomorphism h : Fm → Z that sends x to s . From ( ) it follows that 3

h ( s s x p z ( 1, . . . , zn ) ↔ 0 ) = s . But observe that h ( s s x p z ( 1, . . . , zn ) ↔ 0 ) = s ⇐⇒ h ( p ( s s x ( z 1 ) , . . . , s s x ( zn )) ↔ 0 ) = s ⇐⇒ p Z ( h s s x ( z 1 ) , . . . , h s s x ( zn )) ↔ h 0 = s ⇐⇒ p Z ( h s s x ( z 1 ) , . . . , h s s x ( zn )) = h 0 ⇐⇒ p Z ( h s s x ( z 1 ) , . . . , h s s x ( zn )) = 0.

Therefore we conclude that 〈 h s s x ( z 1 ) , . . . , h s s x ( zn ) 〉 is an integer solution to the equation p z ( 1, . . . , zn ) ≈ 0.

It only remains to prove (iv) ⇒ (i). Suppose that the equation p z ( 1, . . . , zn ) ≈ 0 admits an integer solution. Recall that the free commutative ring with free generators { z 1, . . . , zn } is the polynomial ring Z [ z 1, . . . , zn ] . Since Z is a subalgebra of Z [ z 1, . . . , zn ] , this implies that there are constant terms (in the language of commutative rings) a 1, . . . , a n such that Z [ z 1, . . . , zn ] glyph[satisfies] p ( a 1, . . . , a n ) ≈ 0 and, therefore, that CR glyph[satisfies] p ( a 1, . . . , a n ) ≈ 0. From point 3 of Lemma 4 1 . it follows that p ( a 1, . . . , a n ) glyph[turnstileright] glyph[turnstileleft] CR 0. By Theorem 4 6 . this is equivalent to the fact that p ( a 1, . . . , a n ) glyph[turnstileright] glyph[turnstileleft] CR 0. Therefore we can apply Lemma 4 4 . obtaining a finite sequence 〈 g 1, g 2, . . . , g m 〉 , where g 1 = p ( a 1, . . . , a n ) , g m = 0 and for every k &lt; m there is a rule a glyph[turnstileright] glyph[turnstileleft] b ∈ CR and a substitution s (in the language of commutative rings) such that { sa sb , } = { g k , g k + 1 } . Observe that s can be regarded as a substitution in the language of L ( p ) as well. Moreover, recall that a ↔ b is an axiom of L ( p ) by (CR). Therefore, by structurality, we obtain ˘ glyph[turnstileleft] L ( p ) sa ↔ sb . Applying (S) if necessary, this yields that ˘ glyph[turnstileleft] L ( p ) g k ↔ g k + 1 . Hence we proved that ˘ glyph[turnstileleft] L ( p ) g k ↔ g k + 1 for every k glyph[lessorequalslant] m -1. Applying m -1 times (T) we conclude that

$$\emptyset \vdash _ { \mathcal { L } ( p ) } p ( \alpha _ { 1 }, \dots, \alpha _ { n } ) \leftrightarrow 0.$$

Recall that the variables x and y do not appear in the equation p z ( 1, . . . , zn ) ≈ 0 therefore, we can safely consider the substitution s that sends zi to a i for every i glyph[lessorequalslant] n and leaves the other variables untouched. By (MP'), (A 3 '), (G') and ( 4 ) we obtain that

$$x, x \leftrightarrow y \vdash _ { \mathcal { L } ( p ) } y \ \ x \dashv \vdash _ { \mathcal { L } ( p ) } x \leftrightarrow ( x \leftrightarrow x ) \text{ and } x, y \vdash _ { \mathcal { L } ( p ) } x \leftrightarrow y.$$

Now it is easy to see that what we have proved is just the syntactic characterization of algebraizability of Theorem 3 2 . for t ( x ) : = { x ≈ x ↔ } x and r ( x y , ) : = { x ↔ } y . Therefore, with an application of Lemma 3 4 . , we conclude that L ( p ) is finitely regularly algebraizable. glyph[squaremultiply]

Corollary 4 9 . . The logic L ( p ) is consistent for every Diophantine equation p ≈ 0 .

Proof. It is easy to see that the matrix 〈 Z , { }〉 s defined in the above proof is a model of L ( p ) . Since { } glyph[negationslash] s = Z , we conclude that L ( p ) is consistent. glyph[squaremultiply]

Observe that every class of the Leibniz hierarchy is contained either into the class of protoalgebraic logic or into the one of logics L whose

truth sets are implicitly definable in Mod ∗ L . Moreover every class of the Leibniz hierarchy contains the one of finitely regularly algebraizable logics. Keeping this is mind, Theorem 4 8 . shows that the problem of determining whether a logic of the form L ( p ) belong to a given level of the Leibniz hierarchy is equivalent to the one of determining whether it belongs to any level of the Leibniz hierarchy. This does not contradicts the fact that in general these two problems are different. By means of this peculiar feature of logics of the form L ( p ) , we are able to establish at once the undecidability of the various problems (one for each level of the Leibniz hierarchy) of determining whether a logic belong to a given level of the Leibniz hierarchy.

Theorem 4 10 . . Let K be a level of the Leibniz hierarchy in Figure 1 . The problem of determining whether the logic of a given consistent finite Hilbert calculus in a finite language belongs to K is undecidable.

Proof. Suppose towards a contradiction that there is an algorithm A 1 that, given a consistent finite Hilbert calculus in a finite language, determines whether its logic belongs to K . Then we define a new algorithm A 2 as follows: given a Diophantine equation p ≈ 0, we construct the logic L ( p ) and check with A 1 whether it belongs to K . Observe that we can do this, since L ( p ) is consistent by Corollary 4 9 . . Then in the positive case A 2 returns yes , while no otherwise. Observe that K contains the class of finitely regularly algebraizable logics and is included either in the class of protoalgebraic logics or in the class of logics L whose truth sets are implicitly definable in Mod ∗ L . Therefore we can apply Theorem 4 8 . , yielding that:

L ( p ) ∈ K ⇐⇒ p ≈ 0 has an integer solution.

Therefore A 2 would provide a decision procedure for Hilbert's tenth problem. Since we know that such a procedure does not exist, we obtain a contradiction as desired. glyph[squaremultiply]

## 5 . T he classification problem in the F rege hierarchy

Now we move our attention to the problem of classifying logics in the Frege hierarchy, which deals with several kinds of replacement properties. Our goal is to prove a result analogous to the one obtained for the Leibniz hierarchy. More precisely, we will show that the problem of classifying the logic of a consistent finite Hilbert calculus in a finite language in the Frege hierarchy is in general undecidable (Theorem 5 2 . ). Remarkably, our argument shows that this classification problem remains undecidable even if we restrict our attention to Hilbert calculi that determine a finitary algebraizable logic. Our strategy is as follows. Consider a finitely based variety

V of finite type, whose equational theory in one variable is undecidable. 2 We will reduce the problem of determining the equational theory of V in a single variable to the problem of classifying logics of finite consistent Hilbert calculi in the Frege hierarchy.

Let F be a finite equational basis for the variety V , and let Eq x ( ) be the set of all equations in the language of V in a single variable x . We will introduce a new logic L ( a b , ) for each equation a ≈ b ∈ Eq x ( ) .

Definition 5 1 . . Let a ≈ b ∈ Eq x ( ) and let L be the language of V , expanded with two new connectives glyph[square] and → , respectively unary and binary. Then L ( a b , ) is the logic in the language L axiomatized by the following Hilbert calculus:

$$\emptyset \vdash x \rightarrow x$$

x x

,

→

y

glyph[turnstileleft]

y

(MP)

$$\{ x _ { i } \to y _ { i }, y _ { i } \to x _ { i } \, \colon 1 \leqslant i \leqslant n \} \vdash f ( x _ { 1 }, \dots, x _ { n } ) \to f ( y _ { 1 }, \dots, y _ { n } ) \quad ( \text{Rep} )$$

$$x \dashv \vdash \Box x \to x, x \to \Box x$$

$$\emptyset \vdash \varepsilon \rightarrow \delta, \delta \rightarrow \varepsilon$$

$$\alpha ( \varphi ) \rightarrow \beta ( \varphi ) \vdash \varphi$$

for every # ≈ d ∈ F , every n -ary connective f , and every formula j of the following list:

$$\text{following list} \\ \varphi _ { 1 } \coloneqq & x \to ( y \to x ) \\ \varphi _ { 2 } \coloneqq & ( x \to ( y \to z ) ) \to ( ( x \to y ) \to ( x \to z ) ) \\ \varphi _ { 3 } \coloneqq & ( x _ { 1 } \to y _ { 1 } ) \to ( ( y _ { 1 } \to x _ { 1 } ) \to ( \cdots \to ( ( x _ { n } \to y _ { n } ) \to \\ & \to ( ( y _ { n } \to x _ { n } ) \to ( f ( \vec { x } ) \to f ( \vec { y } ) ) ) \cdots ) ) \\ \varphi _ { 4 } \coloneqq & x \to ( x \to \Box x ) \\ \varphi _ { 5 } \coloneqq & x \to ( \Box x \to x ) \\ \varphi _ { 6 } \coloneqq & ( \Box x \to x ) \to ( ( x \to \Box x ) \to x ) \\ \text{again with $f$ ranging over all $n$-ary for every $n\in\omega$.}$$

again with f ranging over all n -ary for every n ∈ w .

Observe that the syntactic characterization of algebraizability (Theorem 3 2 . ) implies that L ( a b , ) is finitely algebraizable through

$$\tau ( x ) = \{ x \approx \Box x \} \text{ and } \rho ( x, y ) = \{ x \rightarrow y, y \rightarrow x \}.$$

The next result expresses the relation between the validity of the equation a ≈ b in V and the location of the logic L ( a b , ) in the Frege hierarchy.

Theorem 5 2 . . Let a ≈ b ∈ Eq x . The following conditions are equivalent: ( ) (i) L ( a b , ) is fully Fregean.

2 Observe that examples of finitely based varieties of finite type, whose equational theory in one variable is undecidable, are known. For instance, the variety of relation algebras is of this kind, as shown in [ 26 , Section 8 5 . (viii)]. Other examples are described in [ 18 ].

- (ii) L ( a b , ) is selfextensional.
- (iii) V glyph[satisfies] a ≈ b .

Proof. (i) ⇒ (ii) is straightforward. Then we turn to prove (ii) ⇒ (iii). Suppose towards a contradiction that L ( a b , ) is selfextensional and that V glyph[notsatisfies] a ≈ b . Then let A ∈ V be the free algebra with countably many free generators. It is well known that the universe of A consists of congruence classes of terms, that we denote by J j K , J y K . . . In particular, we denote the free generators of A by { J z K : z ∈ Var } . In particular, consider the three distinct elements J x K , J y K and J v K of A corresponding to the three distinct variables x y , and v . Then expand A with two new unary and binary operations glyph[square] and → defined as glyph[negationslash]

glyph[negationslash]

for every a b , ∈ A . Let B be the result of the expansion and put F : = B glyph[integerdivide] { J x K } .

$$\Box a \coloneqq \begin{cases} \begin{array} { c c } [ y ] & \text{if $a=\left[x\right]$} \\ a & \text{otherwise} \end{array} \quad a \to b \coloneqq \begin{cases} \begin{array} { c } \left [ x \right ] & \text{if $a\neq b$} \\ \left [ y \right ] & \text{if $a=b\neq \left[x\right]$} \\ \left [ v \right ] & \text{if $a=b=\left[x\right]$} \end{cases} \\ \text{for every $a,b\in A$.\, Let $B$ be the result of the expansion and put $F\coloneqq$} \end{cases}$$

$$\text{Claim } 5. 2. 1. \, \langle B, F \rangle \in \text{Mod} ^ { * } \mathcal { L } ( \alpha, \beta ).$$

First observe that 〈 B , F 〉 is a reduced matrix. To prove this, consider two different elements a b , ∈ B and the polynomial function p x ( ) : = x → a . It is easy to see that p a ( ) ∈ F and p b ( ) / ∈ F . By point 1 of Lemma 2 1 . we conclude that 〈 a b , 〉 ∈ / W B F and, therefore, that 〈 B , F 〉 is reduced. Then we turn to prove that it is a model of L ( a b , ) . The closure of F under the rules axiomatizing L ( a b , ) is easily proved, except perhaps for the set of rules (W). Consider a rule a j ( ) → b j ( ) glyph[turnstileleft] j in (W) and a homomorphism h : Fm → B such that h a j ( ) → h b j ( ) ∈ F . Clearly we have that h a j ( ) = h b j ( ) . Since V glyph[notsatisfies] a ≈ b and A is the free relation algebra, we know that h ( j ) / ∈ { J z K : z ∈ Var } . Together with the definition of F , this implies that h ( j ) ∈ F .

Now observe that both x → x and y → y are instances of (R) and, therefore, they are theorems of L ( a b , ) . In particular this means that x → x glyph[turnstileright] glyph[turnstileleft] L ( a b , ) y → y . Since L ( a b , ) is selfextensional, we obtain that Alg L ( a b , ) glyph[satisfies] x → x ≈ y → y by Lemma 3 5 . . Let g : Fm → B the the natural surjection, which sends z to J z K for every z ∈ Var . It is easy to see that glyph[negationslash]

But from Claim 5 2 1 . . it follows that B ∈ Alg L . Therefore we reach a contradiction as desired.

$$g ( x \to x ) = \left [ v \right ] & \neq \left [ y \right ] = g ( y \to y ). \\ \lim \, \Xi \, \frac { 1 } { 2 } \, \text{ if follow that } R \, \subset \, \Delta \ell \alpha \, \ell \quad \text{Therefore for}$$

It only remains to prove part (iii) ⇒ (i). Suppose that V glyph[satisfies] a ≈ b . Recall that L ( a b , ) is algebraizable with set of congruence formulas r ( x y , ) = { x → y y , → } x . By Lemma 3 3 . we have that

$$\emptyset \vdash _ { \mathcal { L } ( \alpha, \beta ) } \rho ( \gamma, \eta ) \Longleftrightarrow \text{Alg} \mathcal { L } ( \alpha, \beta ) \vdash \gamma \approx \eta$$

for every g h , ∈ Fm . Applying this observation to the axiom (V), we conclude that Alg L ( a b , ) is a class of expansions of algebras in V . Together with the fact that V glyph[satisfies] a ≈ b , this implies that a → b is a theorem of L ( a b , ) . Then consider any i glyph[lessorequalslant] 7. By structurality a j ( i ) → b j ( i ) is a theorem of L ( a b , ) . Therefore we can apply the rules (W), obtaining that also j i is a theorem of L ( a b , ) .

Now, let L be the logic axiomatized only by { j i : i glyph[lessorequalslant] 6 } , (V) and (MP).

$$\text{Claim } 5. 2. 2. \ \mathcal { L } = \mathcal { L } ( \alpha, \beta ).$$

Clearly we have that L glyph[lessorequalslant] L ( a b , ) . To show the other direction, observe that L satisfies the rules (W). Moreover, with an application of (MP) and j 3, j 4, j 5, j 6, it is easy to see that L satisfies (Rep) and (A 3 ) too. It only remains to show that L satisfies (R). But observe that L is an expansion of the implication fragment IPC→ of propositional intuitionistic logic, which is axiomatized by j 1, j 2 and (MP) [ 14 , Example 5 91 . ]. Since x → x is a theorem of IPC→ , we conclude that L satisfies (R) and, therefore, that L ( a b , ) glyph[lessorequalslant] L . Thus we established the claim.

It is well known that a finitary logic in a language containing → satisfies the classical version of the deduction-detachment theorem if and only if it is an axiomatic extension of the logic defined in its language by the axioms j 1 and j 2 and the rule (MP) [ 27 , Theorem 2 4 2 . . ]. Together with Claim 5 2 2 . . , this implies that

$$\Gamma \vdash _ { \mathcal { L } ( \alpha, \beta ) } \gamma \to \psi \Longleftrightarrow \Gamma, \gamma \vdash _ { \mathcal { L } ( \alpha, \beta ) } \psi$$

for every G ∪{ g y , } ⊆ Fm . In particular, this means that for every g y , ∈ Fm :

$$\gamma \dashv _ { \mathcal { L } ( \alpha, \beta ) } \psi \Longleftrightarrow \emptyset \vdash _ { \mathcal { L } ( \alpha, \beta ) } \rho ( \gamma, \psi ) \Longleftrightarrow A \mathbf l g \mathcal { L } \mathbb { = } \gamma \approx \psi.$$

This fact easily implies that glyph[turnstileright] glyph[turnstileleft] L ( a b , ) is a congruence of Fm . Hence we conclude that L ( a b , ) is selfextensional. The fact that L ( a b , ) is also fully Fregean, is a consequence of two general results of abstract algebraic logic. First, every finitary selfextensional logic with a classical deductiondetachment theorem is fully selfextensional [ 15 , Theorem 4 46 . ] (see also [ 23 ]). 3 Second, every truth-equational fully selfextensional logic is also fully Fregean [ 1 , Theorem 22 ]. glyph[squaremultiply]

We are now ready to state the main result on the classification of syntactically presented logics in the Frege hierarchy.

Theorem 5 3 . . Let K be a level of the Frege hierarchy. The problem of determining whether the logic of a given finite consistent Hilbert calculus in a finite language belongs to K is undecidable. Moreover, the problem remains undecidable when

3 In these references the classical deduction-detachment theorem is called uniterm deduction-detachment theorem. The expression uniterm refers to the fact that this deductiondetachment theorem is witnessed by a single formula in two variables in contrast to the cases where the deduction-detachment theorem is witnesses by a set of formulas as in [ 8 , 13 ].

restricted to the classification of finite consistent Hilbert calculi that determine a finitely algebraizable logic.

Proof. Observe that the logic L ( a b , ) was defined starting from an arbitrary variety V of finite type, which is finitely based and whose equational theory in one variable is undecidable. We can assume w.l.o.g. that V is the variety RA of relation algebras. Under this assumption, we claim that the logic L ( a b , ) is consistent for every a ≈ b ∈ Eq x ( ) . The fact that L ( a b , ) is consistent when RA glyph[notsatisfies] a ≈ b has been proved in part (ii) ⇒ (iii) of Theorem 5 2 . . Then consider the case where RA glyph[satisfies] a ≈ b . In part (iii) ⇒ (i) of Theorem 5 2 . , we showed that L ( a b , ) is the logic axiomatized by only by { j i : i glyph[lessorequalslant] 6 } , (V) and (MP). Then consider any non-trivial Boolean algebra A = 〈 A , ∧ ∨ ¬〉 , , and expand it to a relation algebra 〈 A , ∧ ∨ ¬ · , , , , glyph[smile] , 1 〉 by interpreting · as ∧ , glyph[smile] as the identity map, and 1 as the top element. Moreover, let → be the usual Boolean implication and glyph[square] be the constant function with value 1. Let B be the result of the expansion. It is very easy to see that 〈 B , { 1 }〉 is a model of { j i : i glyph[lessorequalslant] 6 } , (V) and (MP). Hence L ( a b , ) is consistent. This establishes our claim.

Now, we turn back to the main proof, again assuming that V = RA . Let K be a level of the Frege hierarchy. Suppose towards a contradiction that there is an algorithm A 1 which, given a finite consistent Hilbert calculus in a finite language that moreover determines a finitely algebraizable logic, decides whether its logic belongs to K . Then we define a new algorithm A 2 as follows: given an equation a ≈ b ∈ Eq x ( ) , we construct the logic L ( a b , ) and check with A 1 if it belongs to K . In the positive case A 2 returns yes , while no otherwise. Observe that we can do this, since L ( a b , ) is finitely algebraizable and, by the claim, consistent. Since K contains the class of selfextensional logics and is included in the of class of fully Fregean ones, we can apply Theorem 5 2 . obtaining that

$$\mathcal { L } ( \alpha, \beta ) \in K \Longleftrightarrow \text{RA} \models \alpha \approx \beta.$$

Therefore A 2 would provide a decision procedure for the validity in RA of equations in one variable. But this contradicts the known fact that such a procedure does not exist [ 26 , Section 8 5 . (viii)]. glyph[squaremultiply]

## A ppendix

Proof of Lemma 4 5 . . First we check that glyph[turnstileright] glyph[turnstileleft] CR preserves the connective -. To do this, consider y j , ∈ Fm such that y glyph[turnstileright] glyph[turnstileleft] CR j : we have to prove that -y glyph[turnstileright] glyph[turnstileleft] CR j . By Lemma 4 4 . it will be enough to check that -a glyph[turnstileright] glyph[turnstileleft] CR b for every a glyph[turnstileright] glyph[turnstileleft] b ∈ CR . We shall make use of some deductions. In particular, by suitable substitutions and applying (N) and (O) to (B), (D),

(E), (H), (I), (L) and (M), we obtain that

$$x \cdot y \stackrel { \vdash } { \longmapsto } _ { \mathcal { C R } } y \cdot x$$

$$( x + y ) + z \dashv \vdash _ { \mathcal { C R } } x + ( y + z )$$

$$x + y \dashv \vdash _ { c \mathcal { R } } y + x$$

$$x \cdot ( y + z ) \dashv \vdash _ { \mathcal { C R } } ( x \cdot y ) + ( x \cdot z )$$

$$- ( x + y ) \stackrel { \_ } { \longmapsto } _ { \mathcal { C R } } - x + - y$$

$$w + - ( x \cdot y ) \dashv \vdash _ { \mathcal { C R } } w + ( - x \cdot y )$$

$$w + - ( x \cdot y ) \dashv \vdash _ { \mathcal { C R } } w + ( x \cdot - y )$$

Then suppose that we are given a rule of our calculus (X), different from (N) and (O). Then (X) is of the form w +( u · # ) glyph[turnstileright] glyph[turnstileleft] w +( u · d ) for some formulas # and d . But we have that

$$- ( w + ( u \cdot \varepsilon ) ) \dashv \vdash _ { \mathcal { C R } } - w + - ( u \cdot \varepsilon )$$

$$\neg \vdash _ { \mathcal { C R } } - w + ( - u \cdot \varepsilon )$$

$$\neg \vdash _ { \mathcal { C R } } - w + ( - u \cdot \delta )$$

$$\neg \vdash _ { \mathcal { C R } } - w + - ( u \cdot \delta )$$

$$\neg \vdash _ { \mathcal { C R } } - ( w + ( u \cdot \delta ) )$$

Therefore it only remains to prove the cases of (N) and (O). This is what we do now:

$$- ( 0 + x ) \stackrel { \_ } { \longrightarrow } \vdash _ { \mathcal { C R } } 0 + - ( 0 + x )$$

$$\neg \vdash _ { C \mathcal { R } } 0 + ( 1 \cdot - ( 0 + x ) )$$

$$\neg \vdash _ { C \mathcal { R } } 0 + - ( 1 \cdot ( 0 + x ) )$$

$$\neg \vdash _ { C \mathcal { R } } 0 + ( - 1 \cdot ( 0 + x ) )$$

$$\neg \vdash _ { \mathcal { C R } } 0 + ( - 1 \cdot ( x + 0 ) )$$

$$\neg \vdash _ { C \mathcal { R } } 0 + ( - 1 \cdot x )$$

$$\neg \vdash _ { C \mathcal { R } } 0 + - ( 1 \cdot x )$$

$$\neg \vdash _ { \mathcal { C R } } 0 + ( 1 \cdot - x )$$

$$\neg \vdash _ { C \mathcal { R } } 0 + - x$$

$$\neg \vdash _ { c \mathcal { R } } - x$$

$$- ( x + ( 1 \cdot y ) ) \dashv \vdash _ { \mathcal { C R } } - x + - ( 1 \cdot y )$$

$$\neg \vdash _ { \mathcal { C R } } - x + ( 1 \cdot - y )$$

$$\Phi _ { \Phi } \Phi _ { \mathcal { C R } } - x + - y$$

$$\neg \vdash _ { \mathcal { C R } } - ( x + y )$$

Therefore we conclude that glyph[turnstileright] glyph[turnstileleft] CR preserves -.

and

Then we turn to prove that glyph[turnstileright] glyph[turnstileleft] CR preserves + and · too. In order to do this, it will be enough to show that if y glyph[turnstileright] glyph[turnstileleft] CR j , then c + y glyph[turnstileright] glyph[turnstileleft] CR c + j and c · y glyph[turnstileright] glyph[turnstileleft] CR c · j for every formula c . Let us explain briefly why. Suppose that this condition, call it (Y), holds. Then consider y 1, y 2, j 1, j 2 ∈ Fm such that y 1 glyph[turnstileright] glyph[turnstileleft] CR j 1 and y 2 glyph[turnstileright] glyph[turnstileleft] CR j 2. We would have that

$$\psi _ { 1 } + \psi _ { 2 } \stackrel { \_ } { \longleftarrow } _ { \mathcal { C R } } \psi _ { 1 } + \varphi _ { 2 }$$

$$\neg \vdash _ { \mathcal { C R } } \varphi _ { 2 } + \psi _ { 1 }$$

$$\neg \vdash _ { \mathcal { C R } } \varphi _ { 2 } + \varphi _ { 1 }$$

$$\neg \vdash _ { \mathcal { C R } } \varphi _ { 1 } + \varphi _ { 2 }$$

$$\psi _ { 1 } \cdot \psi _ { 2 } \stackrel { \_ } { \longmapsto } \vdash _ { \mathcal { C R } } \psi _ { 1 } \cdot \varphi _ { 2 }$$

$$\neg \vdash _ { \mathcal { C R } } \varphi _ { 2 } \cdot \psi _ { 1 }$$

$$\neg \vdash _ { \mathcal { C R } } \varphi _ { 2 } \cdot \varphi _ { 1 }$$

$$\neg \vdash _ { \mathcal { C R } } \varphi _ { 1 } \cdot \varphi _ { 2 }$$

concluding the proof. Therefore we turn to prove that if y glyph[turnstileright] glyph[turnstileleft] CR j , then c + y glyph[turnstileright] glyph[turnstileleft] CR c + j and c · y glyph[turnstileright] glyph[turnstileleft] CR c · j for every formula c . Suppose that y glyph[turnstileright] glyph[turnstileleft] CR j and consider an arbitrary formula c . By Lemma 4 4 . , to prove that c + y glyph[turnstileright] glyph[turnstileleft] CR c + j and c · y glyph[turnstileright] glyph[turnstileleft] CR c · j , it will be enough to check that c + a glyph[turnstileright] glyph[turnstileleft] CR c + b and c · a glyph[turnstileright] glyph[turnstileleft] CR c · b for every rule a glyph[turnstileright] glyph[turnstileleft] b in CR . Then suppose that we are given a rule (X) of CR , different from (N) and (O). Then (X) is of the form w +( u · # ) glyph[turnstileright] glyph[turnstileleft] w +( u · d ) for some formulas # and d . We have that

$$\chi + ( w + ( u \cdot \varepsilon ) ) \dashv \vdash _ { \mathcal { C R } } ( \chi + w ) + ( u \cdot \varepsilon )$$

$$\neg \vdash _ { \mathcal { C R } } ( \chi + w ) + ( u \cdot \delta )$$

$$\neg \vdash \mathcal { C R } \ \chi + ( w + ( u \cdot \delta ) )$$

and

and and

and

$$\chi \cdot \left ( w + ( u \cdot \varepsilon ) \right ) \dashv _ { \mathcal { C R } } \left ( \chi \cdot w \right ) + \left ( \chi \cdot ( u \cdot \varepsilon ) \right )$$

$$\neg \vdash _ { \mathcal { C R } } ( \chi \cdot w ) + ( 1 \cdot ( \chi \cdot ( u \cdot \varepsilon ) ) )$$

$$\neg \vdash _ { \mathcal { C R } } ( \chi \cdot w ) + ( 1 \cdot ( ( \chi \cdot u ) \cdot \varepsilon ) ) \quad \quad ( A )$$

$$\neg \vdash _ { \mathcal { C R } } ( \chi \cdot w ) + ( ( \chi \cdot u ) \cdot \varepsilon )$$

$$\neg \vdash _ { \mathcal { C R } } ( \chi \cdot w ) + ( ( \chi \cdot u ) \cdot \delta )$$

$$\neg \vdash _ { \mathcal { C R } } ( \chi \cdot w ) + ( 1 \cdot ( ( \chi \cdot u ) \cdot \delta ) )$$

$$\neg \vdash _ { \mathcal { C R } } ( \chi \cdot w ) + ( 1 \cdot ( \chi \cdot ( u \cdot \delta ) ) ) \quad \quad ( A )$$

$$\neg \vdash _ { \mathcal { C R } } ( \chi \cdot w ) + ( \chi \cdot ( u \cdot \delta ) )$$

$$\neg \vdash _ { \mathcal { C R } } \chi \cdot ( w + ( u \cdot \delta ) )$$

Therefore it only remains to check cases (N) and (O). For what concerns (N) we have that:

$$\chi + ( 0 + x ) \dashv { \vdash } _ { \mathcal { C R } } \left ( 0 + x \right ) + \chi$$

$$\neg \vdash _ { \mathcal { C R } } 0 + ( x + \chi )$$

$$\neg \vdash _ { \mathcal { C R } } x + \chi$$

$$\neg \vdash \mathcal { C R } \, \chi + x$$

$$\chi \cdot ( 0 + x ) \stackrel { \neg } { \vdash } _ { \mathcal { C R } } 0 + ( \chi \cdot ( 0 + x ) )$$

$$\neg \vdash _ { c \mathcal { R } } 0 + ( \chi \cdot ( x + 0 ) )$$

$$\neg \vdash _ { c \mathcal { R } } 0 + ( \chi \cdot x )$$

$$\neg \vdash _ { c \mathcal { R } } \chi \cdot x$$

Then we turn to prove the case of (O). We have that

$$\chi + ( x + ( 1 \cdot y ) ) \stackrel { \neg \vdash } { \neg \vdash } _ { \mathcal { C R } } ( \chi + x ) + ( 1 \cdot y )$$

$$\neg \vdash _ { \mathcal { C R } } ( \chi + x ) + y$$

$$\neg \vdash _ { \mathcal { C R } } \chi + ( x + y )$$

$$\chi \cdot \left ( x + \left ( 1 \cdot y \right ) \right ) \dashv { \vdash } c _ { \mathcal { R } } \left ( \chi \cdot x \right ) + \left ( \chi \cdot \left ( 1 \cdot y \right ) \right )$$

$$\neg \vdash _ { c \mathcal { R } } ( \chi \cdot x ) + ( \chi \cdot ( y \cdot 1 ) )$$

$$\neg \vdash _ { c \mathcal { R } } ( \chi \cdot x ) + ( \chi \cdot y )$$

$$\neg \vdash _ { \mathcal { C R } } \chi \cdot ( x + y )$$

This concludes the proof that CR is selfextensional.

glyph[squaremultiply]

Acknowledgements. The idea of considering the problem of classifying logics in the Leibniz and Frege hierarchies from a computational point of view originates from a list of open problems in abstract algebraic logic presented by F´ elix Bou in the Seminar on Non-Classical Logics of the University of Barcelona. I am very grateful to him for bringing my attention of this topic. Thanks are due also to Professors Josep Maria Font, Jos´ e Gil-F´ erez, Ramon Jansana and James Raftery for their useful comments on early versions of the paper, which contributed to improve a lot its presentation, and to Eduardo Hermo for discussing its topic when the work was at a preliminary stage. Finally, I wish to thank the anonymous referee, whose comments and suggestions improved further the presentation of the paper. The author was supported by the project GA 13 14654 -S of the Czech Science Foundation.

## 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 , Outstanding Contributions. Springer-Verlag., To appear.
- [ 2 ] S. V. Babyonyshev. Fully Fregean logics. Reports on Mathematical Logic , 37 59 : -77 , 2003 .
- [ 3 ] J. L. Bell and M. Machover. A Course in Mathematical Logic . North-Holland, Amsterdam, 1977 .
- [ 4 ] G. Bezhanishvili, T. Moraschini, and J. G. Raftery. Epimorphism surjectivity in varieties of residuated structures. To appear in the Jounal of Algebra , 2017 .
- [ 5 ] W. J. Blok and E. Hoogland. The Beth property in Algebraic Logic. Studia Logica , 83 1 ( -3 ): 49 -90 , 2006 .
- [ 6 ] W. J. Blok and D. Pigozzi. Protoalgebraic logics. Studia Logica , 45 337 : -369 , 1986 .
- [ 7 ] W. J. Blok and D. Pigozzi. Algebraizable logics , volume 396 of Mem. Amer. Math. Soc. A.M.S., Providence, January 1989 .
- [ 8 ] W. J. Blok and D. Pigozzi. Abstract algebraic logic and the deduction theorem. Available in internet http: // orion. math. iastate. edu/ dpigozzi/ , 1997 . Manuscript.
- [ 9 ] S. Burris and H. P. Sankappanavar. A course in Universal Algebra . Available in internet https://www.math.uwaterloo.ca/ ~ snburris/htdocs/ualg.html , the millennium edition, 2012 .
- [ 10 ] A. Chagrov and M. Zakharyaschev. Modal Logic , volume 35 of Oxford Logic Guides . Oxford University Press, 1997 .
- [ 11 ] J. Czelakowski. Protoalgebraic logics , volume 10 of Trends in Logic-Studia Logica Library . Kluwer Academic Publishers, Dordrecht, 2001 .
- [ 12 ] J. Czelakowski and D. Pigozzi. Amalgamation and interpolation in abstract algebraic logic. In X. Caicedo and Carlos H. Montenegro, editors, Models, algebras and proofs , number 203 in Lecture Notes in Pure and Applied Mathematics Series, pages 187 265 -. Marcel Dekker, New York and Basel, 1999 .
- [ 13 ] J. Czelakowski and D. Pigozzi. Fregean logics with the multiterm deduction theorem and their algebraization. Studia Logica , 78 1 2 ( -): 171 212 -, 2004 .
- [ 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., 2009 . First edition 1996 . Electronic version freely available through Project Euclid at https://www.projecteuclid.org/euclid.lnl/ 1235416965 .

## TOMMASO MORASCHINI

- [ 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 ] J. M. Font and T. Moraschini. Logics of varieties, logics of semilattices, and conjunction. Logic Journal of the IGPL , 22 818 : -843 , 2014 .
- [ 18 ] A. I. Maltsev Identical relations on varieties of quasigroups. Mat. Sbornik , 69 3 : -12 , 1966 .
- [ 19 ] J. M. Font and T. Moraschini. A note on congruences of semilattices with sectionally finite height. Algebra Universalis , 72 3 ( ): 287 293 -, 2014 .
- [ 20 ] J. M. Font and T. Moraschini. On the logics associated with a given variety of algebras. In A. Indrzejczak, J. Kaczmarek, and M. Zawidzki, editors, Trends in Logic XIII: Gentzen's and Ja´ skowski's heritage. 80 years of natural deduction and sequent calculi , pages 67 80 -, Ł´ od´, z 2014 . Wydawnictwo Uniwersytetu Ł´ odzkiego.
- [ 21 ] D. M. Gabbay and L. Maksimova. Interpolation and definability , volume 46 of Oxford Logic Guides . The Clarendon Press Oxford University Press, Oxford, 2005 . Modal and intuitionistic logics.
- [ 22 ] E. Hoogland. Algebraic characterizations of various Beth definability properties. Studia Logica, Special Issue on Abstract Algebraic Logic , 65 91 : -112 , 2000 .
- [ 23 ] R. Jansana. Selfextensional logics with implication. In J.-Y. Beziau, editor, Logica universalis , pages 65 -88 . Birkh¨ auser, Basel, 2005 .
- [ 24 ] L. L. Maksimova. Craig's theorem in superintuitionistic logics and amalgamable varieties of pseudo-Boolean algebras. Algebra i Logika , 16 643 : -681 , 1977 .
- [ 25 ] Y. Matiyasevich. Hilbert's 10 th Problem . MIT Press, 1993 .
- [ 26 ] A. Tarski and S. Givant. A formalization of set theory without variables , volume 41 of American Mathematical Society Colloquium Publications . American Mathematical Society, Providence, RI, 1987 .
- [ 27 ] R. W´ ojcicki. Theory of logical calculi. Basic theory of consequence operations , volume 199 of Synthese Library . Reidel, Dordrecht, 1988 .
- E-mail address : tommaso.moraschini@gmail.com
T. Moraschini
A computational glimpse at the Leibniz and Frege hierarchies
In this paper we consider, from a computational point of view, the problem of
classifying logics within the Leibniz and Frege hierarchies typical of abstract
algebraic logic. The main result states that, for logics presented
syntactically, this problem is in general undecidable. More precisely, we show
that there is no algorithm that classifies the logic of a finite consistent
Hilbert calculus in the Leibniz and in the Frege hierarchies.