pith. sign in

arxiv: 2606.03413 · v1 · pith:VM3M2PE4new · submitted 2026-06-02 · 💻 cs.LO · math.LO

Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents

Tim S. Lyon , Lukas Zenger This is my paper

Pith reviewed 2026-06-28 07:59 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords linear temporal logicnon-wellfounded proofscyclic proofslinear nested sequentscycle recognitionunravelingsaturation recurrence
0
0 comments X

The pith

Non-wellfounded LTL proofs in linear nested sequents normalize to a saturation-recurrence form that yields cyclic proofs.

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

The paper builds non-wellfounded and cyclic proof calculi for linear temporal logic inside the linear nested sequent framework. It solves cycle recognition by proving that every non-wellfounded proof can be normalized to a special form whose repeated saturation points allow direct extraction of a corresponding cyclic proof. It solves the reverse problem of unraveling by defining a forward-shifting operation that moves rule applications along the nested structure while preserving derivability. These steps establish a syntactic back-and-forth correspondence between the two proof styles. The techniques matter because standard Gentzen methods for handling cycles do not scale directly to the richer linear nested sequent setting used for temporal reasoning.

Core claim

Non-wellfounded linear nested sequent proofs for LTL are complete relative to a normal form that exhibits saturation recurrence; this normal form permits systematic extraction of cyclic proofs, while a dedicated forward-shifting procedure on rule applications reconstructs non-wellfounded proofs from cyclic ones, yielding a syntactic correspondence between the two notions of proof.

What carries the argument

Saturation recurrence: a property of normalized non-wellfounded linear nested sequent derivations that marks repeated saturation points and thereby enables systematic extraction of cycles.

If this is right

  • Every valid LTL sequent possesses a non-wellfounded linear nested sequent proof that can be brought into saturation-recurrence normal form.
  • Cyclic linear nested sequent proofs for LTL can be read off directly from the normalized non-wellfounded derivations.
  • The forward-shifting procedure converts any cyclic proof back into a non-wellfounded one without changing its validity status.
  • The same cycle-recognition and unraveling methods apply to any expressive multisequent calculus that supports linear nesting.

Where Pith is reading between the lines

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

  • The normalization and shifting techniques may extend to other modal or temporal logics once their linear nested sequent rules are fixed.
  • Automated proof search could alternate between the cyclic and non-wellfounded representations using the correspondence as a bridge.
  • If saturation recurrence can be decided algorithmically, it would give a decision procedure for the existence of cyclic proofs in this setting.

Load-bearing premise

Every valid non-wellfounded linear nested sequent proof for LTL admits a normalization that produces saturation recurrence, and the forward-shifting procedure never adds or removes derivability.

What would settle it

An LTL formula that possesses a valid non-wellfounded linear nested sequent proof yet cannot be normalized to any derivation exhibiting saturation recurrence, or for which the shifting procedure produces an invalid result.

Figures

Figures reproduced from arXiv: 2606.03413 by Lukas Zenger, Tim S. Lyon.

Figure 1
Figure 1. Figure 1: The set of rules LNSLTL. An index set is a set I ⊆ N such that (1) 0 ∈ I and (2) if n+1 ∈ I, then n ∈ I. We use index sets to define certain kinds of (potentially infinite) sequences below. A path in a derivation π is a (potentially infinite) sequence P = {Gi}i∈I of LNSs such that for each i the LNS Gi is the parent of Gi+1 (if it exists). A branch in a derivation π is a maximal path B = {Gi}i∈I of LNSs su… view at source ↗
Figure 2
Figure 2. Figure 2: Example of a cyclic proof. since their interior components are free of complex formulae (meaning, no rules are bottom-up applicable to these components), two saturated sequents with matching end components represent identical ‘states’ in a proof, making them natural candidates for the endpoints of a cycle. This serves as the motivation for our notion of cyclic proof given below. We define a tuple (π,L,c) t… view at source ↗
Figure 3
Figure 3. Figure 3: Shifting lemma example. We obtain the completeness of the cyclic LNS system as a corollary of Theorems 4.7 and 5.3. Corollary 5.4 (Completeness of LNScyc LTL). If G is valid, then G has an LNScyc LTL-proof. 5.2 From Cyclic Proofs to Non-Wellfounded Proofs In this section, we prove the soundness of cyclic proofs by means of a proof transformation. We introduce a technique for unraveling cyclic linear nested… view at source ↗
read the original abstract

We introduce and investigate non-wellfounded and cyclic linear nested sequent calculi, and, as a case study, develop such systems for linear temporal logic (LTL). The paper addresses two central problems, which we call 'cycle recognition' and 'unraveling.' Cycle recognition concerns identifying cycles in non-wellfounded proofs in order to extract corresponding cyclic proofs, while unraveling studies the converse transformation, from cyclic proofs to non-wellfounded ones. Although these processes are well understood for Gentzen sequents, they have received little attention for more expressive sequent formalisms and become more challenging in the linear nested sequent setting. To address cycle recognition, we show the completeness of non-wellfounded proofs relative to a particular normal form exhibiting a property we call 'saturation recurrence,' which enables the systematic extraction of cyclic proofs. To address unraveling, we introduce a specialized procedure that shifts rule applications forward along linear nested sequents, allowing non-wellfounded proofs to be reconstructed from cyclic ones. Overall, our work provides new proof-theoretic techniques for cycle recognition and unraveling in expressive multisequent formalisms.

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 paper introduces non-wellfounded and cyclic linear nested sequent calculi for LTL. It addresses cycle recognition by proving completeness of non-wellfounded proofs relative to a saturation-recurrence normal form that permits systematic extraction of cyclic proofs, and addresses unraveling by defining a forward-shifting procedure that reconstructs non-wellfounded proofs from cyclic ones along linear nested sequents.

Significance. If the syntactic correspondence holds, the work supplies explicit, constructive procedures that extend Gentzen-style cycle recognition and unraveling results to linear nested sequents. This is a targeted advance in proof theory for temporal logics, providing new tools for handling non-wellfounded and cyclic derivations in a more expressive formalism.

minor comments (3)
  1. [§3] §3 (or the section defining the linear nested sequent calculus): the notation for nested sequents and the precise statement of the saturation recurrence property would benefit from an additional worked example involving nested Until formulas to illustrate the normal-form condition.
  2. [§5] The forward-shifting procedure (likely §5): while the high-level description is clear, the preservation argument for derivability under shifting would be easier to follow if the inductive cases were enumerated explicitly rather than summarized.
  3. References: the manuscript cites prior Gentzen results but should add a pointer to any existing work on cyclic proofs in nested sequents for other modal or temporal logics to better situate the novelty.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our paper and the recommendation of minor revision. The referee's description accurately reflects our contributions on cycle recognition via saturation recurrence and the unraveling shift procedure for linear nested sequents in LTL.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper presents explicit syntactic procedures for normalizing non-wellfounded linear nested sequent proofs to a saturation-recurrence form and for forward-shifting rule applications to reconstruct non-wellfounded proofs from cyclic ones. These constructions are described as operating directly on the sequent structures and rule applications without reducing the claimed completeness or correspondence to quantities defined from the target result itself. Prior Gentzen-style results are invoked as external foundations rather than as self-citations that bear the load of the central claims. No self-definitional equations, fitted inputs renamed as predictions, or ansatzes smuggled via citation appear in the abstract or argument structure.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

No free parameters, invented entities, or ad-hoc axioms are mentioned; the work relies on standard background assumptions of LTL semantics and sequent calculus.

axioms (1)
  • domain assumption Standard sequent rules and LTL semantics are taken as given from prior literature.
    The paper positions its contributions as extensions of known Gentzen techniques to linear nested sequents.

pith-pipeline@v0.9.1-grok · 5736 in / 1180 out tokens · 19718 ms · 2026-06-28T07:59:10.678048+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

29 extracted references · 11 canonical work pages

  1. [1]

    Leigh & Lukas Zenger (2023):Ill-Founded Proof Systems for Intuitionistic Linear-Time Temporal Logic

    Bahareh Afshari, Lide Grotenhuis, Graham E. Leigh & Lukas Zenger (2023):Ill-Founded Proof Systems for Intuitionistic Linear-Time Temporal Logic. In:Automated Reasoning with Analytic Tableaux and Related Methods, 14278, pp. 223–241

    2023

  2. [2]

    Leigh (2017):Cut-free completeness for modal mu-calculus

    Bahareh Afshari & Graham E. Leigh (2017):Cut-free completeness for modal mu-calculus. In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 1–12, doi:10.1109/LICS.2017.8005088

    work page doi:10.1109/lics.2017.8005088 2017

  3. [3]

    Leigh (2022):Lyndon Interpolation for Modalµ-Calculus

    Bahareh Afshari & Graham E. Leigh (2022):Lyndon Interpolation for Modalµ-Calculus. In Aybüke Özgün & Yulia Zinova, editors:Language, Logic, and Computation, Springer International Publishing, Cham, pp. 197–213

    2022

  4. [4]

    Aguilera & Leonardo Pacheco (2025):Intuitionistic Gödel-Löb without Sharps.ACM Trans

    Juan P. Aguilera & Leonardo Pacheco (2025):Intuitionistic Gödel-Löb without Sharps.ACM Trans. Comput. Logic26(4), doi:10.1145/3748649. Available athttps://doi.org/10.1145/3748649

    work page doi:10.1145/3748649 2025

  5. [5]

    Alonderis, R

    R. Alonderis, R. Pliuškevi ˇcius, A. Pliuškeviˇcien˙e & H. Giedra (2020):Loop-Type Sequent Calculi for Tem- poral Logic.Journal of Automated Reasoning64(8), pp. 1663–1684, doi:10.1007/s10817-020-09544-1. Available athttps://doi.org/10.1007/s10817-020-09544-1

    work page doi:10.1007/s10817-020-09544-1 2020

  6. [6]

    In Wilfrid Hodges, Martin Hyland, Charles Steinhorn & John Truss, editors:Logic: From Foundations to Applications: European Logic Colloquium, Clarendon Press, USA, p

    Arnon Avron (1996):The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Log- ics. In Wilfrid Hodges, Martin Hyland, Charles Steinhorn & John Truss, editors:Logic: From Foundations to Applications: European Logic Colloquium, Clarendon Press, USA, p. 1–32

    1996

  7. [7]

    Bianca Boretti (2008):Proof Analysis in Temporal Logic. Ph.D. thesis, University of Milan

    2008

  8. [8]

    Kai Brünnler (2009):Deep sequent systems for modal logic.Arch. Math. Log.48(6), pp. 551–577, doi:10.1007/s00153-009-0137-3. Available athttps://doi.org/10.1007/s00153-009-0137-3

    work page doi:10.1007/s00153-009-0137-3 2009

  9. [9]

    216–225, doi:https://doi.org/10.1016/j.jlap.2008.02.004

    Kai Brünnler & Martin Lange (2008):Cut-free sequent systems for temporal logic.The Journal of Logic and Algebraic Programming76(2), pp. 216–225, doi:https://doi.org/10.1016/j.jlap.2008.02.004. Available athttps://www.sciencedirect.com/science/article/pii/S1567832608000167. Logic and Infor- mation: From Logic to Constructive Reasoning

    work page doi:10.1016/j.jlap.2008.02.004 2008

  10. [10]

    Anupam Das, Iris van der Giessen & Sonia Marin (2024):Intuitionistic Gödel-Löb Logic, à la Simp- son: Labelled Systems and Birelational Semantics. In Aniello Murano & Alexandra Silva, editors:32nd EACSL Annual Conference on Computer Science Logic (CSL 2024),Leibniz International Proceedings in Informatics (LIPIcs)288, Schloss Dagstuhl – Leibniz-Zentrum fü...

    work page doi:10.4230/lipics.csl.2024.22 2024

  11. [11]

    Journal of Automated Reasoning67(3), p

    Anupam Das & Marianna Girlando (2023):Cyclic Hypersequent System for Transitive Closure Logic. Journal of Automated Reasoning67(3), p. 27, doi:10.1007/s10817-023-09675-1. Available athttps: //doi.org/10.1007/s10817-023-09675-1

    work page doi:10.1007/s10817-023-09675-1 2023

  12. [12]

    Simon Docherty & Reuben N. S. Rowe (2019):A Non-wellfounded, Labelled Proof System for Proposi- tional Dynamic Logic. In Serenella Cerrito & Andrei Popescu, editors:Automated Reasoning with Analytic Tableaux and Related Methods, Springer International Publishing, Cham, pp. 335–352

    2019

  13. [13]

    Jérôme Fortier & Luigi Santocanale (2013):Cuts for circular proofs: semantics and cut-elimination. In Simona Ronchi Della Rocca, editor:Computer Science Logic 2013 (CSL 2013),Leibniz International Pro- ceedings in Informatics (LIPIcs)23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 248–262, doi:10.4230/LIPIcs.CSL.2013.248. Ava...

    work page doi:10.4230/lipics.csl.2013.248 2013

  14. [14]

    Ioannis Kokkinis & Thomas Studer (2016):Cyclic proofs for linear temporal logic.Concepts of Proof in Mathematics, Philosophy, and Computer Science6, p. 171

    2016

  15. [15]

    In Hans De Nivelle, editor: Automated Reasoning with Analytic Tableaux and Related Methods,Lecture Notes in Computer Science 9323, Springer, Cham, pp

    Björn Lellmann (2015):Linear Nested Sequents, 2-Sequents and Hypersequents. In Hans De Nivelle, editor: Automated Reasoning with Analytic Tableaux and Related Methods,Lecture Notes in Computer Science 9323, Springer, Cham, pp. 135–150. 16Non-Wellfounded and Cyclic Proofs for LTL

    2015

  16. [16]

    Tim S. Lyon, Agata Ciabattoni, Didier Galmiche, Marianna Girlando, Dominique Larchey-Wendling, Daniel Méry, Nicola Olivetti & Revantha Ramanayake (2025):Internal and External Calculi: Ordering the Jungle without Being Lost in Translations.Bulletin of the Section of Logic54(1), p. 59–151, doi:10.18778/0138- 0680.2025.02. Available athttps://czasopisma.uni....

    work page doi:10.18778/0138- 2025

  17. [17]

    Andrea Masini (1992):2-sequent calculus: A proof theory of modalities.Annals of Pure and Applied Logic 58(3), pp. 229–246

    1992

  18. [18]

    Andrea Masini (1993):2-sequent calculus: Intuitionism and natural deduction.Journal of Logic and Com- putation3(5), pp. 533–562

    1993

  19. [19]

    Guillermo Menéndez Turata (2024):Cyclic proof systems for modal fixpoint logics. Ph.D. thesis, Universiteit van Amsterdam

    2024

  20. [20]

    G. E. Mints (1978):Finite investigations of transfinite derivations.Journal of Soviet Mathematics10(4), pp. 548–596, doi:10.1007/BF01091743. Available athttps://doi.org/10.1007/BF01091743

    work page doi:10.1007/bf01091743 1978

  21. [21]

    In Egon Börger, Hans Kleine Büning & Michael M

    Barbara Paech (1989):Gentzen-Systems for propositional temporal logics. In Egon Börger, Hans Kleine Büning & Michael M. Richter, editors:CSL ’88, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 240– 253

    1989

  22. [22]

    The temporal logic of programs

    Amir Pnueli (1977):The Temporal Logic of Programs. In:18th Annual Symposium on Foundations of Computer Science, pp. 46–57, doi:10.1109/SFCS.1977.32

    work page doi:10.1109/sfcs.1977.32 1977

  23. [23]

    Garrel Pottinger (1983):Uniform, cut-free formulations of T, S4 and S5.Journal of Symbolic Logic48(3), p. 900

    1983

  24. [24]

    In Anupam Das & Sara Negri, editors:Automated Reasoning with Analytic Tableaux and Related Methods, Springer International Publishing, Cham, pp

    Jan Rooduijn (2021):Cyclic Hypersequent Calculi for Some Modal Logics with the Master Modality. In Anupam Das & Sara Negri, editors:Automated Reasoning with Analytic Tableaux and Related Methods, Springer International Publishing, Cham, pp. 354–370

    2021

  25. [25]

    Jan Rooduijn (2024):Fragments and frame classes: Towards a uniform proof theory for modal fixed point logics. Ph.D. thesis, Universiteit van Amsterdam

    2024

  26. [26]

    Jan Rooduijn & Lukas Zenger (2022):An analytic proof system for common knowledge logic over S5.In David Fernández-Duque, Alessandra Palmigiano & Sophie Pinchinat, editors:Advances in Modal Logic 14, College Publications

    2022

  27. [27]

    D. S. Shamkanov (2014):Circular proofs for the Gödel-Löb provability logic.Mathematical Notes96(3), pp. 575–585

    2014

  28. [28]

    Alex K Simpson (1994):The proof theory and semantics of intuitionistic modal logic. Ph.D. thesis, University of Edinburgh. College of Science and Engineering. School of Informatics

    1994

  29. [29]

    Springer Science & Business Media

    Luca Viganò (2000):Labelled Non-Classical Logics. Springer Science & Business Media

    2000