S4 Modal Logic

Origin. Lewis (1932), Kripke semantics (1963). Reflexive + transitive. Topological interpretation. Foundation of epistemic/provability readings.

Models. Preorder frames. Reflexive transitive accessibility. Interior operator. Topological spaces.

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: S4 embeds intuitionistic logic. □ as provability. Gödel translation.

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.2: + □◇A → ◇□A. S4.3: + □(□A → B) ∨ □(□B → A). S5: + symmetric.

Symbols.

Metatheory. Preorders. Topology. Intuitionistic embedding. Decidable.

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

Limitations. KK principle disputed. Not closed under substitution of equivalents. 4 axiom debated.