Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents

Akinori Maniwa, Ryo Kashima

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 comp…