Existential second-order logic and modal logic with quantified accessibility relations

This article investigates the role of arity   of second-order quantifiers in existential second-order logic, also known as Σ11. We identify fragments L of Σ11 where second-order quantification of relations of arity k>1k>1 is (nontrivially) vacuous in the sense that each formula of L can be translated to a formula of (a fragment of) monadic  Σ11. Let polyadic Boolean modal logic with identity   (PBML=PBML=) be the logic obtained by extending standard polyadic multimodal logic with built-in identity modalities and with constructors that allow for the Boolean combination of accessibility relations. Let Σ11(PBML=) be the extension of PBML=PBML= with existential prenex quantification of accessibility relations and proposition symbols. The principal result of the article is that Σ11(PBML=) translates into monadic  Σ11. As a corollary, we obtain a variety of decidability results for multimodal logic. The translation can also be seen as a step towards establishing whether every property of finite directed graphs expressible in Σ11(FO2) is also expressible in monadic Σ11. This question was left open in the 1999 paper of Grädel and Rosen in the 14th Annual IEEE Symposium on Logic in Computer Science.