Deciding the existence of uniform interpolants over transitive models

Abstract We consider the problem of the existence of uniform interpolants in the modal logic K4. We first prove that all Box-free formulas have uniform interpolants in this logic. In the general case, we shall prove that given a modal formula phi and a sublanguage L of the language of the formula, we can decide whether phi has a uniform interpolant with respect to L in K4. The Box-free case is proved using a reduction to the Gödel Löb Logic GL, while in the general case we prove that the question of whether a modal formula has uniform interpolants over transitive frames can be reduced to a decidable expressivity problem on the mu-calculus