Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents

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