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 φ and a
sublanguage L of the language of the formula, we can decide whether φ 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 μ-calculus.
