Uniform interpolation for interpretability logic

TL;DR

This paper develops proof-theoretical frameworks for interpretability logic IL, demonstrating that cyclic proofs enable uniform interpolation, which also applies to the extended logic ILP, advancing the understanding of their structural properties.

Contribution

It introduces wellfounded and non-wellfounded sequent calculi for IL, proving uniform interpolation using cyclic proof techniques, and extends results to ILP.

Findings

Cyclic proofs suffice for IL's proof theory.

Uniform interpolation is established for IL.

Uniform interpolation is also proved for ILP.

Abstract

We present a proof-theoretical study of the interpretability logic IL, providing a wellfounded and a non-wellfounded sequent calculus for IL. The non-wellfounded calculus is used to establish a cut elimination argument for both calculi. In addition, we show that the non-wellfounded proof theory of IL is well-behaved, i.e., that cyclic proofs suffice. This makes it possible to prove uniform interpolation for IL. As a corollary we also provide a proof of uniform interpolation for the interpretability logic ILP.