Uniform interpolation and sequent calculi in modal logic

Abstract

A method is presented that connects the existence of uniform interpolants to the existence of certain sequent calculi. This method is applied to several modal logics and is shown to cover known results from the literature, such as the existence of uniform interpolants for the modal logic K . New is the result that KD has uniform interpolation. The results imply that for modal logics K4 and S4 , which are known not to have uniform interpolation, certain sequent calculi cannot exist.