Nested Sequents for Provability Logic GLP

TL;DR

This paper introduces a nested sequent proof system for the provability logic GLP, proves cut elimination, and demonstrates how GLP can be reduced to its J fragment.

Contribution

It develops a novel nested sequent calculus for GLP and establishes cut elimination, enabling syntactic reduction to the J fragment.

Findings

Proof system for GLP with cut elimination

Syntactic reduction of GLP to J fragment

Formal framework for provability logic

Abstract

We present a proof system for the provability logic GLP in the formalism of nested sequents and prove the cut elimination theorem for it. As an application, we obtain the reduction of GLP to its important fragment called J syntactically.