Propositionally Quantified Modal Logic

Origin. R. A. Bull, "On modal logic with propositional quantifiers" (Journal of Symbolic Logic 34, 1969, 257–263), extended modal calculi with ∀p and its introduction rules. Kit Fine, "Propositional quantifiers in modal logic" (Theoria 36, 1970, 336–346), set the field's agenda: the systems Kπ+, Tπ+, K4π+, S4π+, S4.2π+, Bπ+, and S5π+ with the quantifiers ranging over all sets of worlds, decidability for S5 — shown also by David Kaplan (1970) — and the encoding of second-order arithmetic in the rest. Michael Kaminski and Michael Tiomkin, "The expressive power of second-order propositional modal logic" (Notre Dame Journal of Formal Logic 37, 1996, 35–43), published the full second-order equivalence. Peter Fritz, "Axiomatizability of propositionally quantified modal logics on relational frames" (Journal of Symbolic Logic 89, 2024, 758–793), The Foundations of Modality: From Propositions to Possible Worlds (Oxford 2023), and Propositional Quantifiers (Cambridge Elements, 2024) are the current book-length and survey treatments.

Models. Modal logic with quantifiers binding the proposition letters themselves, so that ∀p φ asks φ of every proposition. Everything turns on what "every proposition" ranges over. Over a Kripke frame with the quantifiers ranging over all sets of worlds, the language is second-order (hence the alternative name second-order propositional modal logic; see Second-Order Logic.md), and the logic inherits second-order strength for almost every base system, S5 being the exception that collapses into decidability (see S5 Modal Logic.md). Over a designated algebra of admissible propositions (a quantifiable general frame, or a complete Boolean algebra) the quantifiers range over the algebra's elements, and axiomatizability returns. Kremer's terminology, following Henkin, calls the all-subsets reading the primary or principal interpretation and the axiomatically constrained readings secondary. Among its Alethic siblings it is the system in which claims about propositions themselves — that there are world propositions, that every truth is entailed by one — become object-language sentences, which is the use higher-order metaphysics makes of it (Fritz 2023).

Formalism.

Language: φ ::= p | ¬φ | φ ∧ φ | □φ | ∀p φ. ∃p φ := ¬∀p ¬φ.

Quantifier logic: instantiation ∀p φ → φ[ψ/p] for ψ substitutable for p; generalization: from φ → ψ infer φ → ∀p ψ, p not free in φ. Barcan scheme Bc: ∀p □φ → □∀p φ.

Kripke (principal) interpretation: M, w ⊨ ∀p φ iff M[X/p], w ⊨ φ for every X ⊆ W.

S5π+ (Fine 1970; the systems of Bull 1969): S5 + the quantifier logic + the atomicity principle At: some true proposition is a world proposition — it entails every truth. Complete for the principal interpretation over universal frames, and decidable (Fine 1970; Kaplan 1970). Mechanism of decidability: monomodal S5π interprets into monadic second-order logic (Antonelli–Thomason 2002).

Second-order collapse below S5: Kaminski–Tiomkin (1996): for every modal logic S4.2 or weaker, the principal-interpretation logic has the expressive power of full second-order predicate logic. Fine (1970) had encoded second-order arithmetic in Kπ+, Tπ+, K4π+, S4π+, S4.2π+, Bπ+; Fine and Kripke proved the recursive isomorphism with full second-order logic shortly after, unpublished (reported in Kremer 1997). Kremer, "Quantifying over propositions in relevance logic" (JSL 58, 1993, 334–349): propositional quantification over relevance logic R, on its primary interpretation, is recursively isomorphic to full second-order logic. Kremer, "On the complexity of propositional quantification in intuitionistic logic" (JSL 62, 1997, 529–544): the intuitionistic Hπ+ likewise. Antonelli–Thomason, "Representability in second-order propositional poly-modal logic" (JSL 67, 2002, 1039–1054): two S5 modalities already give full second-order logic — the S5 exception is strictly monomodal.

Algebraic and general-frame interpretations: Holliday (NDJFL 60, 2019, 311–332): S5Π is complete for the complete Boolean algebras, quantifiers as meets and joins. Ding–Li (2024): every normal propositionally quantified modal logic containing Bc is strongly complete for the quantifiable general frames validating it.

Axiomatizability frontier (Fritz, JSL 89, 2024): general methods mapping which normal modal logics define frame classes with axiomatizable principal-interpretation logics; if the class is defined by finitely many formulas and has finite diversity, the logic is decidable.

Bisimulation quantifiers: read ∃p φ as truth of φ in some bisimilar variant of the model differing only on p; in a logic with uniform interpolation the uniform interpolant computes ∃p (see Craig Interpolation.md). Pitts (JSL 57, 1992, 33–52) for intuitionistic logic; Visser (1996) and Ghilardi–Zawadowski (Studia Logica 55, 1995, 259–271), whose undefinability of propositional quantifiers in S4 is the failure of uniform interpolation there; D'Agostino–Hollenberg (JSL 65, 2000, 310–332) for the μ-calculus, which is closed under bisimulation quantifiers (see Modal Mu-Calculus.md); French (2006) for the modal systems. The two readings disagree on atoms: Kripke frames validate atomicity, while the bisimulation-quantifier reading validates the atomless principle ∀p(◇p → ∃q(◇(p ∧ q) ∧ ◇(p ∧ ¬q))), assuming a reasonably rich model class (Ding–Li 2024).

Symbols.

Metatheory. The field divides along the interpretation. On the principal interpretation, S5π+ is finitely axiomatized, complete, and decidable (Bull 1969, Fine 1970, Kaplan 1970), because over a universal frame the quantifiers are monadic second-order quantifiers and monadic second-order logic is decidable; K, T, K4, B, S4, and S4.2 each yield a logic with the expressive power of full second-order predicate logic (Kaminski–Tiomkin 1996, covering every logic S4.2 or weaker, after Fine's 1970 encodings), hence not recursively axiomatizable, and the parallel results hold for relevance logic (Kremer 1993) and intuitionistic logic (Kremer 1997). The S5 exception does not survive a second modality (Antonelli–Thomason 2002). The algebraic and general-frame interpretations restore completeness: S5Π for complete Boolean algebras (Holliday 2019), and every normal system containing Barcan for its quantifiable general frames (Ding–Li 2024). Fritz (2024) mapped which normal modal logics have axiomatizable principal-interpretation logics and proved decidability where the frame class is defined by finitely many formulas and has finite diversity. Where the base logic has uniform interpolation, bisimulation quantifiers are definable in the logic itself, which is how the μ-calculus absorbs them (D'Agostino–Hollenberg 2000); S4, lacking uniform interpolation, cannot define them (Ghilardi–Zawadowski 1995).

Applies to. Higher-order metaphysics, where quantification over propositions replaces quantification over sets of worlds as the primitive. Epistemic and doxastic logic, for "everything the agent believes" (Ding 2021 for KD45). Temporal logic, as QPTL. Uniform interpolation and the μ-calculus, through bisimulation quantifiers. Expressiveness comparisons between modal systems and second-order logic (see Second-Order Logic.md).

Limitations. On the principal interpretation the logic of nearly every base system is not recursively axiomatizable — for every modal logic S4.2 or weaker it has the expressive power of full second-order logic — so there is no proof system to study, and the decidable S5 case depends on universal frames, where the language interprets into monadic second-order logic, and is destroyed by a second S5 modality. The algebraic reading restores axiomatizability by restricting the range of the quantifiers to admissible propositions, so instantiation covers only what the algebra contains, and the two readings disagree already on atomicity versus atomlessness. Adding the quantifiers is not innocent even over the quantifier-free fragment: the extension can be nonconservative (Fritz, "Nonconservative extensions by propositional quantifiers and modal incompleteness", Journal of Logic and Computation, 2024). And the bisimulation-quantifier route exists only where uniform interpolation does, which Ghilardi–Zawadowski showed fails for S4.

© 2026 Lingenic LLC