Representability in second-order propositional poly-modal logic

A propositional system of modal logic is second-order if it contains quantifiers For Allp and There Existsp, which, in the standard interpretation, are construed as ranging over sets of possible worlds (propositions). Most second-order systems of modal logic are highly intractable: for instance, when augmented with propositional quantifiers, K, B, T, K4 and 14 all become effectively equivalent to full second-order, logic, An exception is S5, which, being interpretable in monadic second-order logic, is decidable. In this paper we generalize this framework by allowing multiple modalities. While this does not affect the undecidability of K, B, T, K4 and S4, poly-modal second-order S5 is dramatically more expressive than its mono-modal counterpart, As an example, we establish the definability of the transitive closure of finitely many modal operators. we also take up the decidability issue, and, using a novel encoding of sets of unordered pairs by partitions of the leaves of certain graphs, we show that the second-order propositional logic of two S5 modalitities is also equivalent to full second-order logic.