Classical propositional and predicate logic are inherently static: an assertion is eternally true or eternally false. Yet human cognition, physics, and computer systems operate across dynamic modes: what is necessary versus what is merely possible; what an agent knows versus what an agent believes; what will be true in the future versus what was true in the past. In 1959, an 18-year-old prodigy named Saul Kripke published the relational semantics that transformed Modal Logic from philosophical speculation into a rigorous mathematical science of possible worlds.
1. The Modal Operators $Box$ and $Diamond$
Modal logic augments propositional logic with two dual unary modal operators:
- $Box phi$: “It is necessary that $phi$” (or “Agent knows $phi$”, “It is provable that $phi$”, “Always in the future $phi$”).
- $Diamond phi$: “It is possible that $phi$” (or “$phi$ is consistent with beliefs”, “At some point in the future $phi$”).
The operators are interdefinable via classical duality: $Diamond phi equiv neg Box neg phi$ (Something is possible if and only if its negation is not necessary).
2. Kripke Frames and Relational Semantics
Kripke replaced abstract metaphysical intuitions about “possible worlds” with a precise mathematical structure: a directed graph.
Definition: Kripke Frame & Kripke Model
- A Kripke Frame is a pair $mathcal{F} = (W, R)$, where:
- $W$ is a non-empty set of possible worlds (or system states, time points).
- $R subseteq W times W$ is a binary accessibility relation. The notation $w R v$ denotes that world $v$ is accessible (visible, reachable) from world $w$.
- A Kripke Model is a triple $mathcal{M} = (W, R, V)$, where $V: text{PropVar} to mathcal{P}(W)$ is a valuation assigning to each propositional variable the set of worlds where it is true.
The satisfaction relation $mathcal{M}, w vDash phi$ (“$phi$ is true at world $w$”) is defined inductively:
- $mathcal{M}, w vDash P iff w in V(P)$ for $P in text{PropVar}$.
- Boolean connectives behave locally at world $w$ ($mathcal{M}, w vDash neg phi iff mathcal{M}, w notvDash phi$).
- The Box Operator (Necessity):
[
mathcal{M}, w vDash Box phi iff forall v in W ; (w R v implies mathcal{M}, v vDash phi)
]
$Box phi$ is true in world $w$ if and only if $phi$ holds in every world accessible from $w$. - The Diamond Operator (Possibility):
[
mathcal{M}, w vDash Diamond phi iff exists v in W ; (w R v land mathcal{M}, v vDash phi)
]
$Diamond phi$ is true in world $w$ if and only if $phi$ holds in at least one accessible world.
3. Frame Correspondence Theory
The astonishing mathematical elegance of Kripke semantics is that specific modal axioms correspond exactly to algebraic properties of the accessibility relation $R$:
The Modal Correspondence Hierarchy
| Axiom Name | Modal Formula | Accessibility Relation Property ($R$) | Interpretation |
|---|---|---|---|
| $mathbf{K}$ | $Box(phi to psi) to (Box phi to Box psi)$ | All frames (Universal distribution) | Basic rationality / deductive closure |
| $mathbf{T}$ | $Box phi to phi$ | Reflexive: $forall w (w R w)$ | Truth Axiom: What is known must be true |
| $mathbf{4}$ | $Box phi to Box Box phi$ | Transitive: $u R v land v R w implies u R w$ | Positive Introspection: “If you know, you know you know” |
| $mathbf{B}$ | $phi to Box Diamond phi$ | Symmetric: $u R v implies v R u$ | Symmetry of perspective |
| $mathbf{5}$ | $Diamond phi to Box Diamond phi$ | Euclidean: $u R v land u R w implies v R w$ | Negative Introspection: “If you don’t know, you know it” |
| $mathbf{S5}$ | $mathbf{K} + mathbf{T} + mathbf{4} + mathbf{5}$ | Equivalence Relation (Refl + Trans + Symm) | Metaphysical necessity / Total epistemic reach |
4. Epistemic Logic & Distributed Systems
In computer science and game theory, modal logic was generalized by Jaakko Hintikka (1962) and Joseph Halpern into Multi-Agent Epistemic Logic. For a set of agents ${1, dots, n}$, each agent $i$ has their own knowledge operator $K_i$ and accessibility relation $sim_i$. Two worlds $w sim_i v$ are indistinguishable to agent $i$ based on their local state.
Common Knowledge: $C(phi)$
Define “Everyone knows $phi$”: $E(phi) equiv bigwedge_{i=1}^n K_i phi$.
Common Knowledge is the infinite conjunction:
[
C(phi) equiv E(phi) land E(E(phi)) land E(E(E(phi))) dots
]
Halpern and Moses (1990) proved that in distributed systems with asynchronous networks subject to message loss (the Two Generals Problem), Common Knowledge is mathematically impossible to attain! Distributed consensus algorithms like Paxos and Raft succeed precisely because they weaken the requirement from modal common knowledge to quorum-based state approximations.
