Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic

Bahareh Afshari, Johannes Kloibhofer

TL;DR

This paper advances cut-elimination for cyclic proofs in a temporal logic fragment by presenting a direct, syntactic procedure for the cyclic sequent calculus $\mathsf{GKe}$ applied to $\mathsf{MLe}$, which includes the eventuality operator $\mathsf{F}$. It distinguishes important and unimportant cuts and introduces a rank-based, traversed-proof methodology combined with discharge-token mechanisms to ensure a cut-free cyclic proof is produced without resorting to infinitary regularisation. The main technical contributions are the graph-theoretic preliminaries, the notion of minimally focused proofs, and the inductive reduction on cut-rank that systematically eliminates cuts while preserving the global validity condition. This approach lays groundwork for applying direct cut-elimination to richer modal-fixpoint logics and related cyclic calculi such as $\mathsf{PDL}$ and alternation-free $\mu$-calculus, potentially improving automation and proof-search in cyclic systems.

Abstract

We consider modal logic extended with the well-known temporal operator 'eventually' and provide a cut-elimination procedure for a cyclic sequent calculus that captures this fragment. The work showcases an adaptation of the reductive cut-elimination method to cyclic calculi. Notably, the proposed algorithm applies to a cyclic proof and directly outputs a cyclic cut-free proof without appealing to intermediate machinery for regularising the end proof.

Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic

TL;DR

This paper advances cut-elimination for cyclic proofs in a temporal logic fragment by presenting a direct, syntactic procedure for the cyclic sequent calculus applied to , which includes the eventuality operator . It distinguishes important and unimportant cuts and introduces a rank-based, traversed-proof methodology combined with discharge-token mechanisms to ensure a cut-free cyclic proof is produced without resorting to infinitary regularisation. The main technical contributions are the graph-theoretic preliminaries, the notion of minimally focused proofs, and the inductive reduction on cut-rank that systematically eliminates cuts while preserving the global validity condition. This approach lays groundwork for applying direct cut-elimination to richer modal-fixpoint logics and related cyclic calculi such as and alternation-free -calculus, potentially improving automation and proof-search in cyclic systems.

Abstract

We consider modal logic extended with the well-known temporal operator 'eventually' and provide a cut-elimination procedure for a cyclic sequent calculus that captures this fragment. The work showcases an adaptation of the reductive cut-elimination method to cyclic calculi. Notably, the proposed algorithm applies to a cyclic proof and directly outputs a cyclic cut-free proof without appealing to intermediate machinery for regularising the end proof.
Paper Structure (14 sections, 11 theorems, 34 equations, 1 figure)

This paper contains 14 sections, 11 theorems, 34 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Modal Logic with Eventuality
  3. Cut Elimination
  4. Preliminary definitions
  5. Important cut
  6. Unimportant cuts
  7. Main theorem
  8. Conclusion
  9. Appendix: Cut Reductions
  10. Principal cut reductions
  11. Trivial principal cut reductions
  12. Cut reductions for $\mathsf{D}^{}$ , $\mathsf{u}$ and $\mathsf{f}$
  13. Non-principal cut-reductions for a rule $\mathsf{R}\xspace$ different from $\mathsf{{ \hbox{origin=c]{45}{$\square$}}}}$, $\mathsf{u}$, $\mathsf{f}$ and $\mathsf{D}^{}$
  14. Appendix: Important Cuts

Key Result

Lemma 4

If $v$ is a discharged leaf in a $\mathsf{GKe}$ proof, then there is a node labelled by $\mathsf{{ \hbox{origin=c]{45}{$\square$}}}}$ on $\tau_v$.

Figures (1)

  • Figure 1: Rules of $\mathsf{GKe}$

Theorems & Definitions (30)

  • Definition 1: Derivation
  • Definition 2: Successful path
  • Definition 3: Proof
  • Lemma 4
  • Theorem 5: Soundness and Completeness
  • Definition 6: Important cut
  • Definition 7: Cut rank
  • Lemma 8
  • Definition 9: Subproof
  • Definition 10: Critical cut
  • ...and 20 more