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 ∑_1~1. We identify fragments L of ∑_1~1 where second-order quantification of relations of arity k ＞ 1 is (nontrivially) vacuous in the sense that each formula of L can be translated to a formula of (a fragment of) monadic ∑_1~1. Let polyadic Boolean modal logic with identity (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 ∑_1~1(PBML=) be the extension of PBML= with existential prenex quantification of accessibility relations and proposition symbols. The principal result of the article is that ∑_1~1(PBML=) translates into monadic ∑_1~1. 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 ∑_1~1(FO~2) is also expressible in monadic ∑_1~1. This question was left open in the 1999 paper of Gradel and Rosen in the 14th Annual IEEE Symposium on Logic in Computer Science.