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 (or T + B)

Symbols.

Symbol	Unicode	Name	Meaning
□	U+25A1	Box	Necessity: "necessarily..."
◇	U+25C7	Diamond	Possibility: "possibly..."
⦿	U+29BF	Strict implication	Necessarily implies
W	—	Worlds	Set of possible worlds
R	—	Accessibility	Relation between worlds
⊨	U+22A8	Satisfaction	True at a world in a model
⦃ ⦄	U+2983/4	World brackets	Evaluation at specific world

Metatheory. Propositional modal logics are decidable. Complexity varies: K is PSPACE-complete, S5 is NP-complete. Soundness and completeness: standard modal logics are complete w.r.t. their frame classes via canonical model construction. Frame correspondence: modal axioms correspond to first-order conditions on frames (e.g., T ↔ reflexivity). First-order modal logic is generally undecidable.

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. Quantified modal logic raises puzzles: transworld identity, de re vs de dicto modality, rigid designators. Barcan formula (◇∃xφ → ∃x◇φ) and its converse are controversial. Choosing the right accessibility relation requires domain knowledge — the formalism doesn't tell you which modal logic to use. Possible worlds semantics is powerful but metaphysically contested.