Uniform interpolation for interpretability logic
Logic
2025-11-04 v1
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.
Cite
@article{arxiv.2511.01428,
title = {Uniform interpolation for interpretability logic},
author = {Sebastijan Horvat and Borja Sierra Miranda and Thomas Studer},
journal= {arXiv preprint arXiv:2511.01428},
year = {2025}
}