Modal Logic

Origin. C.I. Lewis introduced strict implication (1918) to address paradoxes of material implication. Saul Kripke (1959, 1963) provided the possible worlds semantics that made modal logic mathematically tractable. Ruth Barcan Marcus developed quantified modal logic. Jaakko Hintikka connected it to epistemology.

Models. Necessity and possibility. Truth that varies across a space of alternatives, with modal operators quantifying over that space. Core question: is a proposition merely true, or must it be true? Interpretations include logical necessity (true in all possible worlds), physical necessity (true given laws of nature), metaphysical necessity (true in all genuinely possible situations).

Formalism.

Syntax: Propositional logic extended with □ (necessity) and ◇ (possibility). If φ is well-formed, so are □φ and ◇φ. Duality: ◇φ ≡ ¬□¬φ.

Semantics: Kripke frame F = (W, R) where W is a set of possible worlds and R ⊆ W × W is the accessibility relation. Kripke model M = (F, V) adds a valuation V assigning atoms to sets of worlds.

Truth at a world w:

M, w ⊨ □φ iff for all v, if wRv then M, v ⊨ φ
M, w ⊨ ◇φ iff there exists v such that wRv and M, v ⊨ φ

Normal modal logics: Axiom K (□(φ → ψ) → (□φ → □ψ)) plus necessitation rule (if ⊢ φ then ⊢ □φ). Adding axioms constrains R:

T: □φ → φ (R is reflexive)
4: □φ → □□φ (R is transitive)
B: φ → □◇φ (R is symmetric)
5: ◇φ → □◇φ (R is Euclidean)
S4 = K + T + 4; S5 = K + T + 5 (equivalently K + T + 4 + B)

Symbols.

Symbol	Unicode	Name	Meaning
□	U+25A1	White square / Box	Necessity: "necessarily..."
◇	U+25C7	White diamond	Possibility: "possibly..."
⥽	U+297D	Right fish tail	Lewis's strict implication, □(φ → ψ)
⊨	U+22A8	Satisfaction	True at a world in a model
⊢	U+22A2	Derivability	Provable in the calculus
⊆	U+2286	Subset	R as a set of pairs in W × W
×	U+00D7	Cartesian product	Domain of the accessibility relation
≡	U+2261	Equivalence	Duality of □ and ◇
∀	U+2200	Universal quantifier	Truth clause for □
∃	U+2203	Existential quantifier	Truth clause for ◇
φ, ψ	U+03C6, U+03C8	Phi, psi	Schematic formulas
W	—	Worlds	Set of possible worlds
R	—	Accessibility relation	Relation between worlds
V	—	Valuation	Atoms to sets of worlds
K, T, 4, B, 5	—	Axiom names	Distribution, reflexivity, transitivity, symmetry, euclideanness

Metatheory. Kripke (1963) proved soundness and completeness for K, T, S4, B and S5 with respect to the frame classes their axioms define, by semantic tableaux; the canonical model method of Lemmon, Scott and Makinson yields the same results uniformly, and each of those axioms is Sahlqvist, so each logic is canonical and its frame condition is elementary. Filtration gives the finite model property, hence decidability, and Ladner (1977) fixed the complexity: satisfiability is PSPACE-complete for K, T and S4 but only NP-complete for S5, where models collapse to a single cluster. Under the standard translation, propositional modal logic is exactly the bisimulation-invariant fragment of first-order logic (van Benthem, 1976), and it lies within the two-variable fragment. Completeness is not automatic: Thomason (1974) and Fine (1974) constructed normal modal logics determined by no class of Kripke frames, and Blok (1978) showed such incompleteness is generic rather than exceptional. There are continuum many normal modal logics, and Chagrov proved that whether a finitely axiomatized modal logic is decidable, has the finite model property or is Kripke complete is itself undecidable. First-order modal logic is undecidable even in its monadic fragment (Kripke, 1962).

Applies to. Philosophy (metaphysics, essentialism, possible worlds semantics for counterfactuals). Formal verification (temporal logics are modal logics over time). Linguistics (natural language modality). Knowledge representation. Provability logic (□ as "provable in PA").

Limitations. Bisimulation invariance is a hard expressive ceiling: irreflexivity, well-foundedness, antisymmetry and the number of successors are not modally definable, and no formula distinguishes a model from its tree unravelling, so counting, reachability and world-identity require graded, fixed-point or hybrid extensions rather than clever axioms. Frame validity quantifies over all valuations and is therefore second-order, which is why correspondence works only for restricted syntactic classes and why Chagrova (1991) could prove first-order definability undecidable. Normality forces logical omniscience — necessitation and K make every validity necessary, and necessarily equivalent propositions interchangeable inside □ — so no normal system models a resource-bounded or hyperintensional agent. Quantifying in generates the Barcan formulas, which are valid exactly on decreasing and increasing domains respectively, so any domain assumption settles a metaphysical question by fiat; adding equality makes the necessity of identity a theorem. Kripke completeness fails for continuum many normal logics, and the failure is the typical case.