S4 Modal Logic

Origin. Lewis and Langford, Symbolic Logic (1932), Appendix II, introduced S1–S5 as systems of strict implication. Gödel, "Eine Interpretation des intuitionistischen Aussagenkalküls" (1933), gave the modern axiomatization as K + T + 4 and translated intuitionistic propositional logic into it. McKinsey and Tarski, "The Algebra of Topology" (1944) and "Some Theorems About the Sentential Calculi of Lewis and Heyting" (1948), supplied the topological and algebraic semantics and proved the translation faithful. Kripke's relational semantics (1963) identified the frame condition as reflexive transitivity.

Models. Kripke frames whose accessibility relation is a preorder — reflexive and transitive. Equivalently, topological spaces with □ read as interior and ◇ as closure, the interpretation of McKinsey and Tarski; equivalently, the variety of closure algebras (interior algebras). Since clusters can be collapsed without changing the modal theory, S4 is also determined by finite partial orders, and indeed by finite trees.

Formalism.

Axioms: K: □(A → B) → (□A → □B). T: □A → A. Truth axiom. 4: □A → □□A. Positive introspection.

Rules: Modus ponens. Necessitation.

Frame condition: R reflexive: wRw. R transitive: wRv ∧ vRu → wRu. Preorder.

Characteristic formula: □A → □□A (4). Validity: all reflexive transitive frames. Defines S4.

Topological semantics: Open sets = propositions. □ = interior operator. ◇ = closure operator. S4 = logic of topology.

Intuitionistic connection: Gödel–McKinsey–Tarski translation ( )^T: p^T = □p. (A ∧ B)^T = A^T ∧ B^T. (A → B)^T = □(A^T → B^T). (¬A)^T = □¬A^T. IPC ⊢ A iff S4 ⊢ A^T. S4 is the modal companion of intuitionistic logic.

Modalities: Exactly 14 distinct modalities, counting the empty one (Parry, 1939). □, ◇, □◇, ◇□, □◇□, ◇□◇ and their negations, plus identity. Contrast S5 with 6 and T with infinitely many.

Provability reading: □A: A is provable. If provable, provably provable. But □A → A not for formal provability.

Epistemic reading: □A: agent knows A. KK principle: knowing implies knowing you know. Controversial.

Extensions: S4.1: + □◇A → ◇□A (McKinsey; atomic frames). S4.2: + ◇□A → □◇A (directedness / confluence). S4.3: + □(□A → B) ∨ □(□B → A) (no branching to the right). Grz: + □(□(A → □A) → A) → A (Noetherian partial orders). S5: + symmetric.

Symbols.

Metatheory. Sound and complete for reflexive transitive frames; 4 is a Sahlqvist formula, so S4 is canonical and its frame condition is first-order definable. Filtration yields the finite model property with models of size at most 2^|sub(φ)|, and satisfiability is PSPACE-complete (Ladner, 1977), matching K and T. The McKinsey–Tarski theorem (1944) is sharper than mere topological completeness: S4 is the logic of any dense-in-itself metrizable space, in particular of the real line and of Cantor space. The Gödel–McKinsey–Tarski translation is faithful in both directions (McKinsey and Tarski, 1948), making S4 the largest modal companion of intuitionistic logic and, by the Blok–Esakia theorem, placing the lattice of intermediate logics in isomorphism with the lattice of normal extensions of Grz. S4 has exactly fourteen distinct modalities (Parry, 1939) and enjoys Craig interpolation; Maksimova (1979) showed that at most thirty-seven normal extensions of S4 have the interpolation property, so it fails in most of them. S4 is a proper extension of T and a proper sublogic of S4.2, S4.3, Grz and S5.

Applies to. Topology. Intuitionistic logic. Knowledge. Provability (modified).

Limitations. S4 is unsound for formal provability: it contains T, and by Löb's axiom adding the reflection schema □A → A to GL proves everything, so any provability logic containing reflection is inconsistent; the correct system is GL, in which 4 survives but T does not. Under the epistemic reading, 4 is the KK principle, which forces an agent's knowledge to be transparent to itself, and the underlying normality forces logical omniscience. Topologically, S4 is too coarse to distinguish spaces: the real line, the plane, and Cantor space all validate exactly S4, so no topological invariant beyond the interior–closure structure is detectable. S4 does not validate the McKinsey formula □◇A → ◇□A or directedness ◇□A → □◇A, so it says nothing about convergence of alternatives, and it does not decide whether accessibility branches. Interpolation is fragile above it, failing in all but at most thirty-seven of its normal extensions.

© 2026 Lingenic LLC