Modal Logic

What Modal Logic Adds

Propositional logic and predicate logic say what is true. Modal logic says what is necessarily or possibly true.

The two new operators:

• $\Box \varphi$: "necessarily $\varphi$." Read in different application domains as: it must be that $\varphi$, it is known that $\varphi$, it is obligatory that $\varphi$, $\varphi$ holds at every future time.
• $\Diamond \varphi$: "possibly $\varphi$." Read as: it might be that $\varphi$, it is consistent with what is known that $\varphi$, $\varphi$ is permissible, $\varphi$ holds at some future time.

The two are interdefinable: $\Diamond \varphi \equiv \neg \Box \neg \varphi$, and $\Box \varphi \equiv \neg \Diamond \neg \varphi$. So the language with one of them as primitive can express the other.

Once $\Box$ and $\Diamond$ are in the language, modal logic becomes the natural framework for several distinct philosophical and technical tasks: metaphysics of modality, epistemic and deontic reasoning, temporal logic in formal verification, dynamic logic for program semantics. Kripke's possible-worlds semantics (1959, 1963) made all of this technically tractable in one common framework.¹

This page assumes What Is Logic?, Validity vs Soundness, Syntax vs Semantics in Formal Systems, Propositional Logic, and What Is a Symbolic System?.

Four Readings of the Same Operators

The same modal operators are reused across very different application domains. Choosing which reading to apply commits the user to different formal axioms.

The pluralism is structural, not philosophical confusion. Different domains have different formal commitments about how $\Box$ behaves, captured in different axiom systems below.

Kripke Semantics: Frames and Models

The conceptual move that made modal logic technically tractable is Kripke's possible-worlds semantics.

A Kripke frame is a pair $\langle W, R \rangle$:

• $W$ is a non-empty set of worlds.
• $R \subseteq W \times W$ is the accessibility relation. $w R w'$ means "world $w'$ is accessible from world $w$."

A Kripke model is a triple $\mathcal{M} = \langle W, R, V \rangle$ where $\langle W, R \rangle$ is a frame and $V: \text{atoms} \to \mathcal{P}(W)$ is a valuation: $V(p)$ is the set of worlds where $p$ is true.

The recursive truth definition:

• $\mathcal{M}, w \models p$ iff $w \in V(p)$, for atomic $p$.
• $\mathcal{M}, w \models \neg \varphi$ iff $\mathcal{M}, w \not\models \varphi$.
• $\mathcal{M}, w \models \varphi \land \psi$ iff $\mathcal{M}, w \models \varphi$ and $\mathcal{M}, w \models \psi$.
• (likewise for the other propositional connectives)
• $\mathcal{M}, w \models \Box \varphi$ iff for every $w'$ with $w R w'$, $\mathcal{M}, w' \models \varphi$.
• $\mathcal{M}, w \models \Diamond \varphi$ iff for some $w'$ with $w R w'$, $\mathcal{M}, w' \models \varphi$.

The clauses for $\Box$ and $\Diamond$ are the heart of Kripke semantics. $\Box \varphi$ at $w$ says $\varphi$ holds at every world accessible from $w$. The accessibility relation $R$ encodes which worlds are "reachable" from a given world, and the modality is interpreted relative to the worlds reachable.

Different readings of the modal operators correspond to different intuitive readings of accessibility:

• Alethic: $w R w'$ means $w'$ is a way the world might have been, given $w$.
• Epistemic: $w R w'$ means $w'$ is consistent with what the agent at $w$ knows.
• Deontic: $w R w'$ means $w'$ is one of the deontic alternatives to $w$, the worlds where everything obligatory is the case.
• Temporal: $w R w'$ means $w'$ is a moment after $w$ (with various refinements for branching versus linear time).

A Worked Kripke Model

Take a small Kripke model with three worlds.

$W = \{w_1, w_2, w_3\}$, with accessibility relation

Visualization: $w_1$ accesses $w_2$ and $w_3$; $w_2$ accesses $w_3$; $w_3$ accesses itself.

Atomic valuations: $V(p) = \{w_2, w_3\}$ (so $p$ is true at $w_2$ and $w_3$, false at $w_1$). $V(q) = \{w_3\}$ ($q$ is true only at $w_3$).

Evaluate $\Box p$ at each world:

• $w_1$: accesses $w_2$ and $w_3$. $p$ is true at both. So $\mathcal{M}, w_1 \models \Box p$.
• $w_2$: accesses $w_3$. $p$ is true at $w_3$. So $\mathcal{M}, w_2 \models \Box p$.
• $w_3$: accesses $w_3$. $p$ is true at $w_3$. So $\mathcal{M}, w_3 \models \Box p$.

So $\Box p$ is true at every world.

Evaluate $\Box q$ at each world:

• $w_1$: accesses $w_2$ and $w_3$. $q$ is true at $w_3$ but false at $w_2$. So $\mathcal{M}, w_1 \not\models \Box q$ (one accessible world fails).
• $w_2$: accesses $w_3$. $q$ is true at $w_3$. So $\mathcal{M}, w_2 \models \Box q$.
• $w_3$: accesses $w_3$. $q$ is true at $w_3$. So $\mathcal{M}, w_3 \models \Box q$.

So $\Box q$ is true at $w_2$ and $w_3$, false at $w_1$.

Evaluate $\Diamond q$ at each world:

• $w_1$: accesses $w_2$ and $w_3$. $q$ is true at $w_3$. So $\mathcal{M}, w_1 \models \Diamond q$.
• $w_2$: accesses $w_3$. $q$ is true at $w_3$. So $\mathcal{M}, w_2 \models \Diamond q$.
• $w_3$: accesses $w_3$. $q$ is true at $w_3$. So $\mathcal{M}, w_3 \models \Diamond q$.

So $\Diamond q$ is true everywhere.

The general procedure: to evaluate a modal formula at a world, look at all worlds accessible from it and recursively evaluate the formula's interior.

The Standard Systems: K, T, S4, S5

Different axiom systems correspond to different classes of Kripke frames. The classical hierarchy:

The two inference rules of any normal modal system:

• Modus ponens: from $\varphi$ and $\varphi \to \psi$, infer $\psi$.
• Necessitation: from $\vdash \varphi$ (i.e., $\varphi$ is a theorem), infer $\vdash \Box \varphi$.

Necessitation says: anything provable in pure logic must hold in every world (since the proof goes through regardless of which world we are at).

The axiom labeled K above (sometimes called the distribution axiom) is the modal analog of modus ponens: necessity distributes over conditional. Every normal modal logic includes K. The other axioms add stronger commitments.

Correspondence Between Frame Properties and Axioms

The most striking technical fact about modal logic: each standard modal axiom corresponds to a specific algebraic property of the accessibility relation.²

The correspondence theorem makes the choice of modal system non-arbitrary. If the application domain demands that $\Box$ behaves factively ($\Box \varphi \to \varphi$, "what is known is true"), the accessibility relation must be reflexive. If it demands positive introspection ($\Box \varphi \to \Box \Box \varphi$, "if you know it, you know that you know it"), the relation must be transitive. The axioms and the relation are not two independent choices.

Worked Application: Epistemic Logic for AI Agents

Modal logic is the standard substrate for epistemic logic: reasoning about what agents know.³ In a multi-agent system with $n$ agents, we use $n$ modal operators $K_1, \ldots, K_n$, where $K_i \varphi$ reads "agent $i$ knows that $\varphi$."

The standard epistemic axioms:

• $K_i \varphi \to \varphi$ (T): knowledge is factive. Agents know only true things.
• $K_i \varphi \to K_i K_i \varphi$ (4): positive introspection. Agents know what they know.
• $\neg K_i \varphi \to K_i \neg K_i \varphi$ (5): negative introspection. Agents know what they do not know.

A logically idealized agent satisfies S5 epistemic logic. Real human agents do not: humans regularly believe false things (failure of T), are mistaken about the contents of their knowledge (failure of 4), and lack awareness of their ignorance (failure of 5). Whether an AI agent's representations satisfy these axioms depends on the architecture, the training, and the deployment regime.

Common variants:

• Belief logic drops the factivity axiom T (agents can believe false things). The standard system is KD45: $K \varphi \to \neg K \neg \varphi$ (consistency), positive introspection, negative introspection.
• Common knowledge uses an additional operator $C \varphi$: "everyone knows that everyone knows that ... $\varphi$, ad infinitum." Common knowledge is needed for coordinated action and is famously hard to establish via finite communication (Fagin, Halpern, Moses, Vardi 1995).

This is one of the cleanest places where modal logic is not a philosophy detour but a working tool for reasoning about distributed AI systems.

Common Confusions

Confusion 1: $\Box$ as logical truth. $\Box \varphi$ does not mean "$\varphi$ is logically valid." It means "$\varphi$ holds at every world accessible from the current one." Whether the modality coincides with logical validity depends on the accessibility relation. In S5 with a single equivalence class of worlds, the two notions can collapse; in K with arbitrary accessibility, they cannot.

Confusion 2: $\Box \varphi \to \Box \Box \varphi$ is "obvious." Positive introspection is intuitive in some readings but not always true. For factive knowledge, S4 (positive introspection) is plausible. For objective necessity, the axiom is much more contestable. For belief, agents often believe propositions without higher-order beliefs about those beliefs. The choice is empirical and varies by application.

Confusion 3: alethic and epistemic readings are interchangeable. They share notation but make different commitments. Alethic necessity ("must be") and epistemic necessity ("known") are different modalities. A statement can be epistemically possible (consistent with what is known) but alethically impossible (false in every metaphysically possible world), or vice versa.

Confusion 4: $\Box$ and $\forall$ are the same. They are related (both are universal-style operators) but they quantify over different things. $\forall x\, P(x)$ quantifies over objects in the domain. $\Box \varphi$ quantifies over accessible worlds. Combining them gives quantified modal logic (QML), which has additional technical complications: should constants denote the same object across worlds (rigid designation, Kripke 1972)? what is the domain at each world? QML is well-developed but more involved than either propositional modal logic or standard first-order logic alone.

Three Exercises

Exercise 1. Consider the Kripke model from "A Worked Kripke Model" above. Evaluate each formula at each world:

(a) $\Box (p \to q)$. (b) $\Diamond (p \land \neg q)$. (c) $\Box \Diamond q$.

Exercise 2. Decide whether each formula is valid in K (true at every world of every Kripke model), and separately whether it is valid in S5 (true at every world of every Kripke model whose accessibility is an equivalence relation):

(a) $\Box (\varphi \to \psi) \to (\Box \varphi \to \Box \psi)$. (b) $\Box \varphi \to \varphi$. (c) $\Diamond \Box \varphi \to \varphi$.

Exercise 3. Construct a Kripke model with at least two worlds where the K axiom $\Box (p \to q) \to (\Box p \to \Box q)$ holds at every world but $\Box p \to \Box \Box p$ fails at some world. (Such a model demonstrates that 4 is strictly stronger than K.)

Answers

Answer 1:

(a) $\Box (p \to q)$:

• $w_1$: accesses $w_2, w_3$. At $w_2$: $p$ is true, $q$ is false, so $p \to q$ is false. Therefore $\Box (p \to q)$ is false at $w_1$.
• $w_2$: accesses $w_3$. At $w_3$: $p$ is true, $q$ is true, so $p \to q$ is true. Therefore $\Box (p \to q)$ is true at $w_2$.
• $w_3$: accesses $w_3$. Same check, true. Therefore $\Box (p \to q)$ is true at $w_3$.

(b) $\Diamond (p \land \neg q)$:

• $w_1$: accesses $w_2, w_3$. At $w_2$: $p$ is true, $\neg q$ is true (since $q$ is false at $w_2$). So $p \land \neg q$ is true at $w_2$. Therefore $\Diamond (p \land \neg q)$ is true at $w_1$.
• $w_2$: accesses $w_3$. At $w_3$: $p$ is true, $\neg q$ is false. So $p \land \neg q$ is false. Therefore $\Diamond (p \land \neg q)$ is false at $w_2$.
• $w_3$: accesses $w_3$. Same as above, false. Therefore $\Diamond (p \land \neg q)$ is false at $w_3$.

(c) $\Box \Diamond q$:

• We computed earlier that $\Diamond q$ is true at every world. So $\Box \Diamond q$ holds at every world (regardless of where the world accesses).

Answer 2:

(a) $\Box (\varphi \to \psi) \to (\Box \varphi \to \Box \psi)$. Valid in K, valid in S5. This is the K axiom itself, valid in every normal modal logic.

(b) $\Box \varphi \to \varphi$. Not valid in K (counterexample: a frame where $w$ does not access itself; let $V(p) = \emptyset$ at $w$, then $\Box p$ holds vacuously at $w$ but $p$ does not hold at $w$). Valid in S5 (since S5 includes T as an axiom; reflexivity guarantees the formula).

(c) $\Diamond \Box \varphi \to \varphi$. Not valid in K. Valid in S5. Reasoning for S5: in an equivalence-relation frame, if $\Diamond \Box \varphi$ holds at $w$, there is some accessible $w'$ with $\Box \varphi$ at $w'$. Since $R$ is symmetric, $w' R w$, so $w$ is among the worlds accessible from $w'$ at which $\Box \varphi$ guarantees $\varphi$. Hence $\varphi$ at $w$. The argument fails without symmetry.

Answer 3. Take three worlds $W = \{u, v, w\}$ with accessibility $R = \{(u, v), (v, w)\}$. The relation is not transitive (we have $u R v$ and $v R w$ but not $u R w$).

Set $V(p) = \{v\}$ (so $p$ is true at $v$, false at $u$ and $w$).

Check the K axiom holds at $u$ for arbitrary $\varphi, \psi$: K is valid in every Kripke model regardless of frame conditions, so we can move on.

Check $\Box p \to \Box \Box p$ at $u$:

• $\Box p$ at $u$: accesses $v$ only. $p$ is true at $v$. So $\Box p$ holds at $u$.
• $\Box \Box p$ at $u$: $\Box p$ should hold at every world accessible from $u$. The only accessible world is $v$. $\Box p$ at $v$: accesses $w$ only. $p$ is false at $w$. So $\Box p$ does not hold at $v$. Therefore $\Box \Box p$ does not hold at $u$.

So at $u$, $\Box p$ holds but $\Box \Box p$ does not. The implication $\Box p \to \Box \Box p$ fails at $u$. The frame is non-transitive, which is why the 4-axiom does not hold.

The model demonstrates that 4 is a strictly stronger axiom than K alone: there are K-models in which 4 fails.

Where Modal Logic Lives in Practice

Three concrete uses.

Formal verification of programs and protocols. Linear temporal logic (LTL) and computation tree logic (CTL) are temporal modal logics used to specify properties of concurrent and reactive systems. Statements like "every request is eventually granted" or "on every branch, the system never deadlocks" are formal-modal sentences over a transition system. Model checkers (SPIN, NuSMV, TLA+) verify them automatically. Modal logic is the substrate of working software-correctness verification.

Knowledge representation in multi-agent AI. Multi-agent epistemic logic (the Fagin-Halpern-Moses-Vardi framework) is the theoretical foundation of game-theoretic AI and distributed-systems verification. Common-knowledge reasoning is essential for analyzing protocols where coordination is required but communication channels can fail.

Metaphysics and counterfactuals. David Lewis's Counterfactuals (1973) develops a possible-worlds semantics for counterfactual conditionals that has shaped Anglophone metaphysics for fifty years. The modal logic of necessity, possibility, and actuality is the formal toolkit for these debates. The pages in PhilosophyPath that touch on possibility and counterfactual reasoning trace back here.

The general lesson: modal logic is one of the few formal systems that crosses cleanly from technical computer science to working metaphysics, and the bridge runs through Kripke's 1959-63 papers.

Prerequisites and Next Pages

• Prerequisites: What Is Logic?, Validity vs Soundness, Syntax vs Semantics in Formal Systems, Propositional Logic, What Is a Symbolic System?.
• Next: Predicate Logic, the natural extension that adds quantifiers; combining it with modal logic gives quantified modal logic.
• Forward link: epistemic logic in particular connects directly to questions about machine knowledge and understanding raised in The Chinese Room Argument.

References

Primary texts:

• Kripke, Saul A. "A Completeness Theorem in Modal Logic." Journal of Symbolic Logic 24 (1959): 1-14.
• Kripke, Saul A. "Semantical Considerations on Modal Logic." Acta Philosophica Fennica 16 (1963): 83-94. The two papers that introduced possible-worlds semantics.
• Lewis, C. I., and C. H. Langford. Symbolic Logic. New York: Dover, 1932. The early modern source for modal axiomatizations.
• Lewis, David. Counterfactuals. Harvard University Press, 1973. The standard possible-worlds semantics for counterfactual conditionals.

Modern reference:

• Hughes, G. E., and M. J. Cresswell. A New Introduction to Modal Logic. Routledge, 1996. The standard textbook covering all of K, T, S4, S5 and the correspondence theory.
• Blackburn, Patrick, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge, 2001. The advanced reference; full mathematical depth on Kripke semantics.
• Fagin, Ronald, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning About Knowledge. MIT Press, 1995. Multi-agent epistemic logic for AI and distributed systems.
• van Benthem, Johan. Modal Logic for Open Minds. CSLI Publications, 2010. The contemporary view of modal logic across applications.

Stanford Encyclopedia entries (link, do not paraphrase):

• "Modal Logic."
• "Possible Worlds."
• "Epistemic Logic."
• "Deontic Logic."
• "Temporal Logic."