Uniform Interpolation via Proof Systems

Rosalie Iemhoff

We present a proof–theoretic method to prove interpolation for (intuitionistic) modal and intermediate logics that is inspired by Pitts' syntactic proof of uniform interpolation for intuitionistic propositional logic from 1992. The method, which is based on sequent calculi, inductively defines uniform interpolants based on the rules of a calculus. Thereby establishing that logics with such a calculus have uniform interpolation. The method abstracts away from the particular logical connectives that appear in the rules of a calculus and is to a large degree based on the structural properties that the rules in the calculus satisfy. This abstract approach allows for the application of the method to many logics. And, as we will see, it has useful consequences for logics that do not have uniform interpolation as well.