Uniform Interpolation in provability logics

TL;DR

This paper establishes the uniform interpolation property for modal provability logics GL and Grz using a proof-theoretical approach with specialized sequent calculi, advancing the understanding of these logics' structural features.

Contribution

It introduces a proof-theoretical method with analytical, terminating sequent calculi to prove uniform interpolation in GL and Grz logics, including a loop-preventing mechanism for Grz.

Findings

Proved uniform interpolation for GL and Grz logics.

Developed a variant of the sequent calculus for GL.

Implemented a loop-preventing mechanism for Grz calculus.

Abstract

We prove the uniform interpolation theorem in modal provability logics GL and Grz by a proof-theoretical method, using analytical and terminating sequent calculi for the logics. The calculus for G\"odel-L\"ob's logic GL is a variant of the standard sequent calculus, in the case of Grzegorczyk's logic Grz, the calculus implements an explicit loop-preventing mechanism inspired by work of Heuerding.