Modal
Logic □◇

00What Modal Logic Is

Classical logic deals in flat truth: a sentence is true or false. But ordinary reasoning is shot through with modality — qualifications about how something is true. "Two plus two must equal four." "It might rain." "You ought to keep your promise." "She knows the answer." Each italicized word shifts a plain claim into a modal one.

Modal logic extends classical logic with two operators to capture this:

The genius of modal logic is that these two little symbols are schematic. Read □ as "necessarily" and you have alethic logic; read it as "it ought to be" and you have deontic logic; as "knows that," epistemic logic; as "always will be," temporal logic; as "is provable that," provability logic. One formal engine, many interpretations — that universality is why modal logic permeates philosophy, computer science, linguistics, and AI.

01Syntax, Reading & Duality

The language of propositional modal logic is just propositional logic plus □ and ◇. If φ is a formula, so are □φ and ◇φ. The modal operators bind tightly, like negation — so □p → q means (□p) → q, and □(p → q) needs its parentheses.

The duality of □ and ◇

The two operators are interdefinable, exactly as ∀ and ∃ are in predicate logic. "Necessarily" is "not possibly not"; "possibly" is "not necessarily not."

Other equivalences that hold in every modal logic: □(φ ∧ ψ) ≡ □φ ∧ □ψ (necessity distributes over conjunction) and dually ◇(φ ∨ ψ) ≡ ◇φ ∨ ◇ψ. But beware: □(φ ∨ ψ) does not imply □φ ∨ □ψ — "necessarily heads-or-tails" doesn't make either outcome necessary. Verify any of these in the sandbox by checking they hold at every world of any model.

02Possible Worlds

The intuition behind modal logic is ancient (Leibniz spoke of God surveying all possible worlds), but the formal idea is simple and powerful: a possible world is a complete way things could be. The actual world is one of them; others represent alternative total scenarios.

This already explains the duality: if φ fails to be necessary, there must be some world where ¬φ — i.e. ◇¬φ. And it explains why □φ → φ feels right for necessity (whatever is true in all worlds is true here, since the actual world is one of them) yet wrong for obligation (what ought to be, sadly, often isn't).

03Kripke Semantics

A Kripke model (or relational structure) is a triple M = ⟨W, R, V⟩:

Truth is always relative to a world. Writing M, w ⊨ φ for "φ is true at world w in model M," the clauses are the usual ones for atoms and connectives, plus the two that make modal logic modal:

So □ is a universal quantifier over accessible worlds and ◇ an existential one — modal logic is, under the hood, a tame fragment of predicate logic. Two consequences worth tattooing on your memory:

• Vacuous necessity. If a world has no accessible worlds (a "dead end"), then □φ is true there for every φ (an empty "for all"), while ◇φ is false for every φ.
• Truth is local, then global. A formula is valid in a model if true at every world; valid on a frame if true under every valuation; and valid (a theorem) if true on every frame of the relevant class.

Time to make this concrete. The sandbox below is a live Kripke model you can rewire.

◇The Possible-Worlds Sandbox

Here is a four-world Kripke model you can edit. Click cells of the accessibility matrix to add or remove arrows (row = from, column = to; the diagonal is reflexive self-access). Toggle which atoms p, q, r are true at each world. Type a modal formula and the engine evaluates it at every world, colours the graph, and — in the panel below — reports which characteristic axioms your accessibility relation validates.

05The System K — the Modal Floor

Just as propositional logic has its tautologies, each modal logic has its theorems — formulas valid on a class of frames. The smallest "normal" modal logic, valid on all frames whatsoever, is called K (after Kripke). Every other normal system is K plus extra axioms.

Axiom K holds at every world of every Kripke model — try [](p->q) -> ([]p -> []q) in the sandbox under any accessibility relation and it is always true. The intuition: if all accessible worlds make φ→ψ true, and all make φ true, then all make ψ true.

K is sound and complete with respect to the class of all frames: a formula is a theorem of K if and only if it is valid on every frame. Stronger logics are obtained by restricting the frames — which brings us to correspondence theory.

06Frames & Axioms — Correspondence Theory

Here is the most beautiful result in modal logic: each famous axiom is true on exactly those frames whose accessibility relation has a particular property. Adding the axiom and constraining the relation are two sides of one coin. This is correspondence theory.

You can watch this correspondence in the sandbox. Load the counter-model preset: world w1 sees only w2, and p is true only at w2. There □p is true at w1 (every world w1 sees — just w2 — has p) yet p is false at w1, so □p → p fails. The relation isn't reflexive, so axiom T isn't valid. Now click the reflexive preset and T springs to life everywhere.

◇The Map of Modal Systems

Stacking these axioms onto K yields the classic hierarchy of modal logics. Click any system to see its axioms, its frame condition, and where it is used.

08The Many Faces of □

Because the formalism is interpretation-neutral, the same machinery models radically different notions. Each "flavour" of modal logic picks an interpretation of □ and the frame conditions that fit it.

Alethic — necessity & possibility

The original reading: □ = "necessarily," ◇ = "possibly." Metaphysical necessity is standardly modelled by S5. Logical, physical, and metaphysical necessity form nested grades.

Epistemic — knowledge

Read □ as K_a = "agent a knows that." K_aφ → φ (T: knowledge is factive — you can't know falsehoods) is essential; with introspection axioms 4 (you know that you know) and 5 (you know what you don't know) you get S5 for idealized knowers. Accessible worlds are those compatible with what a knows. Multi-agent versions add common knowledge — central to game theory and the puzzle of the muddy children.

Doxastic — belief

□ = "believes." Belief drops factivity (you can believe falsehoods) but keeps consistency (D) and introspection (4, 5): the standard system is KD45.

Deontic — obligation & permission

□ = O = "it is obligatory that," ◇ = P = "it is permitted that." Crucially we reject T (the obligatory is, sadly, not always actual) but keep D: Oφ → Pφ (what is obligatory is permitted) — the logic KD. Accessible worlds are the deontically ideal ones. Deontic logic is famous for paradoxes (Ross's paradox, the gentle-murderer paradox) that probe the limits of the analysis.

Temporal — time

Tense logic uses operators for the future and past: Gφ ("it will always be that φ"), Fφ ("it will at some point"), and their past mirrors H, P. Worlds are moments; R is the earlier-than relation. Linear vs. branching time (the latter underlying CTL) drives the temporal logics used to verify hardware and software via model checking.

Provability — what arithmetic can prove

Read □ as "it is provable in Peano Arithmetic that." The resulting logic GL (Gödel–Löb) adds the Löb axiom □(□φ → φ) → □φ and is not reflexive (provability is not factivity for the system itself). GL exactly captures the provability behaviour behind Gödel's incompleteness theorems — modal logic illuminating the deepest results in metamathematics.

09Quantified Modal Logic

Combine modal operators with the quantifiers of predicate logic and you can express claims about objects across worlds — at the cost of genuine philosophical puzzles.

The Barcan formulas & domains

Does ◇∃x φ → ∃x ◇φ hold (the Barcan formula)? It says no merely-possible objects appear in other worlds — that all worlds share one domain (constant domains). Rejecting it allows varying domains, where different worlds contain different objects (some merely possible people exist in other worlds). The choice is the modal analogue of "could there have been things that don't actually exist?"

10Counterfactuals & the Metaphysics of Worlds

The strict conditional □(φ → ψ) mishandles counterfactuals: "if I had dropped the glass, it would have broken" is not "in all accessible worlds where I drop it, it breaks" (some bizarre world has a force field). David Lewis and Robert Stalnaker gave the modern closest-worlds analysis: a counterfactual φ □→ ψ is true iff in the most similar worlds where φ holds, ψ also holds. Accessibility is replaced by a similarity ordering of worlds.

Possible-worlds talk has paid off across philosophy: analyses of supervenience ("no mental difference without a physical difference" = agreement across worlds), property essentialism, and even formal versions of the ontological argument — Gödel's modal proof derives □∃x God(x) from axioms about "positive properties," a striking (if contested) application of S5 reasoning to theology.

11The GNU Octave Modal Lab

Kripke models are graphs, so modal logic is linear algebra. Represent accessibility as an adjacency matrix R and a valuation as a boolean vector p over worlds; then □ and ◇ are single matrix operations. Run these in GNU Octave or at octave-online.net.

Lab 1 — □ and ◇ as matrix operations

% 4 worlds in a chain: w1 -> w2 -> w3 -> w4
R = [0 1 0 0;
     0 0 1 0;
     0 0 0 1;
     0 0 0 0];
p = [0 1 1 0]';        % p is true at worlds 2 and 3

% []p true at w  <=>  NO accessible world falsifies p
box_p = (R * (~p)) == 0;
% <>p true at w  <=>  SOME accessible world satisfies p
dia_p = (R * p) > 0;

printf('world :  1 2 3 4\n');
printf('p     :  %d %d %d %d\n', p);
printf('[]p   :  %d %d %d %d   (w4 sees nothing -> vacuously true)\n', box_p);
printf('<>p   :  %d %d %d %d\n', dia_p);

Lab 2 — Frame properties as matrix conditions

R = [1 1 0; 0 1 1; 0 0 1];   % reflexive, transitive-ish
R = logical(R);
n = rows(R);

reflexive = all(diag(R));                          % T axiom
serial    = all(any(R, 2));                        % D axiom
symmetric = isequal(R, R');                         % B axiom
transitive= all(all( (double(R)*double(R) > 0) <= R )); % 4 axiom: R^2 ⊆ R
euclidean = all(all( (double(R')*double(R) > 0) <= R )); % 5 axiom

printf('reflexive(T)=%d serial(D)=%d symm(B)=%d trans(4)=%d eucl(5)=%d\n', ...
        reflexive, serial, symmetric, transitive, euclidean);

Lab 3 — Watch axiom T fail, then succeed

R = [0 1; 0 0];   p = [0 1]';      % w1 -> w2 ; p only at w2
box_p = (R * (~p)) == 0;
T = box_p <= p;                  % []p -> p, per world (1 = holds)
printf('Non-reflexive:  []p->p per world = [%d %d]  (w1 FAILS)\n', T);

R = [1 1; 0 1];                 % add self-loops -> reflexive
box_p = (R * (~p)) == 0;  T = box_p <= p;
printf('Reflexive:      []p->p per world = [%d %d]  (holds everywhere)\n', T);

Lab 4 — The S5 collapse of iterated modalities

R = ones(4);             % universal relation = S5 (every world sees every world)
p = [0 1 1 0]';

box   = @(x) (R * (~x)) == 0;
boxp  = box(p);
boxboxp = box(boxp);
printf('[]p   = [%d %d %d %d]\n', boxp);
printf('[][]p = [%d %d %d %d]\n', boxboxp);
printf('In S5, []p == [][]p ? %d\n', isequal(boxp, boxboxp));

Lab 5 — Frame validity over all valuations

% Is axiom T valid on a FRAME? Test every possible valuation of p.
function v = T_valid(R)
  n = rows(R); v = true;
  for m = 0:(2^n - 1)
    p = (bitget(m, 1:n))';          % one of the 2^n valuations
    box_p = (R * (~p)) == 0;
    if any(box_p > p), v = false; return; end  % counterexample
  end
end

printf('T valid on reflexive frame?     %d\n', T_valid(logical(eye(3))));
printf('T valid on non-reflexive frame? %d\n', T_valid(logical([0 1 0;0 0 1;0 0 0])));

Lab 6 — Reachability & the transitive closure (axiom 4)

R = logical([0 1 0; 0 0 1; 0 0 0]);   % w1->w2->w3, NOT transitive

% Transitive closure by repeated boolean matrix powers (reachability)
T = R;
for k = 1:rows(R)
  T = T | (double(T) * double(R) > 0);
end
disp('Original R:');  disp(R);
disp('Transitive closure (now w1 reaches w3):'); disp(T);
% Moving to the closure makes axiom 4 ([]p -> [][]p) valid.

◇Self-Test Quiz

Twelve questions across the whole course. Click an answer for instant feedback and explanation.

13Reference