Pith. sign in

REVIEW 36 references

On the complexity of the Leibniz hierarchy

T0 review · 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 Determining whether the logic of a finite reduced matrix is algebraizable, weakly algebraizable, equivalential, protoalgebraic, or order algebraizable is EXPTIME-complete; for truth-equational logic it is EXPTIME-hard.

arxiv 1908.00924 v1 pith:TBHZH7LP submitted 2019-08-01 math.LO

T. Moraschini This is my paper · ORCID
classification math.LO
keywords algebraizableexptimelogicproblemsameclassclassescomplete
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

Abstract algebraic logic sorts propositional logics by how their consequence relations behave. One compact way to present a logic is a finite logical matrix, essentially a finite algebra with a designated set of truth values. This paper asks how hard it is to decide, given such a finite matrix, which level of the Leibniz hierarchy the logic it defines belongs to. The hierarchy includes protoalgebraic, equivalential, weakly algebraizable, algebraizable, and truth-equational logics, which differ in whether equivalence and truth predicates can be defined by formulas and equations. The author proves that for the main classes this decision problem is complete for EXPTIME, meaning that in the worst case it requires exponential time and no substantially faster general algorithm is expected. The lower-bound proof reduces a known EXPTIME-complete problem, whether a given function belongs to the clone generated by an algebra, to the Leibniz hierarchy classification problem. The reduction uses two custom-built finite matrices, called A-sharp and A-flat, whose logical properties are carefully engineered to encode exactly the clone membership question. For truth-equational logic, the problem is shown to be EXPTIME-hard, while a matching upper bound remains open. The paper also sketches the same EXPTIME-completeness result for order algebraizable logics. The results complement earlier work showing that the analogous classification problem for Hilbert-style presentations of logics is undecidable.
Extended reading notes

Core claim

Theorem 5.5: for every level K of the Leibniz hierarchy in Figure 1, the problem of determining whether the logic of a finite reduced matrix of finite type belongs to K is EXPTIME-hard. Corollary 5.6 adds EXPTIME-completeness for all these levels except truth-equational, and Corollary 5.7 adds EXPTIME-completeness for order algebraizable logics.

Load-bearing premise

The hardness direction rests on Lemma 5.2's implication (iv)=>(v), which asserts that if the logic of the matrix ⟨A♮,F♮⟩ is protoalgebraic then the unary operation h belongs to the clone of A. The proof of that implication depends on the technical tree-property lemmas in the Appendix, Lemmas 6.3 through 6.7, which characterize how formulas in the algebra A♮ can evaluate; if any of these lemmas is wrong, the reduction from the EXPTIME-complete problem Gen-clo1_3 collapses.

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.

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

The paper introduces explicit finite algebras A♮ and A♭ as proof constructions, but these are fully defined from the input algebra and function h, not postulated entities with unexplained properties. Their properties are proved in Section 4 and the Appendix. There are no fitted parameters, no hand-chosen constants used to force the result, and no invented physical or model-theoretic entities requiring independent experimental evidence.

assumptions (5)
  • standard math The problem Gen-clo1_3, testing whether a unary operation h belongs to the clone of a finite algebra A, is complete for EXPTIME.
    Theorem 5.1 cites Bergman, Juedes, and Slutzki [4, Theorem 3.7] for this external EXPTIME-completeness result. The hardness proofs in Lemmas 5.2 and 5.4 reduce from this problem, so the entire lower-bound argument depends on it.
  • domain assumption The characterizations of protoalgebraic, equivalential, and weakly algebraizable logics determined by finite matrices given in Theorem 2.1.
    Theorem 2.1 cites Font's textbook [14] for items 1 and 2 and proves item 3 using standard class operators. These characterizations underpin the EXPTIME upper bounds in Lemma 3.1 and the reduction equivalence in Lemma 5.2.
  • domain assumption For a logic determined by a finite set of finite matrices M, the equality Mod*(⊣) = (PsdS(M))* holds, and protoalgebraic logics have reduced model classes closed under subdirect products.
    This is used in the proofs of Theorem 2.1(3), Lemma 2.2, and Lemma 3.2. The paper attributes the relevant theorems to Font [14, Theorems 4.4, 4.7, and 6.17].
  • standard math The free n-generated algebra in the variety generated by a finite algebra A is isomorphic to a subalgebra of A^{A^n}.
    This is used in Lemmas 3.1 and 3.2 to bound the sizes of the free one- and two-generated algebras Tm(x) and Tm(x,y), which makes the upper-bound algorithms exponential or double exponential. The paper cites Berman [5].
  • standard math Finite automaton state minimization can be performed in O(n log n) time.
    Used in Lemma 3.1 to compute Leibniz congruences by reducing the problem to automaton minimization. The paper cites Hopcroft [23].

how reviews work

0 comments
Cite this review

Pith. "Pith review of On the complexity of the Leibniz hierarchy." pith.science (2026). https://pith.science/paper/TBHZH7LP

@misc{pith2026190800924,
  author       = {Pith},
  title        = {Pith review of: On the complexity of the Leibniz hierarchy},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TBHZH7LP}},
  note         = {Machine review of arXiv:1908.00924}
}
read the original abstract

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

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

36 extracted references · 29 canonical work pages

  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 , volume 16 of Outstanding Contributions. Springer-Verlag, 2018

    work page 2018

  2. [2]

    Arora and B

    S. Arora and B. Barak. Computational Complexity: A Modern Approach . Cambridge University Press, 2009

    2009

  3. [3]

    C. Bergman. Universal Algebra: Fundamentals and Selected Topics. Chapman & Hall Pure and Applied Mathematics. Chapman and Hall/CRC, 2011

    2011

  4. [4]

    Bergman, D

    C. Bergman, D. Juedes, and G. Slutzki. Computational complexity of term-equivalence. International Journal of Algebra and Computation , 9(1):113–128, 1999

    work page 1999

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

    work page 2005

  6. [6]

    W. J. Blok and B. J ´onsson. Algebraic structures for logic. A course given at the 23rd Holiday Mathematics Symposium, New Mexico State University, 1999

    work page 1999

  7. [7]

    W. J. Blok and B. J ´onsson. Equivalence of consequence operations. Studia Logica, 83(1– 3):91–110, 2006

    work page 2006

  8. [8]

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

    1989

Show all 36 references
  1. [9]

    W. J. Blok and D. Pigozzi. Algebraic semantics for universal Horn logic without equality. pages 1–56. Heldermann, Berlin, 1992

    1992

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

    2003

  3. [11]

    Czelakowski

    J. Czelakowski. Reduced products of logical matrices. Studia Logica, 39:19–43, 1980

    1980

  4. [12]

    Czelakowski

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

    2001

  5. [13]

    Dellunde and R

    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

    1996

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

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

    2017

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

  9. [17]

    Freese and M

    R. Freese and M. A. Valeriote. On the complexity of some Maltsev conditions. Interna- tional Journal of Algebra and Computation , 19(1):41–77, 2009

    2009

  10. [18]

    O. C. Garc ´ıa and W. Taylor.The lattice of interpretability types of varieties , volume 50. Mem. Amer. Math. Soc., 1984

    1984

  11. [19]

    Gr ¨atzer

    G. Gr ¨atzer. Two Mal’cev-Type Theorems in Universal Algebra. Journal of Combinatorial Theory, 8:334–342, 1970

    1970

  12. [20]

    Hartmanis and R

    J. Hartmanis and R. E. Stearns. On the computational complexity of algorithms. Transactions of the Americal Mathematical Society, 117:285–306, 1965. 24 TOMMASO MORASCHINI

    1965

  13. [21]

    D. Hobby. Finding type sets is NP-hard. International Journal of Algebra and Computation, 1(4):437–444, 1991

    1991

  14. [22]

    Hobby and R

    D. Hobby and R. McKenzie. The structure of finite algebras, volume 76 of Contemporary Mathematics. American Mathematical Society, Providence, RI, 1988

    1988

  15. [23]

    Hopcroft

    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

    1971

  16. [24]

    Jansana and T

    R. Jansana and T. Moraschini. The poset of all logics I: interpretations and lattice struc- ture. Manuscript, 2019. Available online at http://uivty.cs.cas.cz/~moraschini/ files/submitted/poset-all-logics-1.pdf

    2019

  17. [25]

    Jansana and T

    R. Jansana and T. Moraschini. The poset of all logics II: Leibniz classes and hierarchy. Manuscript, 2019

    2019

  18. [26]

    Jansana and T

    R. Jansana and T. Moraschini. The poset of all logics III: finitely presentable logics. Manuscript, 2019

    2019

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

    2013

  20. [28]

    R. N. McKenzie, G. F. McNulty, and W. F. Taylor.Algebras, lattices, varieties. Vol. I. The Wadsworth & Brooks/Cole Mathematics Series. Wadsworth & Brooks/Cole Advanced Books & Software, Monterey, CA, 1987

    1987

  21. [29]

    Moraschini

    T. Moraschini. A computational glimpse at the Leibniz and Frege hierarchies. Annals of Pure and Applied Logic, 169(1):1–20, January 2018

    2018

  22. [30]

    Moraschini

    T. Moraschini. A study of the truth predicates of matrix semantics. Review of Symbolic Logic, 11(4):780–804, 2018

    2018

  23. [31]

    C. H. Papadimitriou. Computational complexity. Addison-Wesley Publishing Company, Reading, MA, 1994

    1994

  24. [32]

    J. G. Raftery. Correspondences between Gentzen and Hilbert systems. The Journal of Symbolic Logic, 71(3):903–957, 2006

    2006

  25. [33]

    J. G. Raftery. The equational definability of truth predicates. Reports on Mathematical Logic, (41):95–149, 2006

    2006

  26. [34]

    J. G. Raftery. A perspective on the algebra of logic.Quaestiones Mathematicae, 34:275–325, 2011

    2011

  27. [35]

    J. G. Raftery. Order algebraizable logics. Annals of Pure and Applied Logic, 164(3):251–283, 2013

    2013

  28. [36]

    W. Taylor. Characterizing Mal’cev conditions. Algebra Universalis, 3:351–397, 1973. Institute of Computer Science, A cademy of Sciences of Czech Republic, P od Vod ´arenskou v ˇeˇz´i 271/2, 182 07 P rague 8, Czech Republic E-mail address: moraschini@cs.cas.cz

    1973

Pith tools

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