Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents

Akinori Maniwa, Ryo Kashima

TL;DR

This paper addresses the longstanding difficulty of syntactic cut-elimination for provability logic $GL$, where the Löb axiom induces a diagonal formula that complicates reduction. The authors develop a nested-sequents proof system and introduce a diagonal-formula-elimination subprocedure, aided by an annotated calculus that tracks diagonal usage. By combining diagonal-elimination with a standard double induction, they obtain a syntactic cut-elimination theorem that avoids Valentini-Poggiolesi style triple-induction pitfalls. The approach yields a concise, modular proof and suggests robust avenues for extensions to related modal logics and alternative cut rules. Overall, the work clarifies termination issues and offers a clearer, more composable pathway to cut-elimination in GL using nested sequents.

Abstract

The cut-elimination procedure for the provability logic is known to be problematic: a Löb-like rule keeps cut-formulae intact on reduction, even in the principal case, thereby complicating the proof of termination. In this paper, we present a syntactic cut-elimination proof based on nested sequents, a generalization of sequents that allows a sequent to contain other sequents as single elements. A similar calculus was developed by Poggiolesi (2009), but there are certain ambiguities in the proof. Adopting the idea of Kushida (2020) into nested sequents, our proof does not require an extra measure on cuts or error-prone, intricate rewriting on derivations, but only straightforward inductions, thus leading to less ambiguity and confusion.

Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents

TL;DR

This paper addresses the longstanding difficulty of syntactic cut-elimination for provability logic , where the Löb axiom induces a diagonal formula that complicates reduction. The authors develop a nested-sequents proof system and introduce a diagonal-formula-elimination subprocedure, aided by an annotated calculus that tracks diagonal usage. By combining diagonal-elimination with a standard double induction, they obtain a syntactic cut-elimination theorem that avoids Valentini-Poggiolesi style triple-induction pitfalls. The approach yields a concise, modular proof and suggests robust avenues for extensions to related modal logics and alternative cut rules. Overall, the work clarifies termination issues and offers a clearer, more composable pathway to cut-elimination in GL using nested sequents.

Abstract

The cut-elimination procedure for the provability logic is known to be problematic: a Löb-like rule keeps cut-formulae intact on reduction, even in the principal case, thereby complicating the proof of termination. In this paper, we present a syntactic cut-elimination proof based on nested sequents, a generalization of sequents that allows a sequent to contain other sequents as single elements. A similar calculus was developed by Poggiolesi (2009), but there are certain ambiguities in the proof. Adopting the idea of Kushida (2020) into nested sequents, our proof does not require an extra measure on cuts or error-prone, intricate rewriting on derivations, but only straightforward inductions, thus leading to less ambiguity and confusion.
Paper Structure (7 sections, 12 theorems, 13 equations, 5 figures)

This paper contains 7 sections, 12 theorems, 13 equations, 5 figures.

Table of Contents

  1. Introduction
  2. The Calculus
  3. Problem on Cut-Reduction
  4. Annotated System
  5. Diagonal-Formula-Elimination
  6. Syntactic Cut-Elimination
  7. Conclusion

Key Result

theorem 2.2

A formula $A$ is a theorem of $\logic{GL}$ if and only if the sequent $A$ is provable in the calculus.

Figures (5)

  • Figure 1: Inference rules for $\logic{GL}$.
  • Figure 2: Original derivation $\mathscr{D}$.
  • Figure 3: First step: Truncate the derivation above the application of \ref{['tree:orig:box']} by adding $\raisebox{\lasyOffset}{$\UseName{m@th}\mdwhtdiamond$} B\cramped{\sp\bot}$ as an assumption.
  • Figure 4: Second step: Displace the application of \ref{['tree:orig:dia']} with a cut on $A$.
  • Figure 6: Inference rules with annotations.

Theorems & Definitions (27)

  • definition 2.1: Depth
  • theorem 2.2: Completeness
  • remark 1
  • definition 2.3: Cut
  • lemma 2.4: Inversion
  • proof
  • lemma 2.5: Identity
  • proof
  • lemma 2.6: Structural rules
  • proof
  • ...and 17 more