 The great success of the Kripkean model theory notwithstanding, it is worth emphasizing that not all modal logics are complete. For incompleteness results see Makinson 1969, for a system weaker than S4; and Fine 1974, S. Thomason 1974, Goldblatt 1975, and van Benthem 1978, for systems between S4 and S5. Some modal formulas impose conditions on frames that cannot be expressed in a first-order language, thus even propositional modal logic is fundamentally second-order in nature. Insofar as the notion of validity on a frame abstracts from the interpretation function, it implicitly involves a higher-order quantification over propositions. On the correspondence between frame validity and second-order logic and on the model-theoretic criteria that distinguish the modal sentences that are first-order expressible from those that are essentially second-order see Blackburn and van Benthem’s “Modal Logic: A Semantic Perspective” (2007a).