Representability in Second-Order Propositional Poly-Modal Logic

A propositional system of modal logic is second-order if it contains quantifiers p and p, 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 S4 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 secondorder 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 se...

• Type: Journal
• Year: 2002
• Where: JSYML
• Authors: Gian Aldo Antonelli, Richmond H. Thomason
• Keywords: JSYML 2002, Logic, Modal Logic, Second-order Logic