pith. sign in

arxiv: 2605.17175 · v1 · pith:2X2RBHTRnew · submitted 2026-05-16 · 🧮 math.LO

Inception Display Calculi

Andrea De Domenico , Giuseppe Greco , Alessandra Palmigiano This is my paper

Pith reviewed 2026-05-20 14:01 UTC · model grok-4.3

classification 🧮 math.LO
keywords display calculiinductive axiomsSahlqvist axiomsLE-logicscut-eliminationsubstructural hierarchyanalytic rules
0
0 comments X

The pith

Display calculi extend to inductive axioms beyond the analytic inductive class, covering all Sahlqvist axioms.

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

The paper extends the framework of proper display calculi for LE-logics to axiomatic extensions based on inductive axioms that need not be analytic inductive. This broader class includes every Sahlqvist axiom and reaches the acyclic fragment of the substructural hierarchy for arbitrary signatures. The extension generates analytic rules in a uniform way that keeps the display property and cut-elimination intact. A sympathetic reader would care because the approach supplies a modular proof-theoretic setting for a larger collection of logics than before. If the extension works, more logics become accessible to automated analysis inside display calculi.

Core claim

The authors establish that the framework of proper display calculi for LE-logics can be extended to include axiomatic extensions with axioms that are inductive but not necessarily analytic inductive. This class of axioms covers and properly extends all Sahlqvist axioms. The present framework captures the whole acyclic fragment of the substructural hierarchy when generalized to arbitrary signatures. Analytic rules for these extensions are generated uniformly by applying unified correspondence theory and the ALBA algorithm.

What carries the argument

The uniform generation of analytic rules from inductive axioms that preserves the display property of the calculi.

If this is right

  • The extended calculi admit cut-elimination.
  • All Sahlqvist axioms fall inside the new class.
  • The acyclic fragment of the substructural hierarchy is captured for any signature.
  • Analytic rules are produced automatically for the wider class of axioms.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar rule-generation techniques might apply to cyclic fragments or other parts of the hierarchy.
  • The approach could support automated proof search for additional families of substructural logics.
  • Connections may exist to sequent systems for modal and relevance logics that use related correspondence methods.

Load-bearing premise

The correspondence algorithm produces rules that keep both the display property and cut-elimination when applied to non-analytic inductive axioms.

What would settle it

A concrete inductive axiom for which the generated rules produce a calculus in which cut-elimination fails.

read the original abstract

Display calculi were introduced by Nuel Belnap in `Display logic' (1982) as a natural extension of Gentzen's sequent calculi, as a uniform and modular framework capable of encompassing broad classes of logics. In `Unified correspondence as a proof-theoretic tool', the properly displayable (D)LE-logics are syntactically characterized as the logics axiomatised by analytic inductive axioms for any signature. We extend the framework of proper display calculi for LE-logics to include axiomatic extensions with axioms that are inductive but not necessarily analytic inductive. This class of axioms covers and properly extends all Sahlqvist axioms. The present framework takes inspiration from Schroeder-Heister's calculus of Higher-Level Rules and captures the whole acyclic fragment of the substructural hierarchy when generalized to arbitrary signatures. We apply unified correspondence theory and the algorithm ALBA to uniformly generate analytic rules for the aforementioned axiomatic extensions.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper extends the framework of proper display calculi for LE-logics to include axiomatic extensions with axioms that are inductive but not necessarily analytic inductive. This class covers and properly extends all Sahlqvist axioms. Using unified correspondence theory and the ALBA algorithm, analytic rules are generated for these extensions, taking inspiration from Schroeder-Heister's higher-level rules. The resulting framework is claimed to capture the whole acyclic fragment of the substructural hierarchy when generalized to arbitrary signatures while preserving the display property and cut-elimination.

Significance. If the central claims hold, the work would meaningfully broaden the scope of proper display calculi by providing a uniform method for incorporating a larger class of axioms (inductive but non-analytic-inductive) while retaining modularity and cut-elimination. It integrates correspondence-theoretic tools with proof theory in a way that could unify treatment of more logics in the substructural hierarchy across signatures.

major comments (2)
  1. [Application of ALBA] The section on application of ALBA: the central claim that ALBA-generated rules for non-analytic inductive axioms preserve the display property and admit cut-elimination via the existing metatheorem requires an explicit verification or proof that the higher-level rules satisfy the necessary display postulates and subformula conditions once the axioms leave the analytic-inductive class; the abstract and high-level description do not supply this check.
  2. [Capture of acyclic fragment] The claim that the framework captures the whole acyclic fragment of the substructural hierarchy in arbitrary signatures: a precise definition of the acyclic fragment in the generalized signature setting, together with a demonstration that the generated rules exactly correspond to it, is needed to support the extension beyond analytic inductive axioms.
minor comments (2)
  1. Clarify the precise distinction between analytic inductive and (non-analytic) inductive axioms with a small concrete example early in the paper.
  2. Add a reference to the original Schroeder-Heister higher-level rules paper when introducing the inspiration for the rule format.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments on our manuscript. We address the major comments point by point below and indicate the revisions we will make.

read point-by-point responses

  1. Referee: [Application of ALBA] The section on application of ALBA: the central claim that ALBA-generated rules for non-analytic inductive axioms preserve the display property and admit cut-elimination via the existing metatheorem requires an explicit verification or proof that the higher-level rules satisfy the necessary display postulates and subformula conditions once the axioms leave the analytic-inductive class; the abstract and high-level description do not supply this check.

    Authors: We agree that an explicit verification strengthens the presentation. The ALBA algorithm produces higher-level rules whose syntactic form is controlled by the inductive shape of the axiom, ensuring that the display postulates and subformula property are preserved by construction even outside the analytic-inductive class. In the revised manuscript we will add a dedicated subsection that spells out this verification, citing the relevant preservation lemmas from unified correspondence theory and confirming compatibility with the existing cut-elimination metatheorem. revision: yes

  2. Referee: [Capture of acyclic fragment] The claim that the framework captures the whole acyclic fragment of the substructural hierarchy in arbitrary signatures: a precise definition of the acyclic fragment in the generalized signature setting, together with a demonstration that the generated rules exactly correspond to it, is needed to support the extension beyond analytic inductive axioms.

    Authors: The acyclic fragment in the generalized signature is defined as the class of inductive axioms whose first-order correspondents have acyclic dependency graphs (extending the standard substructural hierarchy to arbitrary signatures). The exact correspondence follows from the completeness of ALBA: every such axiom is reduced to an equivalent set of analytic higher-level rules. We will insert a formal definition of the generalized acyclic fragment together with a theorem establishing the exact capture in the revised version. revision: yes

Circularity Check

1 steps flagged

Relies on prior unified correspondence and ALBA results for extending to non-analytic inductive axioms

specific steps
  1. self citation load bearing [Abstract]
    "In `Unified correspondence as a proof-theoretic tool', the properly displayable (D)LE-logics are syntactically characterized as the logics axiomatised by analytic inductive axioms for any signature. We extend the framework of proper display calculi for LE-logics to include axiomatic extensions with axioms that are inductive but not necessarily analytic inductive. ... We apply unified correspondence theory and the algorithm ALBA to uniformly generate analytic rules for the aforementioned axiomatic extensions."

    The load-bearing step of uniformly generating analytic rules for non-analytic inductive axioms (to preserve display property and cut-elimination) is justified by invoking unified correspondence theory and ALBA from the cited prior work, without an independent metatheorem or explicit verification shown for the generalized case; the extension claim thus partially reduces to the applicability of that prior result.

full rationale

The derivation extends proper display calculi by applying ALBA and unified correspondence theory (cited from prior work) to generate analytic rules for inductive but non-analytic-inductive axioms, claiming preservation of display property and cut-elimination while capturing the acyclic fragment. This relies on the prior characterization of properly displayable (D)LE-logics via analytic inductive axioms, but the extension itself introduces new content for the broader class without reducing the central claims to self-definition, fitted parameters, or unverified self-citation chains. The abstract provides no equations showing constructional equivalence, making the overall circularity minor and non-load-bearing for the new framework.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the applicability of unified correspondence theory and ALBA to the broader inductive class; no free parameters or new entities are mentioned in the abstract.

axioms (1)
  • domain assumption LE-logics can be extended by inductive axioms while remaining amenable to display calculi via ALBA-generated rules.
    Invoked when stating that the framework captures the acyclic fragment and generates analytic rules.

pith-pipeline@v0.9.0 · 5675 in / 1163 out tokens · 62578 ms · 2026-05-20T14:01:35.190536+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

34 extracted references · 34 canonical work pages · 1 internal anchor

  1. [1]

    Untersuchung ¨uber das Eliminationsproblem der Mathe- matischen Logik.Mathematische Annalen, 110:390–413, 1935

    Wilhelm Ackermann. Untersuchung ¨uber das Eliminationsproblem der Mathe- matischen Logik.Mathematische Annalen, 110:390–413, 1935

    work page 1935

  2. [2]

    Abstract cyclic proofs

    Bahareh Afshari and Dominik Wehr. Abstract cyclic proofs. In Agata Ciabattoni, Elaine Pimentel, and Ruy J. G. B. de Queiroz, editors,Logic, Language, Infor- mation, and Computation, pages 309–325, Cham, 2022. Springer International Publishing

    work page 2022

  3. [3]

    Nuel D. Belnap. Display logic.Journal of philosophical logic, 11(4):375–417, 1982

    work page 1982

  4. [4]

    Wijnberg

    Marta B ´ılkov´a, Giuseppe Greco, Alessandra Palmigiano, Apostolos Tzimoulis, and Nachoem M. Wijnberg. The logic of resources and capabilities.The Review of Symbolic Logic, 11(2):371–410, 2018

    work page 2018

  5. [5]

    Non-normal modal logics and conditional logics: Semantic analysis and proof theory.Information and Computation, 287:104756, 2022

    Jinsheng Chen, Giuseppe Greco, Alessandra Palmigiano, and Apostolos Tzi- moulis. Non-normal modal logics and conditional logics: Semantic analysis and proof theory.Information and Computation, 287:104756, 2022

    work page 2022

  6. [6]

    Syntactic completeness of proper display calculi.ACM Transactions on Computational Logic, 23:4:1–46, 2022

    Jinsheng Chen, Giuseppe Greco, Alessandra Palmigiano, and Apostolos Tzi- moulis. Syntactic completeness of proper display calculi.ACM Transactions on Computational Logic, 23:4:1–46, 2022

    work page 2022

  7. [7]

    From Axioms to An- alytic Rules in Nonclassical Logics

    Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. From Axioms to An- alytic Rules in Nonclassical Logics. InLogic in Computer Science, volume 8, pages 229–240, 2008. 28

    work page 2008

  8. [8]

    Power and Limits of Structural Display Rules.ACM Transactions on Computational Logic, 17(3):1–39, 2016

    Agata Ciabattoni and Revantha Ramanayake. Power and Limits of Structural Display Rules.ACM Transactions on Computational Logic, 17(3):1–39, 2016

    work page 2016

  9. [9]

    Algorithmic correspondence for intuitionistic modal mu-calculus.Theoretical Computer Science, 564:30–62, 2015

    Willem Conradie, Yves Fomatati, Alessandra Palmigiano, and Sumit Sourabh. Algorithmic correspondence for intuitionistic modal mu-calculus.Theoretical Computer Science, 564:30–62, 2015

    work page 2015

  10. [10]

    Unified Corre- spondence

    Willem Conradie, Silvio Ghilardi, and Alessandra Palmigiano. Unified Corre- spondence. In A. Baltag and A. Smets, editors,Johan van Benthem on Logic and Information Dynamics, volume 5 ofOutstanding Contributions to Logic, pages 933–975. Springer International Publishing, 2014

    work page 2014

  11. [11]

    Algorithmic cor- respondence and completeness in modal logic

    Willem Conradie, Valentin Goranko, and Dimiter Vakarelov. Algorithmic cor- respondence and completeness in modal logic. I. The core algorithm SQEMA. Logical Methods in Computer Science, 2:1–26, 2006

    work page 2006

  12. [12]

    Algorithmic correspondence and canonicity for distributive modal logic.Annals of Pure and Applied Logic, 163(3):338–376, 2012

    Willem Conradie and Alessandra Palmigiano. Algorithmic correspondence and canonicity for distributive modal logic.Annals of Pure and Applied Logic, 163(3):338–376, 2012

    work page 2012

  13. [13]

    Algorithmic correspondence and canonicity for non-distributive logics.Annals of Pure and Applied Logic, 170:923–974, 2019

    Willem Conradie and Alessandra Palmigiano. Algorithmic correspondence and canonicity for non-distributive logics.Annals of Pure and Applied Logic, 170:923–974, 2019

    work page 2019

  14. [14]

    Wijnberg

    Willem Conradie, Alessandra Palmigiano, Claudette Robinson, and Nachoem M. Wijnberg. Non-distributive logics: from semantics to meaning. In A. Rezus, editor,Contemporary Logic and Computing, volume 1 ofLandscapes in Logic, pages 38–86. College Publications, 2020

    work page 2020

  15. [15]

    Canonicity and Relativized Canonicity via Pseudo-Correspondence: an Application of ALBA

    Willem Conradie, Alessandra Palmigiano, Sumit Sourabh, and Zhiguang Zhao. Canonicity and Relativized Canonicity via Pseudo-Correspondence: an Applica- tion of ALBA. Submitted. ArXiv preprint 1511.04271, 2015

    work page internal anchor Pith review Pith/arXiv arXiv 2015

  16. [16]

    Davey and Hilary A

    Brian A. Davey and Hilary A. Priestley.Introduction to Lattices and Order. Cam- bridge University Press, 2002

    work page 2002

  17. [17]

    Phd thesis, Vrije Universiteit Amsterdam, December 2025

    Andrea De Domenico.Unified correspondence, proof-theoretically. Phd thesis, Vrije Universiteit Amsterdam, December 2025

    work page 2025

  18. [18]

    Algorithmic correspondence and analytic rules

    Andrea De Domenico and Giuseppe Greco. Algorithmic correspondence and analytic rules. In D. Fern ´andez-Duque, A. Palmigiano, and S. Pinchinat, edi- tors,Advances in Modal Logic, volume 14, pages 371–389. College Publications, 2022

    work page 2022

  19. [19]

    Multi-type Sequent Calculi

    Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, and Vlasta Sikimi ´c. Multi-type Sequent Calculi. In A. Indrzejczak, J. Kaczmarek, and M. Zawidski, editors,Proceedings Trends in Logic XIII, volume 13, pages 81–93, 2014. 29

    work page 2014

  20. [20]

    A multi-type calculus for inquisitive logic

    Sabine Frittella, Giuseppe Greco, Alessandra Palmigiano, and Fan Yang. A multi-type calculus for inquisitive logic. In J. V ¨a¨an¨anen, Å. Hirvonen, and R. de Queiroz, editors,Logic, Language, Information, and Computation, LNCS 9803, pages 215–233. Springer, 2016

    work page 2016

  21. [21]

    Gaggles, Gentzen and Galois: How to display your favourite sub- structural logic.Logic Journal of the IGPL, 5(5):669–694, 1998

    Rajeev Gor ´e. Gaggles, Gentzen and Galois: How to display your favourite sub- structural logic.Logic Journal of the IGPL, 5(5):669–694, 1998

    work page 1998

  22. [22]

    Substructural logics on display.Logic Journal of IGPL, 6(3):451– 504, 1998

    Rajeev Gor ´e. Substructural logics on display.Logic Journal of IGPL, 6(3):451– 504, 1998

    work page 1998

  23. [23]

    Algebraic proof theory for LE-logics.ACM Trans

    Giuseppe Greco, Peter Jipsen, Fei Liang, Alessandra Palmigiano, and Apostolos Tzimoulis. Algebraic proof theory for LE-logics.ACM Trans. Comput. Logic, 25(1), 2024

    work page 2024

  24. [24]

    Logics for rough concept analysis

    Giuseppe Greco, Peter Jipsen, Krishna Manoorkar, Alessandra Palmigiano, and Apostolos Tzimoulis. Logics for rough concept analysis. In A. Khan and A. Manuel, editors,Logic and Its Applications, ICLA 2019, volume 11600 of LNCS, pages 144–159. Springer-Verlag Berlin Heidelberg, 2019

    work page 2019

  25. [25]

    Proper multi-type display calculi for rough algebras

    Giuseppe Greco, Fei Liang, Krishna Manoorkar, and Alessandra Palmigiano. Proper multi-type display calculi for rough algebras. In13th Workshop on Logical and Semantic Frameworks with Applications, 2019

    work page 2019

  26. [26]

    Andrew Moshier, and Alessandra Palmigiano

    Giuseppe Greco, Fei Liang, M. Andrew Moshier, and Alessandra Palmigiano. Multi-type display calculus for semi De morgan logic.Logic, Language, Infor- mation, and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18-21, 2017, Proceedings, pages 199–215, 2017

    work page 2017

  27. [27]

    Bi- lattice logic properly displayed.Fuzzy Sets and Systems, 363:138–155, 2019

    Giuseppe Greco, Fei Liang, Alessandra Palmigiano, and Umberto Rivieccio. Bi- lattice logic properly displayed.Fuzzy Sets and Systems, 363:138–155, 2019

    work page 2019

  28. [28]

    Unified correspondence as a proof-theoretic tool.Journal of Logic and Computation, 28(7):1367–1442, 2018

    Giuseppe Greco, Minghui Ma, Alessandra Palmigiano, Apostolos Tzimoulis, and Zhiguang Zhao. Unified correspondence as a proof-theoretic tool.Journal of Logic and Computation, 28(7):1367–1442, 2018

    work page 2018

  29. [29]

    Proof analysis beyond geometric theories: from rule systems to sys- tems of rules.Journal of Logic and Computation, 26:513–537, 2014

    Sara Negri. Proof analysis beyond geometric theories: from rule systems to sys- tems of rules.Journal of Logic and Computation, 26:513–537, 2014

    work page 2014

  30. [30]

    Unified inverse correspondence for LE-logics.Annals of Pure and Applied Logic, page 103635, 2025

    Alessandra Palmigiano and Mattia Panettiere. Unified inverse correspondence for LE-logics.Annals of Pure and Applied Logic, page 103635, 2025

    work page 2025

  31. [31]

    Completeness and Correspondence in the First and Second Order Semantics for Modal Logic

    Henrik Sahlqvist. Completeness and Correspondence in the First and Second Order Semantics for Modal Logic. InStudies in Logic and the Foundations of Mathematics, volume 82, pages 110–143. Elsevier, 1975

    work page 1975

  32. [32]

    The Calculus of Higher-Level Rules, Propositional Quantification, and the Foundational Approach to Proof-Theoretic Harmony.Stu- dia Logica, 102:1185–1216, 2014

    Peter Schroeder-Heister. The Calculus of Higher-Level Rules, Propositional Quantification, and the Foundational Approach to Proof-Theoretic Harmony.Stu- dia Logica, 102:1185–1216, 2014. 30

    work page 2014

  33. [33]

    Springer Dordrecht, 1998

    Heinrich Wansing.Displaying modal logic, volume 3 ofTrends in Logic. Springer Dordrecht, 1998

    work page 1998

  34. [34]

    Springer, Dordrecht, 2002

    Heinrich Wansing.Sequent Systems for Modal Logics, volume 8, pages 61–145. Springer, Dordrecht, 2002. A Proper display calculi Definition A.1.A proof system enjoys thedisplay propertyif, for every sequentΠ⊢Σ and every substructureΥof eitherΠorΣ, the sequentΠ⊢Σcan be equivalently trans- formed, using the rules of the system, into a sequent which is either ...

    work page 2002