pith. sign in

arxiv: 2606.31890 · v1 · pith:LJTQWTLXnew · submitted 2026-06-30 · 💻 cs.LO

Uniform Lyndon Interpolation via Non-wellfounded Proofs

Borja Sierra Miranda (University of Bern) , Thomas Studer (University of Bern) This is my paper

Pith reviewed 2026-07-01 02:24 UTC · model grok-4.3

classification 💻 cs.LO
keywords uniform Lyndon interpolationprovability logic GLSnon-wellfounded proofssequent calculuscut eliminationinterpolation
0
0 comments X

The pith

The provability logic GLS has uniform Lyndon interpolation, shown via non-wellfounded sequent calculus.

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

The paper establishes uniform Lyndon interpolation for GLS, a strengthening of its known uniform interpolation that requires the interpolant to preserve the polarity of each variable. The proof proceeds inside a non-wellfounded sequent calculus for the logic, from which interpolants are extracted directly. The same framework supplies a new demonstration of cut elimination. This settles an open question for GLS and supplies a template usable for other provability logics once a non-wellfounded calculus is at hand.

Core claim

We show that GLS has uniform Lyndon interpolation by constructing interpolants from non-wellfounded proofs in a sequent calculus for the logic. The construction tracks polarities of propositional variables throughout the infinite branches. The same calculus yields an alternative proof of cut elimination for GLS.

What carries the argument

A non-wellfounded sequent calculus for GLS, whose infinite but locally finite proofs allow extraction of polarity-preserving interpolants.

If this is right

  • GLS satisfies both uniform interpolation and uniform Lyndon interpolation.
  • Cut elimination for GLS receives an alternative non-wellfounded proof.
  • The method extends directly to any other provability logic that possesses a non-wellfounded sequent calculus.
  • Lyndon interpolation holds in uniform form for GLS.

Where Pith is reading between the lines

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

  • Other modal logics admitting non-wellfounded calculi may inherit uniform Lyndon interpolation by the same route.
  • The explicit construction could support algorithmic extraction of Lyndon interpolants in GLS.
  • Links to cut-elimination techniques in related non-wellfounded systems become available for comparison.

Load-bearing premise

A non-wellfounded sequent calculus for GLS exists and the interpolation construction can be carried out inside it.

What would settle it

A concrete GLS formula that possesses a uniform interpolant but lacks any Lyndon interpolant, or a point in the non-wellfounded calculus where the polarity-tracking step fails.

Figures

Figures reproduced from arXiv: 2606.31890 by Borja Sierra Miranda (University of Bern), Thomas Studer (University of Bern).

Figure 1
Figure 1. Figure 1: Sequent Rules 3 The logic GLS and its sequent calculi We fix an infinite countable set Var whose elements are called propositional variables. Definition 3.1. We define the language L◻ given by the following Backus-Naur form: φ ::= p | ⊥ | φ → φ | ◻φ, where p ∈ Var. The expressions of L◻ are called (modal) formulas. The complexity of a formula φ is the number of logical connectives of φ, and will be denoted… view at source ↗
Figure 2
Figure 2. Figure 2: Structural Rules Definition 3.3. We make the following definitions. 1. G GLS is the wellfounded calculus with rules (ax), (⊥L), (⊥R), (→L), (→R), (◻GL) and (T). 3 2. G ∞GLS is the local progress calculus with rules (ax), (⊥L), (⊥R), (→L), (→R), (◻K4) and (T). Progress only occurs at the premise of (◻K4). Lemma 3.4. For any formula φ and multisets Γ,∆ we have that 1. G GLS ⊢ φ,Γ ≫ φ,∆ and G ∞GLS ⊢ φ,Γ ≫ φ,∆… view at source ↗
Figure 3
Figure 3. Figure 3: Interpolation Template Rules Given a sequent S = Γ ≫ ∆ we define its saturation complexity, denoted |S|Sat, as the multiset {|φ| | φ ∈ Γ,φ not left saturated in S}∪{|φ| | φ ∈ ∆,φ not right saturated in S}. We assume the saturation complexity comes with the multiset ordering attached to it, so |S|Sat < |S ′ |Sat means that |S|Sat is obtained from |S ′ |Sat by the process of taking out at least one element a… view at source ↗
read the original abstract

Non-wellfounded proof theory has been applied to establish uniform interpolation and Lyndon interpolation (separately) for multiple logics. However, it has not yet been used to prove uniform Lyndon interpolation. We close this gap by showing uniform Lyndon interpolation for the provability logic GLS. This logic was known to have uniform interpolation, but it was open whether it has uniform Lyndon interpolation (or at least non-uniform Lyndon interpolation). The methodology we provide is easy to adapt to other provability logics if a non-wellfounded sequent calculus is available for them. In addition, we offer an alternative proof of cut elimination for GLS via non-wellfounded proofs.

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 / 2 minor

Summary. The manuscript establishes uniform Lyndon interpolation for the provability logic GLS by constructing (or employing) a non-wellfounded sequent calculus, proving cut elimination therein, and deriving the interpolation property from the resulting proofs. It also supplies an alternative non-wellfounded proof of cut elimination for GLS and states that the same methodology applies to other provability logics once a suitable non-wellfounded calculus is available. The result closes the open question of whether GLS possesses uniform (or even non-uniform) Lyndon interpolation, given that uniform interpolation was already known.

Significance. If the derivations hold, the work supplies the first uniform Lyndon interpolation result for GLS and demonstrates that non-wellfounded proof theory can simultaneously handle both uniform interpolation and its Lyndon strengthening. The alternative cut-elimination argument and the explicit adaptability claim are additional strengths; the latter supplies a reusable template rather than an ad-hoc construction for a single logic.

minor comments (2)
  1. The abstract and introduction should clarify whether the non-wellfounded calculus for GLS is taken from prior work or newly constructed in the paper, and which specific sequent rules are added or modified to obtain the Lyndon property.
  2. Notation for the non-wellfounded rules and the precise statement of the uniform Lyndon interpolation theorem (including the precise form of the interpolant) should be introduced early and used consistently throughout.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the accurate summary of our results on uniform Lyndon interpolation for GLS and for noting the significance of the non-wellfounded approach, the alternative cut-elimination proof, and the adaptability claim. No specific major comments were listed in the report.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper constructs a non-wellfounded sequent calculus for GLS, establishes cut elimination inside it, and derives uniform Lyndon interpolation as a consequence. This chain relies on standard proof-theoretic constructions and does not reduce any target property to a fitted parameter, self-definition, or load-bearing self-citation. The abstract explicitly frames the result as obtained from the calculus rather than presupposed by it. No equations or steps equate the claimed interpolation property to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Review performed on abstract only; no concrete free parameters, invented entities, or ad-hoc axioms are visible. The central claim rests on the existence of a non-wellfounded sequent calculus for GLS.

axioms (1)
  • domain assumption Existence of a non-wellfounded sequent calculus for GLS that is adequate for the interpolation argument
    Abstract conditions the method on availability of such a calculus.

pith-pipeline@v0.9.1-grok · 5635 in / 1053 out tokens · 44233 ms · 2026-07-01T02:24:06.692306+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

26 extracted references · 24 canonical work pages · 1 internal anchor

  1. [1]

    Afshari, G

    B. Afshari, G. E. Leigh & G. Menéndez Turata (2021): Uniform Interpolation from Cyclic Proofs: The Case of Modal Mu-Calculus . In: Automated Reasoning with Analytic Tableaux and Related Methods: 30th In- ternational Conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021, Proceedings , Springer- Verlag, Berlin, Heidelberg, p. 335–353, doi:10.1007/9...

    work page doi:10.1007/978-3-030-86059-2_20 2021

  2. [2]

    Afshari, G

    B. Afshari, G. E. Leigh & G. Menéndez Turata (2023): A Cyclic Proof System for Full Computation Tree Logic. In B. Klin & E. Pimentel, editors: 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), Leibniz International Proceedings in Informatics (LIPIcs) 252, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 5:1–5:19, ...

    work page doi:10.4230/lipics.csl.2023.5 2023

  3. [3]

    In: Leonardis, A., Ricci, E., Roth, S., Russakovsky, O., Sattler, T., Varol, G

    B. Afshari, L. Grotenhuis G. E. Leigh & L. Zenger (2023): Ill-Founded Proof Systems for Intuitionistic Linear-Time Temporal Logic. In R. Ramanayake & J. Urban, editors: Automated Reasoning with Analytic Tableaux and Related Methods , Springer Nature Switzerland, Cham, pp. 223–241, doi:10.1007/978-3-031- 43513-3_13

    work page doi:10.1007/978-3-031- 2023

  4. [4]

    Akbar Tabatabai, R

    A. Akbar Tabatabai, R. Iemhoff & R. Jalali (2021): Uniform Lyndon Interpolation for Basic Non-normal Modal Logics. In A. Silva, R. Wassermann & R. de Queiroz, editors: Logic, Language, Information, and Computation, Springer, pp. 287–301, doi:10.1093/logcom/exae057

    work page doi:10.1093/logcom/exae057 2021

  5. [5]

    Baelde, A

    D. Baelde, A. Doumane & A. Saurin (2016): Infinitary Proof Theory: the Multiplicative Additive Case . In: Annual Conference for Computer Science Logic , pp. 42:1–42:17, doi:10.4230/LIPIcs.CSL.2016.42. Avail- able at https://api.semanticscholar.org/CorpusID:269432892

    work page doi:10.4230/lipics.csl.2016.42 2016

  6. [6]

    arXiv:2506.14307

    Justus Becker (2025): A Non-Wellfounded and Labelled Sequent Calculus for Bimodal Provability Logic . arXiv:2506.14307

    work page arXiv 2025

  7. [7]

    L. D. Beklemishev (1987): Normalization of deductions and interpolation for some logics of provability . Russian Math. Surveys 42(6), pp. 223–224, doi:10.1070/RM1987v042n06ABEH001496

    work page doi:10.1070/rm1987v042n06abeh001496 1987

  8. [8]

    Boolos (2008): On systems of modal logic with provability interpretations

    G. Boolos (2008): On systems of modal logic with provability interpretations . Theoria 46, pp. 7 – 18, doi:10.1111/j.1755-2567.1980.tb00686.x

    work page doi:10.1111/j.1755-2567.1980.tb00686.x 2008

  9. [9]

    Borzechowski, M

    M. Borzechowski, M. Gattinger, H. H. Hansen, R. Ramanayake, V . Trucco Dalmas & Y . Venema (2025): Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof. arXiv:2503.13276

    work page arXiv 2025

  10. [10]

    Brotherston & A

    J. Brotherston & A. Simpson (2007): Complete Sequent Calculi for Induction and Infinite De- scent. In: 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007) , pp. 51–62, doi:10.1109/LICS.2007.16

    work page doi:10.1109/lics.2007.16 2007

  11. [11]

    Bucheli, R

    S. Bucheli, R. Kuznets & T. Studer (2010):Two Ways to Common Knowledge. Electronic Notes in Theoretical Computer Science 262, pp. 83–98, doi:10.1016/j.entcs.2010.04.007. Proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009)

    work page doi:10.1016/j.entcs.2010.04.007 2010

  12. [12]

    A. Das & D. Pous (2018): Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices) . In D. R. Ghica & A. Jung, editors: 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, Birmingham, UK, September 4-7, 2018 , LIPIcs 119, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 19:1–19:18, doi:10.4230/LIPICS.CSL.2018.19

    work page doi:10.4230/lipics.csl.2018.19 2018

  13. [13]

    Horvat, B

    S. Horvat, B. Sierra Miranda & T. Studer (2025): Non-wellfounded Proof Theory for Interpretability Logic. In: Automated Reasoning with Analytic Tableaux and Related Methods: 34th International Conference, TABLEAUX 2025, Reykjavik, Iceland, September 27–29, 2025, Proceedings , Springer-Verlag, Berlin, Hei- delberg, p. 201–219, doi:10.1007/978-3-032-06085-3_11

    work page doi:10.1007/978-3-032-06085-3_11 2025

  14. [14]

    Horvat, B

    S. Horvat, B. Sierra Miranda & T. Studer (2025): Uniform interpolation for interpretability logic . arXiv:2511.01428

    work page arXiv 2025

  15. [15]

    Kloibhofer, V

    J. Kloibhofer, V . Trucco Dalmas & Y . Venema (2026): Interpolation for Converse PDL . In G. L. Pozzato & T. Uustalu, editors: Automated Reasoning with Analytic Tableaux and Related Methods , Springer Nature Switzerland, Cham, pp. 258–277, doi:10.1007/978-3-032-06085-3_14. 730 Uniform Lyndon Interpolation via Non-wellfounded Proofs

    work page doi:10.1007/978-3-032-06085-3_14 2026

  16. [16]

    Kokkinis & T

    I. Kokkinis & T. Studer (2016): Cyclic Proofs for Linear Temporal Logic, pp. 171–192. De Gruyter, Berlin, Boston, doi:10.1515/9781501502620-011

    work page doi:10.1515/9781501502620-011 2016

  17. [17]

    Kurahashi (2020): Uniform Lyndon interpolation property in propositional modal logics

    T. Kurahashi (2020): Uniform Lyndon interpolation property in propositional modal logics . Arch. Math. Log. 59(5-6), pp. 659–678, doi:10.1007/s00153-020-00713-y

    work page doi:10.1007/s00153-020-00713-y 2020

  18. [18]

    Kushida (2020): A Proof Theory for the Logic of Provability in True Arithmetic

    H. Kushida (2020): A Proof Theory for the Logic of Provability in True Arithmetic . Studia Logica 108, pp. 857–875, doi:10.1007/s11225-019-09891-0

    work page doi:10.1007/s11225-019-09891-0 2020

  19. [19]

    Lindström (2006): Note on Some Fixed Point Constructions in Provability Logic

    P. Lindström (2006): Note on Some Fixed Point Constructions in Provability Logic . J Philos Logic 35, pp. 225–230, doi:10.1007/s10992-005-9013-8

    work page doi:10.1007/s10992-005-9013-8 2006

  20. [20]

    Proof Theory for Bimodal Provability Logics

    Borja Sierra Miranda & Thomas Studer (2026): Proof Theory for Bimodal Provability Logics . arXiv:2605.12351

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  21. [21]

    Savateev & D

    Y . Savateev & D. Shamkanov (2021):Non-well-founded proofs for the Grzegorczyk modal logic. The Review of Symbolic Logic 14(1), p. 22–50, doi:10.1017/S1755020319000510

    work page doi:10.1017/s1755020319000510 2021

  22. [22]

    Shamkanov (2014): Circular proofs for the Gödel-Löb provability logic

    D. Shamkanov (2014): Circular proofs for the Gödel-Löb provability logic . Mathematical Notes 96, pp. 575–585, doi:10.1134/S0001434614090326

    work page doi:10.1134/s0001434614090326 2014

  23. [23]

    Sierra Miranda & T

    B. Sierra Miranda & T. Studer (in press): Cut elimination for the master modality . Journal of Symbolic Logic

  24. [24]

    Sierra Miranda, T

    B. Sierra Miranda, T. Studer & L. Zenger (2024): Coalgebraic Proof Translations for Non-Wellfounded Proofs. In A. Ciabattoni, D. Gabelaia & I. Sedlár, editors: Advances in Modal Logic 2024 , pp. 527–548

    2024

  25. [25]

    Smory ´nski (1985): Self-Reference and Modal Logic

    C. Smory ´nski (1985): Self-Reference and Modal Logic . Universitext, Springer New York, NY , doi:10.1007/978-1-4613-8601-8

    work page doi:10.1007/978-1-4613-8601-8 1985

  26. [26]

    R. M. Solovay (1976): Provability interpretations of modal logic . Israel Journal of Mathematics 25, pp. 287–304, doi:10.1007/BF02757006

    work page doi:10.1007/bf02757006 1976