Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Cut elimination for a non-wellfounded system for the master modality

Borja Sierra Miranda, Thomas Studer

TL;DR

The paper addresses syntactic cut elimination for a non-wellfounded sequent calculus of the master modality, $K^+$, where standard height-based recursion is unavailable. It replaces ultrametric-space techniques with a partition-based corecursive framework, defining an ordinal-indexed local-progress system $\alpha\text{-G}^{\infty}_{\ell}K^{+}_{s}$ and employing proofs-with-witnesses to manage infinite branches via focus annotations. The authors develop a two-stage cut-pushing method (to the main local fragment and then to witnesses) and prove cut admissibility in a stratified sequence (atomic, Box formulas, master formula, general case), culminating in full cut elimination for $G^{\infty}_{\ell}K^{+}_{s}$. This yields syntactic cut elimination for $K^+$ and demonstrates a scalable approach for non-wellfounded logics with a master modality, with potential applicability to related systems like common knowledge and modal mu-calculus frameworks. The method leverages only basic structural proof-theoretic tools and corecursion, offering a flexible path toward understanding recursive-corecursive interactions in non-wellfounded proofs.

Abstract

In previous work we provided a method for eliminating cuts in non-wellfounded proofs with a local-progress condition, these being the simplest kind of non-wellfounded proofs. The method consisted of splitting the proof into nicely behaved fragments. This paper extends our method to proofs based on simple trace conditions. The main idea is to split the system with the trace condition into infinitely many local-progress calculi that together are equivalent to the original trace-based system. This provides a cut elimination method using only basic tools of structural proof theory and corecursion, which is needed due to the non-wellfounded character of proofs. We will employ the method to obtain syntactic cut elimination for $K^+$, a system of modal logic with the master modality.

Cut elimination for a non-wellfounded system for the master modality

TL;DR

The paper addresses syntactic cut elimination for a non-wellfounded sequent calculus of the master modality, , where standard height-based recursion is unavailable. It replaces ultrametric-space techniques with a partition-based corecursive framework, defining an ordinal-indexed local-progress system and employing proofs-with-witnesses to manage infinite branches via focus annotations. The authors develop a two-stage cut-pushing method (to the main local fragment and then to witnesses) and prove cut admissibility in a stratified sequence (atomic, Box formulas, master formula, general case), culminating in full cut elimination for . This yields syntactic cut elimination for and demonstrates a scalable approach for non-wellfounded logics with a master modality, with potential applicability to related systems like common knowledge and modal mu-calculus frameworks. The method leverages only basic structural proof-theoretic tools and corecursion, offering a flexible path toward understanding recursive-corecursive interactions in non-wellfounded proofs.

Abstract

In previous work we provided a method for eliminating cuts in non-wellfounded proofs with a local-progress condition, these being the simplest kind of non-wellfounded proofs. The method consisted of splitting the proof into nicely behaved fragments. This paper extends our method to proofs based on simple trace conditions. The main idea is to split the system with the trace condition into infinitely many local-progress calculi that together are equivalent to the original trace-based system. This provides a cut elimination method using only basic tools of structural proof theory and corecursion, which is needed due to the non-wellfounded character of proofs. We will employ the method to obtain syntactic cut elimination for , a system of modal logic with the master modality.
Paper Structure (32 sections, 24 theorems, 170 equations, 1 figure)

This paper contains 32 sections, 24 theorems, 170 equations, 1 figure.

Table of Contents

  1. Preliminaries
  2. Definition of $\alpha\textsf{-}\text{G}^{ \infty }_{ \ell }\text{K}^{ + }_{ s }$
  3. Change of annotations
  4. Auxiliary functions
  5. Pushing cuts
  6. Pushing a cuts outside main local fragment
  7. Pushing cuts outside main global fragment
  8. Cut admissibility
  9. Atomic
  10. Box formulas
  11. Master formula
  12. General case
  13. Cut elimination
  14. Weakening
  15. Contraction
  16. ...and 17 more sections

Key Result

proposition 1

We have that

Figures (1)

  • Figure 1: A graphical representation of the cut elimination process.

Theorems & Definitions (55)

  • definition 1
  • definition 2
  • definition 3: Adding cuts
  • definition 4
  • proposition 1
  • proof
  • definition 5
  • lemma 1
  • proof
  • definition 6
  • ...and 45 more