Uniform Interpolation and Propositional Quantifiers in Modal Logics

We investigate uniform interpolants in propositional modal logics from the proof-theoretical point of view. Our approach is adopted from Pitts’ proof of uniform interpolationin intuitionistic propositional logic [15]. The method is based on a simulation of certain quantifiers ranging over propositional variables and uses a terminating sequent calculus for which structural rules are admissible. We shall present such a proof of the uniform interpolation theorem for normal modal logics K and T. It provides an explicit algorithm constructing the interpolants. Presented by Heinrich Wansing