Formulary · logic

Modal logics: from K to S5

Part 1 (Kripke semantics) gave the formulas their meaning. This one gives the laws: which axioms to choose, which systems they generate, and why there is no single modal logic but an entire ladder, from the minimal K to the comfortable S5.

0The symbols

English

To the signs from Part 1 are added axiom names, a rule, and the operators of the specialised readings.

Symbol	Meaning
□A, ◇A	Necessarily A, possibly A. The pair from Part 1, dual: ◇A ≡ ¬□¬A.
K	The distribution axiom □(A→B)→(□A→□B), and the minimal system that carries it. K as in Kripke.
RN	The necessitation rule: from "A is a theorem," infer "□A is a theorem."
D, T, 4, B, 5	The five optional axioms. Each is paid for with a property of the arrows (Part 1, section 5).
S4, S5	The stacked systems: S4 = K + T + 4, S5 = K + T + 5. The two stars of this chapter.
⊢	"Is a theorem of": S4 ⊢ A says that A is provable in S4. A single turnstile: syntax, not semantics.
O, P, I, F	The deontic reading: obligatory, permitted, forbidden, optional.
Cᵢ A	The epistemic reading: agent i knows A. The common knowledge of a group is written CK.
G, F, X, U	The temporal reading: always from now on (G), someday (F), tomorrow (X), until (U).
[a]p, ⟨a⟩p	The dynamic reading: p holds after every execution of action a; there exists an execution of a leading to p.
RE, RM, RR	The rules of the families broader than the normal logics: section 6.

Trap number one

"The system K," "the axiom T," "the logic S5": these names designate packages of laws, not truths. Choosing a system means choosing what you want □ to mean. There is no absolute right choice, only a right choice per reading.

1The alethic square

English

The original reading, the philosophers' one: □ says "necessary," ◇ says "possible." Four modalities in all, and a precise play of negations to move from one to the other.

1.1 · The four modalities

The four modalities

□A necessary · □¬A impossible
◇A possible · ◇¬A ≡ ¬□A contingent

What

Necessary: what cannot fail to be true. Impossible: what cannot be true.

Possible: what can be true. Contingent: what can be false. Everything holds together with □, ◇, and negation.

Why

Because the placement of the negation changes everything. "It is not necessary that the students work" leaves an escape route; "it is necessary that the students not work" forbids working.

Everyday language blurs these nuances. Formalism freezes them: ¬□A is not □¬A.

1.2 · The square of opposition

English

The four modalities take their places at the corners of a square inherited from Aristotle. Click a corner: its equivalences, its example, and its relations to the other three appear.

Lab · the clickable square

Modality·

Equivalences·

Example With A = "the students work": ¬□A says "it is not necessary that they work" (contingency of A, a relaxation). □¬A says "it is necessary that they not work" (impossibility, a ban). Two almost-twin sentences in everyday speech, two formulas with nothing in common.

2Axioms and necessitation

2.1 · K and the necessitation rule

The axiom K

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

The necessitation rule RN

if ⊢ A then ⊢ □A

What

K says that necessity respects modus ponens: if the implication is necessary and the antecedent is too, so is the consequent.

RN says that the theorems of the logic are necessary: whatever is provable with no assumptions holds in every world.

Why

Because it is the strict minimum for □ to deserve its name, and exactly what Kripke semantics validates for free: K and RN hold on every frame, with no condition whatsoever on the arrows.

The system K is thus the ground floor: everything it proves, every normal modal logic proves as well.

Watch out

RN is not the formula A → □A. The rule starts from a theorem, true everywhere by nature, and declares it necessary. The formula, by contrast, would take any truth of a single world ("it is raining") and make it necessary: absurd, and invalid the moment one world sees another that differs.

2.2 · The five optional axioms

English

Five reinforcements to choose from. Part 1 showed their semantic price: each corresponds to a property of the arrows. Here they are again, from the syntax side, with their reading in one sentence.

D · necessity implies possibility

□A → ◇A · serial frames

T · the necessary is true

□A → A · reflexive frames · variant: A → ◇A

4 · the necessary is necessarily necessary

□A → □□A · transitive frames

B · the true is necessarily possible

A → □◇A · symmetric frames · B as in Brouwer

5 · the possible is necessarily possible

◇A → □◇A · euclidean frames

How

One builds a system like a menu: K is mandatory, then whichever axioms the targeted reading makes plausible.

The useful combinations have received names: K + D = D, K + T = T, T + 4 = S4, T + B = B, T + 5 = S5. The next section puts them in order.

3The ladder of systems

English

The systems nest from weakest to strongest: K at the bottom, S5 at the top. Climbing a rung means proving more theorems, and holding on fewer frames. Click a system.

Lab · the interactive ladder

System·

Axioms·

Frames·

Proves, for example·

Does not prove·

Why

Why is S5 so comfortable? Because its frames are the equivalence relations: within a block, everyone sees everyone, and stacks of modalities collapse. □◇□A is there equivalent to □A.

And why not always take it? Because some readings contradict it: knowledge is not symmetric, obligation is not reflexive. The ladder exists because usages differ.

4The zoo of modalities

English

The same mechanics plays out across entire families, each with its own operators and its system of choice. This is the grand catalogue of modal logics.

Family	Operators	Read as	Usual system
Alethic	□, ◇	necessary, possible, contingent, impossible	S5
Epistemic	Cᵢ, CK	agent i knows; the group knows in common	S4 (or even idealised S5)
Doxastic	B, CB	the agent believes; common belief. Believing is not knowing: no T	KD45
Deontic	O, P, I, F	obligatory, permitted, forbidden, optional	D
Temporal	G, F, X, U, H	always from now on, someday, tomorrow, until, always in the past	S4 and relatives
Counterfactual	A □→ B	if A were true, B would be too (given that A is not)	sphere logics
Dynamic	[a], ⟨a⟩	after every execution of a; after some execution of a	PDL

Example One arrow per reading: in the epistemic reading, wRv says "v is compatible with what the agent knows in w." In the deontic reading, "v is a world where every norm of w is respected." In the temporal reading, "v is later than w." The formalism from Part 1 does not budge an inch: only the caption on the arrows changes.

5The countermodel search engine

English

How does one prove that a system fails to derive a formula? By exhibiting a countermodel: a frame of the right class and a valuation that make it false somewhere.

This machine does it by brute force: it tries every frame of 1 to 3 worlds in the chosen class, every valuation, and displays the first countermodel it finds. Try T on "all frames," then on the reflexive ones: the countermodel vanishes, exactly as Part 1 promised.

Lab · brute force

Formula

Frame class

How

By hand, one does the same thing more cleverly: assume the formula is false in one world, and deduce from that what the arrows and valuations must contain, world by world.

If the construction succeeds, it is a countermodel. If it contradicts itself on every branch, the formula is valid. This discipline is called the method of semantic tableaux.

6Beyond normal logics

English

Everything so far describes normal logics: those that accept K and necessitation, and that fit Kripke semantics. Around them, three increasingly broader families settle for weaker rules.

Four nested families: each ring accepts one more rule. The blue core, the normal logics, is the domain of Kripke models.

Family	Accepted rule
Classical	RE: from A ↔ B, infer □A ↔ □B
Monotone	RM: from A → B, infer □A → □B
Regular	RR: from (A ∧ B) → C, infer (□A ∧ □B) → □C
Normal	K + RN (equivalently: the rule RK)

Why

Why weaken? Because some readings break K. An agent with bounded resources does not know every consequence of what it knows: the logic of its knowledge cannot be normal.

These families then keep a semantics, but a different one: neighbourhoods of worlds rather than arrows. Off the syllabus here; remember the principle, every weakening of a rule widens the family.

7The method

English

Facing a modal problem, choose your logic before you calculate. The procedure:

Identify the reading of □.

What do the worlds represent? What does an arrow say? Without an answer, no axiom can be justified.

Test each axiom against the reading.

T · "the necessary is true": yes for knowledge, no for obligation and belief. 4 · "who knows, knows that they know": positive introspection, often granted. 5 · "who does not know, knows that they do not know": negative introspection, far more disputed.

Name the system, deduce the frames.

The chosen package of axioms almost always has a name (D, S4, KD45…), and its frame class comes with it (Part 1, section 5).

To prove: derive it, or check it on the class.

Thanks to correspondence theory, proving within the system and validating on the frames amount to the same thing: pick the shorter path.

To refute: a countermodel in the right class.

Careful: a non-reflexive countermodel refutes nothing in S4. The class is part of the claim.

Remember the direction of the ladder.

More axioms equals more theorems equals fewer frames. The two counts always move in opposite directions.

8The six mistakes

Mistake 1

Confusing the rule RN with the formula A → □A. The rule necessitates theorems, true everywhere by nature. The formula would necessitate any local truth whatsoever, and would collapse every modality. No reasonable system contains it.

Mistake 2

Misplacing the negation: reading "not necessary" (¬□A, mere contingency) as "impossible" (□¬A, a prohibition). The square in section 1 exists precisely to inoculate against this confusion.

Mistake 3

Believing D is free. □A → ◇A seems obvious, but it fails at a blind world: the box is vacuously true there and the diamond false. D costs seriality, every world must have a successor. The countermodel search engine shows it in one click.

Mistake 4

Simplifying stacks of boxes without a permit. □□A is not □A in K: you need 4 to go down from □A to □□A, and T to come back up. Only in S4 does the stack flatten, and only in S5 does every sequence of modalities reduce to the last one.

Mistake 5

Taking S5 as the default for every reading. In deontic logic, T would say every obligation is fulfilled; in doxastic logic, that every belief is true. Both false. The system is chosen after the reading, never before.

Mistake 6

Reversing the direction of the ladder. S5 is "stronger" because it proves more theorems, not because it holds on more frames: it is the opposite, its frames are the rarest. Syntactic strength and semantic generality run in opposite directions.

9Test yourself

English

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

10The vocabulary in French and German

English

This formulary comes from Swiss upper-secondary schools (gymnasiums), where the subject is taught in French and German alike. Here are the terms in their original languages, for whenever you need to read a French- or German-language source.

Français	Deutsch
l'axiome de distribution (K)	das Verteilungsaxiom (K)
la règle de nécessitation	die Notwendigkeitsregel (Necessitation)
le théorème	das Theorem
le système modal	das Modalsystem
la hiérarchie des systèmes	die Hierarchie der Systeme
le carré des oppositions	das Quadrat der Gegensätze
contradictoire	kontradiktorisch
contraire	konträr
subalterne	subaltern
la modalité aléthique	die alethische Modalität
épistémique / doxastique	epistemisch / doxastisch
déontique	deontisch
temporel	temporal
contrefactuel	kontrafaktisch
la logique dynamique	die dynamische Logik
obligatoire / permis / interdit / facultatif	geboten / erlaubt / verboten / freigestellt
l'introspection positive / négative	die positive / negative Introspektion
la connaissance commune	das gemeinsame Wissen
la logique normale	die normale Modallogik
monotone / régulière / classique	monoton / regulär / klassisch
le contre-modèle	das Gegenmodell
les tableaux sémantiques	die semantischen Tableaus
la classe de cadres	die Rahmenklasse
plus fort / plus faible (système)	stärker / schwächer (System)