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.
This page was built for publication: Uniform Interpolation in provability logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6416196)
