Uniform interpolation and the existence of sequent calculi

Abstract

This paper presents a uniform and modular method to prove uniform interpolation for several intermediate and intuitionistic modal logics. The proof-theoretic method uses sequent calculi that are extensions of the terminating sequent calculus G4ip for intuitionistic propostitional logic. It is shown that whenever the rules in a calculus satisfy certain structural properties, the corresponding logic has uniform interpolation. It follows that the intuitionistic versions of K and KD (without the diamond operator), as well as several other intuitionistic modal logics, have uniform interpolation. It also follows that no intermediate or intuitionistic modal logic without uniform interpolation has a sequent calculus satisfying those structural properties. Thereby establishing that except for the seven intermediate logics that have uniform interpolation, no intermediate logic has such a sequent calculus.