Modal logic & Kripke frames

Parent: logic

Add operators □ ("necessarily / always / provably") and ◇ ("possibly") to propositional logic. The meaning comes from possible worlds.

Kripke frame & semantics

A frame is (W, R): a set of worlds W and an accessibility relation R ⊆ W×W. A model adds a valuation of atoms per world. Then at a world w:

• □φ holds iff φ holds at every w' with w R w';
• ◇φ holds iff φ holds at some accessible w'.

Frame conditions ↔ axioms (correspondence theory)

The shape of R fixes which modal axioms hold:

S4 = reflexive+transitive (provability, topology, intuitionistic logic); S5 = equivalence relation (knowledge, metaphysical necessity).

The connections that matter

• Intuitionistic logic = S4 (Gödel translation); and intuitionistic logic has its own Kripke models (worlds = states of knowledge, monotone) — the bridge to type theory and Curry–Howard.
• Temporal logic (LTL/CTL) = modal logic over time, and model checking = automata on infinite words (Büchi) — a deep logic ↔ automata link (Vardi–Wolper) back to the automata hierarchy.
• Provability logic (GL): read □ as "provable in PA"; Löb's theorem captures Gödel's incompleteness modally (incompleteness).
• μ-calculus: modal logic + least/greatest fixed points — subsumes LTL/CTL; its natural invariance is bisimulation.

Tie to the thread — this is the harness's backbone

The possible-worlds framing of the recursive harness is literally Kripke semantics:

• a taste/dispatch choice = picking a world w; convergence is per-world;
• [[modal-status-labels|□ definite / ◇ possible]] status labels are the modal operators;
• R (accessibility) = the consistency/dependency relation — "which continuations stay coherent with commitments"; tightening = R contracting toward a single pinned world;
• drift = wandering between worlds not linked by R.

Kripke's worlds gave us the vocabulary to say "non-determinism selects a world; convergence and the gate are per-world."