A computational glimpse at the Leibniz and Frege hierarchies

T. Moraschini

A computational glimpse at the Leibniz and Frege hierarchies

T0 review · 0 major / 8 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Classifying the logic of a finite consistent Hilbert calculus inside the Leibniz or Frege hierarchy is undecidable.

desk verdict Two genuinely new undecidability results for the Leibniz and Frege hierarchy classification problems, built on honest reductions; the fragile-looking selfextensionality lemma checks out on close reading. read the letter →

arxiv 1908.00922 v1 pith:FCPDMI4E submitted 2019-08-01 math.LO

T. Moraschini This is my paper · ORCID

classification math.LO

keywords fregehierarchiesleibnizcomputationallogiclogicsproblemabstract

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Logics are often classified by how they relate to algebraic models. The Leibniz hierarchy sorts logics according to how their logical equivalence and truth notions connect to algebras; the Frege hierarchy sorts them according to replacement rules. A recurring question is whether, given a finite set of inference rules, one can algorithmically determine which level its logic occupies. This paper answers no for both hierarchies.

The author proves this by connecting the classification problem to known undecidable problems. For the Leibniz hierarchy, he defines for each Diophantine equation a finite Hilbert calculus whose logic belongs to a non-minimal level exactly when the equation has an integer solution. Since deciding whether a Diophantine equation has an integer solution is impossible, the classification problem cannot be decidable either. A central technical achievement is a finite axiom system for the logic associated with commutative rings.

For the Frege hierarchy, the argument uses the undecidability of the equational theory of relation algebras in one variable. The paper builds logics whose selfextensionality or Fregean property matches validity in that theory, transferring undecidability again. The results do not say every logic is hard to classify; they say no single general algorithm exists for all finite consistent Hilbert calculi, even in finite languages.

Extended reading notes

Core claim

The paper's central assertion is Theorems 4.10 and 5.3: for any level K of the Leibniz hierarchy (resp. Frege hierarchy), the problem of determining whether the logic of a given consistent finite Hilbert calculus in a finite language belongs to K is undecidable. In the Frege case, this remains undecidable when restricted to finite consistent Hilbert calculi that determine a finitely algebraizable logic. If the paper is correct, no general algorithm can classify syntactically presented logics in these hierarchies.

Load-bearing premise

The most fragile load-bearing premise is Lemma 4.5, that the Hilbert calculus CR (Definition 4.3) is selfextensional. Its proof, placed in the appendix, is a long sequence of term-derivation checks that the author describes as tedious. Lemma 4.5 is used to prove Theorem 4.6, the finite axiomatization of the ring logic L_CR, which underpins the positive direction (iv) implies (i) of Theorem 4.8 in the Leibniz hierarchy reduction. If this lemma failed, the equivalence between hierarchy membership and solvability of Diophantine equations could break, and with it Theorem 4.10. The paper's own text flags that readers may skip the calculation, which makes this the point a verifier should check first.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The paper delivers what it promises: it shows that classifying the logic of a finite consistent Hilbert calculus inside the Leibniz hierarchy, and inside the Frege hierarchy, is undecidable in general. That is genuinely new, and it is not a routine adaptation. The Leibniz side is built on a purpose-built finite Hilbert calculus for the logic of commutative rings, with the reduction going through Hilbert's tenth problem. The Frege side goes through the one-variable equational theory of relation algebras, and it even survives the restriction to finitely algebraizable logics. The constructions are explicit and the reductions are real. I checked the step that looks most fragile—Lemma 4.5, the selfextensionality of the ring calculus, which the author himself suggests skipping. The appendix proof is a valid induction. Lemma 4.4 legitimately linearizes the proofs because every rule has one premise and is symmetric, so checking the primitive rules under −, +, and · is enough. The derivations using (I'), (L'), (M'), (N), and (O) are correct. The completeness direction of Theorem 4.6, which is compressed, uses the standard fact that a logic is complete with respect to its reduced models, so that gap is not a problem. The minor typo in Theorem 5.2 ('free relation algebra' for 'free algebra') is cosmetic. The only real soft spot is the density of the case analysis in Theorem 4.8, where the claim that any derivation of y from x and ρ(x,y) must use (MP') or (A3') is stated quickly. I believe the claim is true, but a referee should ask for a few more lines there. Self-citation is not an issue here: the cited prior lemmas are published and independent, and the new content is the construction of CR and the reductions. The paper is written for people inside abstract algebraic logic; for them the payoff is clear. It deserves a serious referee and, if the small clarifications are made, acceptance. I would bring it to reading group.

Referee Report

0 major / 8 minor

Summary. The paper studies the computational problem of classifying syntactically presented logics within the Leibniz and Frege hierarchies of abstract algebraic logic. The main results (Theorems 4.10 and 5.3) state that for every level K of the Leibniz hierarchy (resp. Frege hierarchy), the problem of deciding whether the logic of a given finite consistent Hilbert calculus in a finite language belongs to K is undecidable. The Leibniz case is proved by a reduction from Hilbert's tenth problem: for each Diophantine equation p≈0 the author constructs a finite consistent calculus L(p) whose membership in any Leibniz-hierarchy level is equivalent to the solvability of p. A key technical ingredient is the finite Hilbert-style axiomatization of the logic L_CR associated with commutative rings (Theorem 4.6), supported by the selfextensionality proof of the calculus CR in the appendix. The Frege case is proved by a reduction from the one-variable equational theory of relation algebras: for each equation α≈β the author constructs a finitely algebraizable calculus L(α,β) whose membership in any Frege-hierarchy level is equivalent to the validity of α≈β in the variety of relation algebras. The Frege-undecidability result persists when restricted to finite consistent calculi that determine a finitely algebraizable logic.

Significance. If the results are correct, they establish a fundamental negative metatheorem: no general algorithm can locate a syntactically presented propositional logic in the Leibniz or Frege hierarchies. This is a significant contribution to abstract algebraic logic and to the metamathematics of nonclassical logics. The paper's strengths include explicit reductions from classical undecidable problems, a self-contained finite axiomatization of the logic of commutative rings, and a long but detailed appendix proof of the selfextensionality of the auxiliary calculus CR. The stress-test review confirmed that the load-bearing Lemma 4.5 is sound and that the completeness step in Theorem 4.6 is justified by standard completeness with respect to reduced models. I found no circularity: the negative results are derived from external undecidable problems, and the internal prior work (Lemma 4.1) is cited from a published source with stated assumptions.

minor comments (8)

[Section 5, Theorem 5.2 proof] In the proof of (iii)⇒(i), the text says "Then consider any i≤7" but Definition 5.1 lists only six formulas ϕ1,...,ϕ6; this should be i≤6.
[Section 5, Theorem 5.2 proof, Claim 5.2.1] The phrase "A is the free relation algebra" should read "A is the free algebra in V"; A is the free algebra on countably many generators in the variety V, not necessarily the free relation algebra.
[Section 5, Theorem 5.3 proof] The sentence "Since K contains the class of selfextensional logics and is included in the of class of fully Fregean ones" has the inclusions reversed; it should state that K contains the fully Fregean logics and is contained in the selfextensional ones.
[Definition 4.3] Rule (A) is missing a closing parenthesis on the right-hand side; it should end with "w + (u· (x· (y· z)))".
[Appendix, proof of Lemma 4.5] In the chain for the case of rule (O), the step "⊢⊣CR −x +−y (0)" should cite rule (O), not "(0)".
[Section 4, Theorem 4.8 proof] The case analysis in the proof of (iii)⇒(iv) claiming that any derivation of y must use (MP') or (A3') is quite compressed; an explicit justification that these are the only rules with non-↔ conclusions (and that the premise p(z)↔0 must therefore be derived) would improve readability.
[Section 4, Theorem 4.6 proof] The completeness direction LCR≤CR is stated briefly; it would be helpful to explicitly invoke the standard fact that a logic is complete with respect to its reduced models, as the argument uses that a separating reduced model over A∈AlgCR=CR is, by definition of LCR, a model of LCR.
[Corollary 4.9] The claim that ⟨Z,{s}⟩ is a model of L(p) is correct for every Diophantine equation p≈0, but since the earlier verification of this matrix in Theorem 4.8 was made under the assumption that p has no integer solution, a brief remark clarifying that the verification does not require that assumption would prevent confusion.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No free parameters or unexplained entities are used. The proof relies on established undecidability results and prior theorems in abstract algebraic logic and universal algebra, all cited. The logics introduced in the paper are explicitly defined by Hilbert calculi, so they are proof devices rather than postulated physical entities.

assumptions (5)

standard math Matiyasevich's theorem: deciding whether a Diophantine equation has an integer solution is undecidable.
Invoked in Section 4 as the external problem for the Leibniz hierarchy reduction.
standard math The equational theory of relation algebras in one variable is undecidable, as shown by Tarski and Givant [26, Section 8.5(viii)].
Invoked in Section 5 and used in the proof of Theorem 5.3.
standard math Standard theorems of abstract algebraic logic, including characterizations of protoalgebraic, equivalential, algebraizable, truth-equational, selfextensional, and Fregean logics, are taken from [14], [15], [16], [1], [23], and [27].
These supply the characterizations used in Lemmas 3.3, 3.4, 3.5 and in the final steps of Theorem 5.2; they are prior published results, not proved in the paper.
standard math Birkhoff's completeness theorem for equational logic.
Used in Example 4.2 and in the analysis of equational consequence in Section 4.
standard math The free algebra property of varieties: an equation holds in a variety iff it holds in its free algebra on suitable generators.
Used in the proof of Claim 5.2.1 within Theorem 5.2 to transfer failure of alpha and beta to evaluations in the expanded algebra.

how reviews work

0 comments

Cite this review

Pith. "Pith review of A computational glimpse at the Leibniz and Frege hierarchies." pith.science (2026). https://pith.science/paper/FCPDMI4E

@misc{pith2026190800922,
  author       = {Pith},
  title        = {Pith review of: A computational glimpse at the Leibniz and Frege hierarchies},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FCPDMI4E}},
  note         = {Machine review of arXiv:1908.00922}
}

read the original abstract

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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

27 extracted references · 17 canonical work pages

[1]

Albuquerque, J

H. Albuquerque, J. M. Font, R. Jansana, and T. Moraschini. Assertional logics, truth- equational 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

work page
[2]

S. V . Babyonyshev. Fully Fregean logics. Reports on Mathematical Logic, 37:59–77, 2003

2003
[3]

J. L. Bell and M. Machover. A Course in Mathematical Logic. North-Holland, Amsterdam, 1977

work page 1977
[4]

Bezhanishvili, T

G. Bezhanishvili, T. Moraschini, and J. G. Raftery. Epimorphism surjectivity in varieties of residuated structures. To appear in the Jounal of Algebra, 2017

work page 2017
[5]

W. J. Blok and E. Hoogland. The Beth property in Algebraic Logic. Studia Logica , 83(1–3):49–90, 2006

work page 2006
[6]

W. J. Blok and D. Pigozzi. Protoalgebraic logics. Studia Logica, 45:337–369, 1986

1986
[7]

W. J. Blok and D. Pigozzi. Algebraizable logics, volume 396 of Mem. Amer. Math. Soc. A.M.S., Providence, January 1989

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

work page 1997

Show all 27 references

[9]

Burris and H

S. Burris and H. P . Sankappanavar. A course in Universal Algebra . Available in in- ternet https://www.math.uwaterloo.ca/~snburris/htdocs/ualg.html, the millen- nium edition, 2012

2012
[10]

Chagrov and M

A. Chagrov and M. Zakharyaschev. Modal Logic, volume 35 of Oxford Logic Guides . Oxford University Press, 1997

1997
[11]

Czelakowski

J. Czelakowski. Protoalgebraic logics, volume 10 of Trends in Logic—Studia Logica Library . Kluwer Academic Publishers, Dordrecht, 2001

2001
[12]

Czelakowski and D

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

1999
[13]

Czelakowski and D

J. Czelakowski and D. Pigozzi. Fregean logics with the multiterm deduction theorem and their algebraization. Studia Logica, 78(1-2):171–212, 2004

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

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. 24 TOMMAS...

2009
[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

2009
[17]

J. M. Font and T. Moraschini. Logics of varieties, logics of semilattices, and conjunction. Logic Journal of the IGPL, 22:818–843, 2014

2014
[18]

A. I. Maltsev Identical relations on varieties of quasigroups. Mat. Sbornik, 69:3–12, 1966

1966
[19]

J. M. Font and T. Moraschini. A note on congruences of semilattices with sectionally ﬁnite height. Algebra Universalis, 72(3):287–293, 2014

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

2014
[21]

D. M. Gabbay and L. Maksimova. Interpolation and deﬁnability , volume 46 of Oxford Logic Guides. The Clarendon Press Oxford University Press, Oxford, 2005. Modal and intuitionistic logics

2005
[22]

Hoogland

E. Hoogland. Algebraic characterizations of various Beth deﬁnability properties. Studia Logica, Special Issue on Abstract Algebraic Logic , 65:91–112, 2000

2000
[23]

R. Jansana. Selfextensional logics with implication. In J.-Y. Beziau, editor, Logica universalis, pages 65–88. Birkh¨auser, Basel, 2005

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

1977
[25]

Matiyasevich

Y. Matiyasevich. Hilbert’s10th Problem. MIT Press, 1993

1993
[26]

Tarski and S

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

1987
[27]

W ´ojcicki

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

1988

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

Albuquerque, J

H. Albuquerque, J. M. Font, R. Jansana, and T. Moraschini. Assertional logics, truth- equational 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

work page

[2] [2]

S. V . Babyonyshev. Fully Fregean logics. Reports on Mathematical Logic, 37:59–77, 2003

2003

[3] [3]

J. L. Bell and M. Machover. A Course in Mathematical Logic. North-Holland, Amsterdam, 1977

work page 1977

[4] [4]

Bezhanishvili, T

G. Bezhanishvili, T. Moraschini, and J. G. Raftery. Epimorphism surjectivity in varieties of residuated structures. To appear in the Jounal of Algebra, 2017

work page 2017

[5] [5]

W. J. Blok and E. Hoogland. The Beth property in Algebraic Logic. Studia Logica , 83(1–3):49–90, 2006

work page 2006

[6] [6]

W. J. Blok and D. Pigozzi. Protoalgebraic logics. Studia Logica, 45:337–369, 1986

1986

[7] [7]

W. J. Blok and D. Pigozzi. Algebraizable logics, volume 396 of Mem. Amer. Math. Soc. A.M.S., Providence, January 1989

1989

[8] [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

work page 1997