S5 Modal Logic

Origin. Lewis and Langford, Symbolic Logic (1932), Appendix II, listed S5 as the strongest of the systems of strict implication. Carnap, Meaning and Necessity (1947), read necessity as truth in all state-descriptions, which validates exactly S5. Kripke, "A Completeness Theorem in Modal Logic" (1959), proved completeness for S5 using the universal accessibility relation; Kripke (1963) then recast the condition as an equivalence relation. Scroggs, "Extensions of the Lewis System S5" (1951), had already mapped its proper normal extensions.

Models. Kripke frames whose accessibility relation is an equivalence relation. Because every point-generated subframe of an equivalence frame is universal, S5 is equally determined by frames in which R = W × W, so accessibility can be dropped from the semantics altogether and □A read as "A holds at every world." Algebraically these are the monadic algebras of Halmos. The corresponding worlds are Leibniz's possible worlds under an unrestricted reading of necessity.

Formalism.

Axioms: K: □(A → B) → (□A → □B). T: □A → A. 5: ◇A → □◇A.

Alternative axiomatizations: KT5 = KTB4 = KT4 + B. B: A → □◇A. Multiple equivalent formulations.

Frame condition: R is equivalence relation. Reflexive, symmetric, transitive. Or: universal within components.

Characteristic formulas: ◇A → □◇A (5). ◇□A → □A. Reduces modality iterations.

Reduction laws: □□A ↔ □A. ◇◇A ↔ ◇A. □◇A ↔ ◇A. ◇□A ↔ □A. Only the innermost operator counts. Exactly 6 distinct modalities: —, □, ◇ and their negations.

Normal extensions (Scroggs, 1951): S5_n = logic of a single cluster of at most n worlds. S5 ⊋ ... ⊋ S5_2 ⊋ S5_1 = Triv. Every proper consistent normal extension is some S5_n. All are finitely axiomatizable and have the finite model property. Triv: A ↔ □A, the logic of a one-world frame.

Metaphysical reading: □A: A is metaphysically necessary. ◇A: A is metaphysically possible. Leibniz: true in all possible worlds.

Semantic simplicity: All worlds accessible to all (in component). No accessibility distinctions. Just: some world vs all worlds.

Model theory: Propositional S5 = monadic predicate logic. One-variable fragment. Decidable, NP-complete (Ladner 1977).

First-order S5: Barcan formula BF: ∀x □A → □∀x A. Converse Barcan CBF: □∀x A → ∀x □A. Constant domains validate both. Kripke's varying domains invalidate BF; increasing domains validate CBF, decreasing validate BF. Possibilism versus actualism.

Symbols.

Symbol	Unicode	Name	Meaning
□	U+25A1	Box / Necessity	True at every world
◇	U+25C7	Diamond / Possibility	True at some world
↔	U+2194	Biconditional	Reduction laws for iterated modalities
⊋	U+228B	Proper inclusion	Strictly stronger logic
×	U+00D7	Cartesian product	Universal relation W × W
∀	U+2200	Universal quantifier	Barcan formulas
5	—	Negative introspection axiom	◇A → □◇A
B	—	Brouwer axiom	A → □◇A
T	—	Veridicality axiom	□A → A
S5	—	System S5	KT5 = KT4B; the logic of equivalence frames
E	—	Equivalence frame	Reflexive, symmetric, transitive R
Triv	—	Trivial logic	S5 + (A → □A); one-world frame
BF	—	Barcan formula	∀x □A → □∀x A

Metatheory. Sound and complete for equivalence frames, and equally for universal frames, since generated subframes of an equivalence frame are universal; T, 4, 5 and B are all Sahlqvist, so S5 is canonical and elementary. It has a strong small model property: any S5-satisfiable φ is satisfiable in a model with at most |sub(φ)| worlds, which puts satisfiability in NP, and Ladner (1977) proved it NP-complete — the one classical system below the PSPACE-completeness of K, T and S4. The reduction laws leave exactly six distinct modalities. Propositional S5 is equivalent to the one-variable fragment of classical first-order logic, a correspondence traced to Wajsberg (1933). S5 has Craig interpolation and Beth definability. Scroggs (1951) proved that every proper consistent normal extension of S5 is the logic of a finite cluster, so the extensions form a descending ω-chain ending in Triv; S5 is therefore not maximal among consistent normal logics. Makinson (1971) identified the only two Post-complete normal modal logics as Triv and Ver = K + □⊥, neither of which is S5.

Applies to. Metaphysics. Possible worlds. Essentialism. Logical necessity.

Limitations. The reduction laws destroy all iterated structure: every modal fact is itself necessary, so S5 cannot represent contingent necessity, relative possibility that varies from world to world, or nomological modality where the laws could have differed. Because accessibility is an equivalence relation there is no notion of one world being reachable from a second but not conversely, so temporal, deontic and provability readings are all unavailable — S5 is unsound for provability twice over, since it contains T and since 5 fails for consistency statements. Under the epistemic reading, 5 is negative introspection, which requires an agent to know what she does not know and is falsified by any ordinary case of unrecognized ignorance. Quantified S5 with constant domains validates both Barcan formulas, which forces a fixed domain across worlds and makes contingent existence inexpressible; recovering it requires varying domains and thereby the loss of the classical quantifier rules. Adding A → □A collapses S5 into Triv, where modality does nothing.