Non-wellfounded Proof Theory for Interpretability Logic

We provide a simple cut elimination proof for the interpretability logic of IL. To achieve this, we introduce a traditional Gentzen- style sequent calculus for IL and a non-wellfounded version of it. The non-wellfounded calculus makes it possible to avoid diagonal formulas. Hence, we can give a simple argument based on a general proof-theoretic method for calculi of this kind. Our results provide a useful basis for further research; in particular, they will allow us to establish uniform interpolation for IL.