Uniform interpolation and propositional quantifiers in modal logics

Abstract

We investigate uniform interpolants in propositional modal logic from the proof-theoretical point of view. We present a constructive proof of uniform interpolation for modal logics K and T providing an explicite algorithm constructing the interpolants.

The method is based on a simulation of certain quantifiers ranging over propositional variables and uses a terminating sequent calculi for the two logics.

Keywords

• Uniform
• interpolation
• propositional
• quantifiers
• modal
• logics