Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents

TL;DR

This paper introduces a clear, syntactic cut-elimination method for provability logic GL using nested sequents, simplifying the proof process and avoiding complex rewriting or additional measures.

Contribution

It develops a straightforward, unambiguous cut-elimination proof for provability logic GL based on nested sequents, improving upon previous ambiguous approaches.

Findings

Provides a syntactic cut-elimination proof for GL

Simplifies proof process with nested sequents

Avoids complex rewriting and additional measures

Abstract

The cut-elimination procedure for the provability logic is known to be problematic: a L\"ob-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.