Second-order propositional modal logic and monadic alternation hierarchies

We establish that the quantifier alternation hierarchy of formulae of second-order propositional modal logic (SOPML) induces an infinite corresponding semantic hierarchy over the class of finite directed graphs. This solves an open problem of van Benthem (1985) [5] and ten Cate (2006) [11]. We also identify modal characterizations of the expressive power of second-order logic (SO) and monadic second-order logic (MSO) in terms of extensions of modal logic with second-order quantification.