Formulary · logic

Kripke semantics

What does "necessarily true" actually mean? Since Kripke, the answer fits in a single picture: true in every world reachable from our own. Three ingredients (worlds, arrows, and a list of facts) are enough to give an exact meaning to necessity, knowledge, and obligation.

0Symbols

Modal logic adds only two symbols to classical logic: a box and a diamond. Everything else exists to give them meaning. Here is the dictionary.

Symbol	Meaning
p, q	Atomic propositions: the simplest sentences, true or false. "It is raining," "the door is closed."
¬, ∧, ∨, →	The classical connectives: not, and, or, if...then. They work here exactly as usual.
□A	"Box A": necessarily A. The formula A is true in every accessible world.
◇A	"Diamond A": possibly A. The formula A is true in at least one accessible world.
w, v	Possible worlds: complete states of affairs. Our world is just one among others.
W	The set of all worlds in the model. There must be at least one.
R	The accessibility relation: the arrows between worlds. wRv reads "from w, the world v is accessible."
V(p)	The valuation: for each proposition p, the list of worlds where it is true.
M = (W, R, V)	The Kripke model: the three ingredients combined. Worlds, arrows, facts.
M, w ⊨ A	"A is true at world w in model M." The double turnstile reads "satisfies."
⊭	The same sign, crossed out: A is not true at that world.
(W, R)	The frame: the worlds and the arrows, without the valuation. It is the model's skeleton.
⊤, ⊥	The constant true and false: ⊤ is true everywhere, ⊥ is true nowhere.
K, T, D, 4, B, 5	Names of axioms, then of systems. Each one places a requirement on the arrows: that is section 5.

Trap number one

A modal formula is not true or false "by itself." It is true or false at a given world. The very first question is always: at which world am I evaluating?

1Possible worlds

"2 + 2 = 4" and "it is raining in Bern" might both be true. But not in the same way.

The first could not have been false. The second very well could have been: just imagine a different course of events.

Classical logic does not see this difference. Modal logic was born to see it.

1.1 · Why one more logic

What

We want to be able to write "necessarily A" and "possibly A," and compute with them.

To do this we add two operators, □ and ◇, in front of any formula.

Why

Because a truth table is no longer enough. The truth of "it is raining" says nothing about whether "necessarily it is raining" is true.

The idea that unlocks everything comes from Leibniz: necessary means true in all possible worlds. Around 1960, Kripke turned this into a mathematical definition by adding arrows between worlds.

How

We draw a small universe: circles for the worlds, arrows to say which worlds count from which, letters to say what is true where.

Then we evaluate the formulas world by world, with four rules. That is the whole chapter.

1.2 · Necessary and possible

Duality

◇A ≡ ¬□¬A and □A ≡ ¬◇¬A

What

"Possibly A" means: it is not necessary that not-A.

"Necessarily A" means: it is not possible that not-A. Each operator is defined in terms of the other.

Why

It is the same pair as "for all" and "there exists" in mathematics: ∀ = ¬∃¬.

The box is a "for all accessible worlds," the diamond a "there exists an accessible world." The duality of the quantifiers becomes the duality of the modalities.

How

In practice: to negate a box, turn it into a diamond and push the negation inside. ¬□A ≡ ◇¬A.

To negate a diamond: ¬◇A ≡ □¬A. Exactly as one negates "all" with "there exists one that does not."

1.3 · The model M = (W, R, V)

The Kripke model

M = ( W, R, V ) · W ≠ ∅ , R ⊆ W×W , V(p) ⊆ W

A complete model: three worlds, three arrows (one of them a loop), and the valuation V(p) = {w2}, V(q) = {w3}.

What

W says which worlds exist. R says which ones count from which: wRv means "when I stand at w, v is among the alternatives I consider."

V states the facts: for each letter p, in which worlds it is true.

Why

The arrows are Kripke's breakthrough. For Leibniz, "necessary" meant true in all worlds, without exception.

With R, each world has its own horizon of alternatives. This fine-tuning is what lets the same machine model necessity, an agent's knowledge, obligation, or time.

How

To build a model: draw circles, draw arrows (a loop is allowed, so is no arrow at all), write in each circle the letters that are true there.

Any doodle of this kind is a legitimate Kripke model. The laboratory in section 3 puts one in your hands.

Watch out

By default, R promises nothing. Not reflexive (a world does not necessarily see itself), nor symmetric (v being accessible from w does not make w accessible from v). Every extra property comes at a cost, and is bought with an axiom: that is section 5.

2Truth in a world

Four rules decide everything. Two copy classical logic, two send us traveling.

Atoms

M, w ⊨ p ⟺ w ∈ V(p)

The classical connectives

M, w ⊨ ¬A ⟺ M, w ⊭ A
M, w ⊨ A ∧ B ⟺ M, w ⊨ A and M, w ⊨ B
M, w ⊨ A → B ⟺ M, w ⊭ A or M, w ⊨ B

What

An atom is true wherever the valuation says so, false elsewhere. Nothing more.

Not, and, or, if...then are computed on the spot, in the world where we stand, with the usual truth tables.

The box

M, w ⊨ □A ⟺ for all v: wRv ⟹ M, v ⊨ A

The diamond

M, w ⊨ ◇A ⟺ there exists v: wRv and M, v ⊨ A

The box inspects every successor, the diamond looks for just one. It is ∀ against ∃, in pictures.

Why

The box translates exactly the original intuition: "necessarily A" means A holds in every alternative this world considers.

The diamond translates "nothing rules out A": at least one alternative where A holds. The arrows decide who is accountable to whom.

Example In the model from diagram 1.3 (V(p) = {w2}, arrows w1→w2, w1→w3, w2→w2): ◇p is true at w1, since the witness w2 is accessible and carries p. But □p is false at w1: the successor w3 does not carry p. And at w2, □p is true: its only successor is w2 itself, which carries p. Same model, three different verdicts depending on the world. That is normal, it is even the point.

The blind world

A world with no successor at all makes every box true automatically: the condition "A holds at every successor" is vacuously satisfied, there is no one to check. Even □⊥ is true there. And every diamond is automatically false there: no possible witness. This is not a bug, it is a consequence of the definition, and a great exam classic.

3Exploring a model

Here is a model with four worlds, entirely yours to play with. Add or remove arrows, change the facts, choose a formula: each world shows green if the formula is true there, red otherwise.

Click a world to read the justification. Three experiments are worth trying: make a world blind and evaluate □⊥. Make □p → p fail, then fix it with a loop. Check that ◇p ∧ ◇¬p can be true: possible does not contradict possibly-not.

Laboratory · the model explorer

Formula

True at·

World examinedw1

The facts (click)

The arrows (click)

4A step-by-step evaluation

Evaluating a modal formula means running a recursion: we descend into the formula, travel along the arrows, and carry the verdicts back up.

This laboratory unrolls the recursion before your eyes, on a fixed model with three worlds. Notice w3: it is blind, and this shows up in the traces.

Laboratory · the evaluation trace

Formula

World

5Frames and axioms

So far, true or false was judged within a model. Let's go up a floor: a formula is valid on a frame (W, R) if it is true at every world, for every possible valuation.

The chapter's most elegant result: the famous modal axioms correspond one to one with geometric properties of the arrows.

K, the foundation, valid on every frame

□(A → B) → (□A → □B)

Why

K asks nothing of the arrows: if every successor validates A → B and every one validates A, then every one validates B. It is distributed modus ponens.

Every normal modal logic contains K. The axioms that follow, however, cost something.

T, reflexive frames

□A → A ⟺ wRw for all w

D, serial frames

□A → ◇A ⟺ every world has a successor

4, transitive frames

□A → □□A ⟺ wRv and vRu ⟹ wRu

B, symmetric frames

A → □◇A ⟺ wRv ⟹ vRw

5, euclidean frames

◇A → □◇A ⟺ wRv and wRu ⟹ vRu

Each axiom buys a property of the arrows, and conversely. This is correspondence theory.

How

The systems stack up: S4 = K + T + 4. S5 = K + T + 5, and its frames are exactly those where R is an equivalence relation (reflexive, symmetric, transitive).

In S5, worlds gather into blocks where everyone sees everyone: necessity again becomes "true everywhere in the block," Leibniz's intuition regained.

The laboratory below tests this correspondence live. The starting frame is a simple chain w1 → w2 → w3: no axiom survives there. Turn on a property and watch the axioms flip to green. Every failure comes with its countermodel: the exact valuation that breaks the axiom.

Laboratory · the correspondence machine

Frame properties

Verdicts on this frame

6The many faces of the box

This is where the strength of Kripke semantics lies: the same symbol □ changes trade depending on what we decide the worlds and arrows represent. The machine stays identical, only the interpretation shifts.

Reading	□A	◇A	Natural axioms
Alethic	necessarily A	possibly A	S5
Epistemic	the agent knows that A	A is compatible with what it knows	T, 4 (one only knows what is true; whoever knows, knows that they know)
Deontic	it is obligatory that A	it is permitted that A	D, certainly not T
Temporal	from now on, always A	someday A	4 (the future of the future is the future)
Provability	A is provable	A is consistent	4, and not T (Gödel lurks)

Example Why does the deontic reading reject T? Because there, □A → A would say: everything obligatory is fulfilled. The real world disobeys every day. We keep the more modest D: what is obligatory is at least permitted, in other words the norms do not contradict each other.

7The method

Facing "M, w ⊨ A?", always the same procedure.

Fix the world.

Write down the world of evaluation, in black and white. Without it, the question makes no sense.

Identify the main connective of A.

¬, ∧, ∨, → · we stay put, classical truth tables. □, ◇ · we travel along the arrows.

If □B: list the successors of w.

∅ · no successor: □B is true automatically. otherwise · B must be true at each one, without exception.

If ◇B: look for a witness.

found · a successor where B is true: ◇B is true. none · ◇B is false, including for lack of successors.

Descend recursively, then carry the verdicts back up.

Each subformula is evaluated at the world the journey has led you to, not at the starting world.

To refute a validity: build a countermodel.

Two or three worlds are almost always enough. Set the valuation so the premise is true and the conclusion false at the same world.

8The six mistakes

Mistake 1

Calling a formula "true" without saying at which world. The same formula can be true at w1 and false at w2 within the same model. Always write M, w ⊨ A, never just A.

Mistake 2

Reading ◇ as a little box. The diamond is a "there exists": one accessible witness is enough. Demanding p at every successor for ◇p means evaluating □p without realizing it.

Mistake 3

Believing □p → p is always true. Without a reflexive loop, a world can impose p on all its successors and ignore it itself. "Necessary, therefore true" is an axiom that costs something, not an obvious fact.

Mistake 4

Distributing the box over "or." □(p ∨ q) yields neither □p nor □q: each successor may pick its own side, p here, q there. The box distributes over ∧, not over ∨. The diamond does the opposite.

Mistake 5

Forgetting the blind worlds. Without a successor, every box is true (even □⊥) and every diamond is false (even ◇⊤). Build one in laboratory 3 and see for yourself.

Mistake 6

Confusing the three floors of truth: true at a world, true in a model (at all its worlds), valid on a frame (for every valuation). The axioms of section 5 live on the third floor. One favorable example proves nothing there: every case is needed.

9Test yourself

Eight questions, exactly one right answer each time. The explanation appears after your choice.

10The vocabulary in French and German

This formulary comes from the Swiss gymnasiums (upper secondary schools), where it is taught bilingually. Here are its core terms in the languages in which they were coined.

Français	Deutsch
la logique modale	die Modallogik
le monde possible	die mögliche Welt
la relation d'accessibilité	die Zugänglichkeitsrelation
la valuation	die Belegung
le modèle de Kripke	das Kripke-Modell
le cadre	der Rahmen
nécessaire	notwendig
possible	möglich
contingent	kontingent
l'opérateur modal	der Modaloperator
satisfaire (une formule)	(eine Formel) erfüllen
valide	gültig
satisfaisable	erfüllbar
le contre-modèle	das Gegenmodell
le successeur	der Nachfolger
le monde aveugle (sans successeur)	die blinde Welt (ohne Nachfolger)
réflexif	reflexiv
symétrique	symmetrisch
transitif	transitiv
sériel	seriell
euclidien	euklidisch
la relation d'équivalence	die Äquivalenzrelation
l'axiome	das Axiom
la théorie de la correspondance	die Korrespondenztheorie
la lecture épistémique / déontique	die epistemische / deontische Lesart