pith. sign in

arxiv: 1907.01270 · v1 · pith:TKNWPD6Ynew · submitted 2019-07-02 · 💻 cs.LO

Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)

Rajeev Gor\'e , Bj\"orn Lellmann This is my paper

Pith reviewed 2026-05-25 10:52 UTC · model grok-4.3

classification 💻 cs.LO
keywords tense logicKtlinear nested sequentscut-eliminationbackward proof-searchmodal logicKBcountermodel construction
0
0 comments X

The pith

A linear nested sequent calculus for basic tense logic Kt supports syntactic cut-elimination, backward proof-search, and counter-model construction.

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

The paper presents a sequent system with linear nesting for the tense logic Kt. It proves that this system admits syntactic cut-elimination and permits proof search that proceeds from the goal formula backward. Failed searches yield counter-models, and the same system supplies a cut-free calculus for the symmetric modal logic KB. Linear nesting is claimed to be the least structure needed to handle modalities and their converses together. A sympathetic reader would care because these features give a uniform, syntax-driven way to decide validity in logics that include both forward and backward modalities.

Core claim

The authors construct a linear nested sequent calculus for Kt whose rules are sound and complete for the standard Kripke semantics. They then prove that every derivation admits a cut-free form obtained by a purely syntactic procedure that does not rely on semantic arguments or on restrictions on nesting depth. The same calculus yields decision procedures via backward search and extracts countermodels from open branches. The construction also yields a cut-free system for KB as a special case.

What carries the argument

Linear nested sequents: sequents whose components are arranged in a single linear chain of nesting, supplying exactly the structure required to internalise both a modality and its converse.

If this is right

  • Backward search in the calculus terminates and decides Kt validity.
  • Every open branch in a failed search produces a finite countermodel for the end-sequent.
  • The same rules give a cut-free calculus for the symmetric modal logic KB.
  • No deeper nesting is required to treat converse modalities.

Where Pith is reading between the lines

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

  • The result suggests that any proof system for logics with converse must at least allow linear nesting if it is to remain cut-free.
  • The method may extend to other normal tense logics whose axioms can be expressed by similar linear rules.
  • Complexity bounds for proof search in Kt might be read off directly from the depth of the linear nesting used in derivations.

Load-bearing premise

The specific rules chosen for the linear nested sequent calculus correctly capture the semantics of Kt, so that soundness, completeness, and the cut-elimination argument hold without hidden limits on nesting or rule use.

What would settle it

A Kt-valid formula whose shortest linear nested sequent derivation requires an application of the cut rule that cannot be eliminated by the given syntactic procedure.

Figures

Figures reproduced from arXiv: 1907.01270 by Bj\"orn Lellmann, Rajeev Gor\'e.

Figure 1
Figure 1. Figure 1: The system LNSKt where l stands for either ր or ւ and (A → B) → (A → B), the necessitation rules Nec : A/A and Nec : A/A, and the two interaction axioms ♦p → p and p → p. The system HKt is sound and complete w.r.t. the Kripke semantics. 3 A Linear Nested Sequent Calculus for Kt Unlike standard Hilbert-calculi, our calculus operates on linear nested sequents instead of formulae, defined and adapted f… view at source ↗
Figure 3
Figure 3. Figure 3: Note that only the component which is not restarted survive [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 2
Figure 2. Figure 2: 5 Completeness via Cut elimination We now provide an alternative proof of cut-free completeness of our calculus via syntactic cut elimination. The proof is interesting from a technical point of view: The additional left premiss in the rules 1 R and 1 R is introduced specifically as a counterpart to the restart rules 2 L and 2 L to facilitate the reduction of cuts on boxed formulae to cuts of smaller comp… view at source ↗
Figure 3
Figure 3. Figure 3: Definition 15. The merge of two linear nested sequents is defined via the fol￾lowing, where we assume G, H to be nonempty: (Γ ⇒ ∆) ⊕ (Σ ⇒ Π) := Γ, Σ ⇒ ∆, Π (Γ ⇒ ∆) ⊕ (Σ ⇒ Π l H) := Γ, Σ ⇒ ∆, Π l H (Γ ⇒ ∆ l H) ⊕ (Σ ⇒ Π) := Γ, Σ ⇒ ∆, Π l H (Γ ⇒ ∆ ր G) ⊕ (Σ ⇒ Π ր H) := Γ, Σ ⇒ ∆, Π ր (G ⊕ H) (Γ ⇒ ∆ ւ G) ⊕ (Σ ⇒ Π ւ H) := Γ, Σ ⇒ ∆, Π ւ (G ⊕ H) . Hence the merge is only defined for linear nested sequents which ar… view at source ↗
read the original abstract

We give a linear nested sequent calculus for the basic normal tense logic Kt. We show that the calculus enables backwards proof-search, counter-model construction and syntactic cut-elimination. Linear nested sequents thus provide the minimal amount of nesting necessary to provide an adequate proof-theory for modal logics containing converse. As a bonus, this yields a cut-free calculus for symmetric modal logic KB.

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

1 major / 2 minor

Summary. The paper presents a linear nested sequent calculus for the basic normal tense logic Kt. It establishes soundness and completeness with respect to Kripke semantics with converse accessibility, demonstrates that the calculus supports backward proof search and counter-model construction from failed searches, and gives a syntactic cut-elimination proof. The authors conclude that linear nesting is the minimal structure needed for an adequate proof theory of modal logics containing converse modalities and obtain a cut-free calculus for KB as a corollary.

Significance. If the semantic correspondence and cut-elimination argument hold, the result is significant: it supplies a proof-theoretic framework for tense logics that avoids the full nesting of standard nested sequents while still handling converse, and the syntactic cut-elimination plus explicit backward-search procedure are concrete strengths. The work directly addresses the minimal-nesting claim for logics with converse.

major comments (1)
  1. [§4.2, Theorem 4.3] §4.2, Theorem 4.3 (cut-elimination): the inductive argument on formula complexity and nesting depth appears to handle arbitrary linear nesting, but the case for the converse rules (L◇ and R□) requires an explicit check that the linear nesting depth does not increase under reduction; if this is only sketched, the claim that the procedure works without hidden restrictions on nesting would need a fuller case analysis.
minor comments (2)
  1. [§2.1] §2.1: the definition of linear nested sequents would benefit from an explicit inductive clause showing that nesting is strictly linear (no branching) rather than left implicit in the examples.
  2. [Table 1] Table 1 (rule set): the side condition on the eigenvariable in the right rule for the past modality is stated only in prose; adding it formally to the rule schema would improve readability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive evaluation and recommendation for minor revision. We address the single major comment below.

read point-by-point responses

  1. Referee: [§4.2, Theorem 4.3] §4.2, Theorem 4.3 (cut-elimination): the inductive argument on formula complexity and nesting depth appears to handle arbitrary linear nesting, but the case for the converse rules (L◇ and R□) requires an explicit check that the linear nesting depth does not increase under reduction; if this is only sketched, the claim that the procedure works without hidden restrictions on nesting would need a fuller case analysis.

    Authors: We agree that an explicit verification for the converse rules would improve clarity. In the revised manuscript we will expand the case analysis within the inductive argument of Theorem 4.3 to explicitly confirm that reductions involving L◇ and R□ preserve or decrease linear nesting depth, thereby removing any ambiguity about hidden restrictions. revision: yes

Circularity Check

0 steps flagged

No circularity; standard independent proof-theoretic construction.

full rationale

The paper defines a linear nested sequent calculus for Kt from scratch and then establishes its soundness, completeness, backward proof-search, counter-model construction, and syntactic cut-elimination via explicit inductive arguments on the rules and derivations. These steps are developed internally without any quoted reduction of a claimed result to a fitted parameter, self-definition, or load-bearing self-citation chain. The abstract and description present the calculus as a new object whose adequacy is verified directly rather than presupposed by construction or prior author work invoked as an unverified uniqueness theorem. This is the normal case of a self-contained sequent-calculus paper.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only the abstract is available; no specific free parameters, axioms, or invented entities can be identified from the given text.

pith-pipeline@v0.9.0 · 5590 in / 1161 out tokens · 25082 ms · 2026-05-25T10:52:51.597182+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

21 extracted references · 21 canonical work pages

  1. [1]

    In: Australian Joint Conference on Artificial Intelligence

    Bonnette, N., Gor´ e, R.: A labelled sequent system for ten se logic K t. In: Australian Joint Conference on Artificial Intelligence. Lecture Notes in Computer Science, vol. 1502, pp. 71–82. Springer (1998)

    work page 1998

  2. [2]

    Br¨ unnler, K.: Deep sequent systems for modal logic. Arch . Math. Log. 48, 551–577 (2009)

    work page 2009

  3. [3]

    Commu- nications of the ACM 22(8), 465–476 (1979)

    Dershowitz, N., Manna, Z.: Proving termination with mult iset orderings. Commu- nications of the ACM 22(8), 465–476 (1979)

    work page 1979

  4. [4]

    In: Handbook of Tableau Methods

    Gor´ e, R.: Tableau methods for modal and temporal logics. In: Handbook of Tableau Methods. Kluwer (1999)

    work page 1999

  5. [5]

    Logical Meth- ods in Computer Science 7(2) (2011)

    Gor´ e, R., Postniece, L., Tiu, A.: On the correspondence b etween display postu- lates and deep inference in nested sequent calculi for tense logics. Logical Meth- ods in Computer Science 7(2) (2011). https://doi.org/10.2168/LMCS-7(2:8)2011, https://doi.org/10.2168/LMCS-7(2:8)2011

    work page doi:10.2168/lmcs-7(2:8)2011 2011

  6. [6]

    In: Automated Reasoning with Analytic Tableaux and Related Met hods, 18th Interna- tional Conference, TABLEAUX 2009, Oslo, Norway, July 6-10, 2009

    Gor´ e, R., Widmann, F.: Sound global state caching for ALC with inverse roles. In: Automated Reasoning with Analytic Tableaux and Related Met hods, 18th Interna- tional Conference, TABLEAUX 2009, Oslo, Norway, July 6-10, 2009. Proceedings. pp. 205–219 (2009)

    work page 2009

  7. [7]

    In: CADE

    Horrocks, I., Sattler, U., Tobies, S.: Reasoning with ind ividuals for the description logic SHIQ. In: CADE. Lecture Notes in Computer Science, vol . 1831, pp. 482–496. Springer (2000)

    work page 2000

  8. [8]

    Bulletin of Symbolic Logic 22, 121–144 (2016)

    Indrzejczak, A.: Linear time in hypersequent framework. Bulletin of Symbolic Logic 22, 121–144 (2016)

    work page 2016

  9. [9]

    Studia Logica 53(1), 119–136 (1994)

    Kashima, R.: Cut-free sequent calculi for some tense logi cs. Studia Logica 53(1), 119–136 (1994)

    work page 1994

  10. [10]

    In: Bezhanishvili, G., D’Agostino , G., Metcalfe, G., Studer, T

    Kuznets, R., Lellmann, B.: Interpolation for intermedi ate logics via hyper- and linear nested sequents. In: Bezhanishvili, G., D’Agostino , G., Metcalfe, G., Studer, T. (eds.) Advances in Modal Logic 2018, pp. 473–492. College Publications (2018)

    work page 2018

  11. [11]

    In: 28th Annual ACM/IEEE Symposium on Logic in Computer Scie nce, LICS 2013, New Orleans, LA, USA, June 25-28, 2013

    Lahav, O.: From frame properties to hypersequent rules i n modal logics. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Scie nce, LICS 2013, New Orleans, LA, USA, June 25-28, 2013. pp. 408–41 7 (2013). https://doi.org/10.1109/LICS.2013.47, https://doi.org/10.1109/LICS.2013.47

    work page doi:10.1109/lics.2013.47 2013

  12. [12]

    In: De Nivelle, H

    Lellmann, B.: Linear nested sequents, 2-sequents and hy persequents. In: De Nivelle, H. (ed.) TABLEAUX 2015, Lecture Notes in Computer Science, v ol. 9323, pp. 135–

    work page 2015

  13. [13]

    Springer International Publishing (2015)

    work page 2015

  14. [14]

    ACM Trans

    Lellmann, B., Pimentel, E.: Modularisation of sequent c alculi for normal and non- normal modalities. ACM Trans. Comput. Logic 20(2), 7:1–7:46 (2019)

    work page 2019

  15. [15]

    Masini, A.: 2-sequent calculus: a proof theory of modali ties. Ann. Pure Applied Logic 58, 229–246 (1992)

    work page 1992

  16. [16]

    Osaka Mathe- matical Journal 9, 113–130 (1957)

    Ohnishi, M., Matsumoto, K.: Gentzen method in modal calc uli I. Osaka Mathe- matical Journal 9, 113–130 (1957)

    work page 1957

  17. [17]

    Parisi, A.: Second-Order Modal Logic. Ph.D. thesis, Uni versity of Connecticut (2017)

    work page 2017

  18. [18]

    Poggiolesi, F.: Gentzen Calculi for Modal Propositiona l Logic, Trends In Logic, vol. 32. Springer-Verlag Berlin Heidelberg (2010)

    work page 2010

  19. [19]

    Bulletin of the Section of Logic Volume 13/2, 7583 (1984)

    Trzesicki, K.: Gentzen-style axiomatization of tense l ogic. Bulletin of the Section of Logic Volume 13/2, 7583 (1984)

    work page 1984

  20. [20]

    Wansing, H.: Sequent calculi for normal modal proposisi onal logics. J. Log. Com- put. 4(2), 125–142 (1994) 18 Rajeev Gor´ e and Bj¨ orn Lellmann A Additional Proofs Lemma 16. The following statements hold for every n, m : (SR□(n, m )) Suppose that all of the following hold: –D1⊢Gր Γ ⇒ ∆, □A with □A principal in the last rule in D1 –D2⊢Hր □A, Σ ⇒ Π ↕I – d...

    work page 1994

  21. [21]

    If the occurrence of A is in the last component, the derivation D1 ends in D′ 1

    to the premiss of the application of EW, followed by the same rule. If the occurrence of A is in the last component, the derivation D1 ends in D′ 1. . . . G G↕ Γ ⇒ ∆, A EW We replace this application of EW with D′ 1. . . . G G↕ Γ, Σ ⇒ ∆, Π EW and then admissibility of weakening yields the desired result. Case: Last rule inD1 is (id) or⊥ L. In this case th...

    work page