Abstract We provide a simple cut elimination proof for the interpretability logic of $$\textsf{IL}$$ IL . To achieve this, we introduce a traditional Gentzen-style sequent calculus for $$\textsf{IL}$$ 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 $$\textsf{IL}$$ IL .