The expressive power of second-order propositional modal logic (Q1924326)

The paper considers modal logics with propositional quantifiers (such a logic is briefly called \textbf{SOPML}), with ``platonistic'' semantics, defined according to \textit{K. Fine} [Theoria 36, 336-346 (1970; Zbl 0302.02005)]. In the latter paper it was proved that second-order arithmetic is interpretable in \textbf{SOPML}, provided the basic modal logic is \textbf{S4.2} or weaker. The authors prove a stronger result, namely that in these cases \textbf{SOPML} is mutually interpretable with classical second-order predicate logic. Also they reproduce an unpublished proof of a result by H. Kamp (1977) that \textbf{SOPML} (for the same cases) is embeddable in Thomason's modal first-order logic \textbf{Q2}, with quantification over individual concepts. Therefore classical second-order predicate logic also is embeddable in \textbf{Q2}.