Variations on the Kripke Trick

In the early 1960s, to prove undecidability of monadic fragments of sublogics of the predicate modal logic QS5 QS 5 that include the classical predicate logic QCl QCl , Saul Kripke showed how a classical atomic formula with a binary predicate letter can be simulated by a monadic modal formula. We consider adaptations of Kripke’s simulation, which we call the Kripke trick, to various modal and superintuitionistic predicate logics not considered by Kripke. We also discuss settings where the Kripke trick does not work and where, as a result, decidability of monadic modal predicate logics can be obtained.