Monadic and Modal Logic with Quantified Binary Relations

We investigate the expressive power of a range of modal logics extended with second-order prenex quantification of binary and unary relations. Our principal result is that , i.e., Boolean modal logic extended with the identity modality and existential prenex quantification of binary and unary relations, translates into monadic . We also briefly discuss a variety of decidability results in multimodal logic implied by our result.