pith. sign in

arxiv: 2605.17161 · v1 · pith:GUDGS6FLnew · submitted 2026-05-16 · 🧮 math.LO

Modular constructive Lyndon interpolation for nondistributive logics

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

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

classification 🧮 math.LO
keywords Lyndon interpolationdisplay calculilattice expansion logicsLE-logicsnondistributive logicsmodal logictense logicinterpolation property
0
0 comments X

The pith

Display calculi establish the Lyndon interpolation property for basic lattice expansion logics.

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

The paper shows that basic lattice expansion logics satisfy the Lyndon interpolation property by means of display calculi. This property guarantees that an implication between two formulas yields an interpolant built only from their common symbols. The method is constructive, extracting the interpolant directly from a given derivation, and modular, so that new axioms preserve the property once their corresponding structural rules pass a local check. A reader would care because these logics capture modal and tense reasoning without relying on distributivity, and interpolation helps separate the shared content from the specific premises and conclusions. The framework works for arbitrary signatures and applies to the tense version of Holliday's fundamental modal logic.

Core claim

We establish the Lyndon interpolation property for basic lattice expansion logics (LE-logics) in arbitrary signatures using display calculi. Our approach is constructive, yielding interpolants algorithmically from derivations, and modular, in the sense that interpolation for axiomatic extensions can be obtained by verifying a local interpolation property for the analytic structural rules corresponding to the additional axioms. To this end, we identify a class of interpolation-safe structural rules preserving local Lyndon interpolation. As an application, the tense version of Holliday's fundamental modal logic enjoys the Lyndon interpolation property.

What carries the argument

Display calculi together with the identified class of interpolation-safe structural rules that preserve local Lyndon interpolation.

Load-bearing premise

The additional axioms of an LE-logic must correspond to analytic structural rules that belong to the class of interpolation-safe rules preserving local Lyndon interpolation.

What would settle it

A concrete counterexample would be an LE-logic extended by an analytic structural rule outside the interpolation-safe class for which some implication has no Lyndon interpolant, or a derivation in the calculus from which no interpolant can be extracted.

read the original abstract

We establish the Lyndon interpolation property for basic lattice expansion logics (LE-logics) in arbitrary signatures using display calculi. Our approach is constructive, yielding interpolants algorithmically from derivations, and modular, in the sense that interpolation for axiomatic extensions can be obtained by verifying a local interpolation property for the analytic structural rules corresponding to the additional axioms. To this end, we identify a class of interpolation-safe structural rules preserving local Lyndon interpolation. As applications of the general framework, we show that the tense version of Holliday's fundamental modal logic enjoys the Lyndon interpolation property.

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

0 major / 3 minor

Summary. The manuscript establishes the Lyndon interpolation property for basic lattice expansion logics (LE-logics) in arbitrary signatures using display calculi. The approach is constructive, yielding interpolants algorithmically from derivations, and modular: interpolation for axiomatic extensions follows from verifying a local Lyndon interpolation property for the analytic structural rules corresponding to the additional axioms. The authors identify a class of interpolation-safe structural rules that preserve this local property. As an application, they show that the tense version of Holliday's fundamental modal logic enjoys the Lyndon interpolation property.

Significance. If the results hold, the paper makes a substantial contribution to proof theory for nondistributive and substructural logics by supplying a general, modular framework for Lyndon interpolation. The constructive character (algorithmic extraction of interpolants) and the isolation of an interpolation-safe rule class are explicit strengths that enable systematic extension to new axioms without re-proving the base case. The application to the tense logic provides a concrete, falsifiable instance. These features align with the field's interest in analytic calculi and interpolation for lattice-based logics.

minor comments (3)
  1. §3.2, Definition 3.5: the local Lyndon interpolation condition is stated in terms of the display calculus; a short remark on how this reduces to the standard syntactic interpolation property for the Hilbert system would aid readers unfamiliar with display calculi.
  2. §5, Example 5.3: the verification that the structural rules for the tense extension are interpolation-safe is sketched; expanding the inductive step for one rule with explicit formula tracking would make the argument easier to follow without lengthening the paper substantially.
  3. Notation: the use of 'LE-logics' and 'basic' is consistent, but a single sentence in the introduction recalling that signatures may include arbitrary lattice expansions would prevent any momentary ambiguity for readers coming from modal logic.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, significance assessment, and recommendation of minor revision. No specific major comments appear in the report, so we have no individual points requiring point-by-point rebuttal or revision at this stage. We will incorporate any minor editorial suggestions during the revision process.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained

full rationale

The paper derives the Lyndon interpolation property for LE-logics via explicit construction of display calculi in arbitrary signatures, cut-elimination/analyticity proofs, and an inductive argument showing that a defined class of interpolation-safe structural rules preserves local Lyndon interpolation. These elements are supplied directly in the manuscript with definitions of the rule class and local condition; the modular inheritance for axiomatic extensions follows from the preservation theorem rather than from any self-citation chain or by-construction renaming of inputs. No load-bearing step reduces to a fitted parameter or prior self-result by definition.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper builds on standard background results about display calculi and analytic rules from prior proof-theoretic literature.

axioms (2)
  • standard math Display calculi admit cut-elimination and have the subformula property for the base logic.
    Invoked as the foundation for constructive interpolation extraction.
  • domain assumption Structural rules can be classified as analytic and interpolation-safe.
    Central to the modularity claim for axiomatic extensions.

pith-pipeline@v0.9.0 · 5619 in / 1144 out tokens · 43925 ms · 2026-05-20T14:19:29.509632+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages

  1. [1]

    D’Agostino, Interpolation in non-classical logics, Synthese 164 (2008) 421–435

    G. D’Agostino, Interpolation in non-classical logics, Synthese 164 (2008) 421–435. URL: http: //www.jstor.org/stable/40271081

    work page arXiv 2008

  2. [2]

    Fussner, Interpolation in Non-Classical Logics, in: B

    W. Fussner, Interpolation in Non-Classical Logics, in: B. ten Cate, J. C. Jung, P. Koopmann, C. Wernhard, F. Wolter (Eds.), Theory and Applications of Craig Interpolation, Ubiquity Press, 2026

    work page 2026

  3. [3]

    van der Giessen, R

    I. van der Giessen, R. Jalali, R. Kuznets, Interpolation in Proof Theory, in: B. ten Cate, J. C. Jung, P. Koopmann, C. Wernhard, F. Wolter (Eds.), Theory and Applications of Craig Interpolation, Ubiquity Press, 2026

    work page 2026

  4. [4]

    T. Lyon, A. Tiu, R. Goré, R. Clouston, Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents, in: M. Fernandez, A. Muscholl (Eds.), 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), Leibniz International Proceedings in Informatics, 2020, pp. 1–16

    work page 2020

  5. [5]

    Kuznets, Proving Craig and Lyndon interpolation using labelled sequent calculi, in: L

    R. Kuznets, Proving Craig and Lyndon interpolation using labelled sequent calculi, in: L. Michael, A. Kakas (Eds.), Logics in Artificial Intelligence, Springer International Publishing, Cham, 2016, pp. 320–335

    work page 2016

  6. [6]

    Kuznets, Interpolation method for multicomponent sequent calculi, in: International Symposium on Logical Foundations of Computer Science, Springer, 2015, pp

    R. Kuznets, Interpolation method for multicomponent sequent calculi, in: International Symposium on Logical Foundations of Computer Science, Springer, 2015, pp. 202–218

    work page 2015

  7. [7]

    Conradie, A

    W. Conradie, A. Palmigiano, Algorithmic correspondence and canonicity for non-distributive logics, Annals of Pure and Applied Logic 170 (2019) 923–974

    work page 2019

  8. [8]

    Conradie, A

    W. Conradie, A. Palmigiano, C. Robinson, N. M. Wijnberg, Non-distributive logics: from semantics to meaning, in: A. Rezus (Ed.), Contemporary Logic and Computing, volume 1 ofLandscapes in Logic, College Publications, 2020, pp. 38–86

    work page 2020

  9. [9]

    Greco, P

    G. Greco, P. Jipsen, F. Liang, A. Palmigiano, A. Tzimoulis, Algebraic proof theory for LE-logics, ACM Trans. Comput. Logic 25 (2024). URL: https://doi.org/10.1145/3632526. doi:10.1145/3632526

    work page doi:10.1145/3632526 2024

  10. [10]

    R. N. Almeida, N. Bezhanishvili, S. Lemal, Superamalgamation for modal lattices via non- distributive dualities, 2026. URL: https://arxiv.org/abs/2602.20380.arXiv:2602.20380

    work page arXiv 2026

  11. [11]

    Holliday, A fundamental non-classical logic, Logics 1 (2023) 36–79

    W. Holliday, A fundamental non-classical logic, Logics 1 (2023) 36–79

    work page 2023

  12. [12]

    W. H. Holliday, Modal logic, fundamentally, in: A. Ciabattoni, D. Gabelaia, I. Sedlár (Eds.), Advances in Modal Logic, Vol. 15, College Publications, 2024

    work page 2024

  13. [13]

    Greco, M

    G. Greco, M. Ma, A. Palmigiano, A. Tzimoulis, Z. Zhao, Unified correspondence as a proof-theoretic tool, Journal of Logic and Computation 28 (2018) 1367–1442

    work page 2018

  14. [14]

    J. Chen, G. Greco, A. Palmigiano, A. Tzimoulis, Syntactic completeness of proper display calculi, ACM Transactions on Computational Logic 23:4 (2022) 1–46

    work page 2022

  15. [15]

    De Domenico, Unified correspondence, proof-theoretically, Phd-thesis - research and graduation internal, Vrije Universiteit Amsterdam, 2025

    A. De Domenico, Unified correspondence, proof-theoretically, Phd-thesis - research and graduation internal, Vrije Universiteit Amsterdam, 2025. doi:10.5463/thesis.1412

    work page doi:10.5463/thesis.1412 2025

  16. [16]

    De Domenico, G

    A. De Domenico, G. Greco, A. Palmigiano, Inception display calculi, 2026. To appear in the Special Issue ofStudia Logicain memory of Nuel Belnap (1930–2024), edited by Thomas Müller, Tomasz Placek, and Heinrich Wansing

    work page 2026

  17. [17]

    Conradie, A

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

    work page 2012

  18. [18]

    Conradie, S

    W. Conradie, S. Ghilardi, A. Palmigiano, Unified Correspondence, in: A. Baltag, A. Smets (Eds.), Johan van Benthem on Logic and Information Dynamics, volume 5 ofOutstanding Contributions to Logic, Springer International Publishing, 2014, pp. 933–975

    work page 2014

  19. [19]

    Brotherston, R

    J. Brotherston, R. Goré, Craig Interpolation in Displayable Logics, in: K. Brünnler, G. Metcalfe (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods, Springer Berlin Heidelberg, Berlin, Heidelberg, 2011, pp. 88–103. Declaration on Generative AI The author(s) have not employed any Generative AI tools

    work page 2011