Five axioms and fifteen logics

Each axiom of modal logic is a property of the arrows between worlds. Add $\Box p \to p$ to the basic logic $K$ and the formulas that become valid are exactly those true on every frame in which each world sees itself; add $\Box p \to \Box\Box p$ and the frames are the transitive ones. Five axioms of this kind turn up again and again, because they say the most natural things a modality might satisfy:

• D: $\Box p \to \Diamond p$ — what is necessary is possible; every world sees at least one world.
• T: $\Box p \to p$ — what is necessary is true; every world sees itself.
• B: $p \to \Box\Diamond p$ — what is true is necessarily possible; the arrows are symmetric.
• 4: $\Box p \to \Box\Box p$ — what is necessary is necessarily necessary; the arrows are transitive.
• 5: $\Diamond p \to \Box\Diamond p$ — what is possible is necessarily possible; two worlds seen from one see each other.

Any subset of the five can be added to $K$, so there are thirty-two candidate logics. Only fifteen of them are different. The figure below is all fifteen, arranged by which contains which, and everything in it — the count, the order and the coincidences — is computed from frames rather than proofs.

This diagram is usually called the modal cube, because with a little distortion it can be drawn on the corners and edges of three nested cubes. Its bottom is $K$, valid on every frame; its top is $S5$, the logic of a necessity that means “true in every world there is”. Between them sit the logics that philosophers and computer scientists actually use — $T$ for necessity that implies truth, $S4$ for provability and intuitionistic knowledge, $KD45$ for belief, $D$ for obligation — and several that nobody uses but that the axioms produce anyway.

What the five axioms are for #

Each axiom earns its place by a reading of the box. Read $\Box p$ as “it is obligatory that $p$” and $D$ says that what is obligatory is permitted — a code of conduct that never demands the impossible — while $T$ would wrongly say that whatever is obligatory happens; deontic logic is $D$ and stops there. Read $\Box p$ as “the agent knows $p$” and $T$ says that knowledge is true, $4$ that an agent who knows something knows that it knows (positive introspection), and $5$ that an agent who does not know something knows that it does not (negative introspection); the epistemic logics run from $T$ through $S4$ to $S5$ depending on how much introspection is granted. Read it as “the agent believes $p$” and $T$ must go — beliefs can be false — while $D$ keeps beliefs consistent, which is $KD45$.

Read $\Box p$ as “$p$ is provable” and the right logic is not in the cube at all: provability satisfies Löb’s axiom, whose frames are transitive with no infinite ascending chains, a condition that no combination of these five axioms expresses. And read it as “$p$ will always be true” and transitivity is natural while symmetry is absurd — the future does not see the past — which leaves the logics with $4$ and without $B$. The cube is a menu, and each application picks the corner whose frame conditions match its reading.

How frames decide sameness #

Two sets of axioms give the same logic when they prove the same formulas. That is a question about infinitely many formulas, and it would be hopeless to settle by listing them. The frames settle it instead.

All five axioms are canonical: the frame built out of a logic’s own maximal consistent sets satisfies the axiom’s condition. A consequence is that the logic generated by any set of these axioms is exactly the set of formulas valid on every frame satisfying the corresponding conditions. So two axiom sets give the same logic exactly when they define the same class of frames — and frame classes can be compared by looking at frames.

The figures look at every frame with one, two, three or four worlds: $2 + 16 + 512 + 65{,}536 = 66{,}066$ frames, one for each possible arrow relation on each set of labelled worlds. For each of the thirty-two axiom sets the computation records which of those frames satisfy all its conditions, and groups together the sets with the same record.

The thirty-two sets fall into fifteen groups, and the groups are the same with three-world frames alone as with four: small frames already separate everything that is separate. $S5$ absorbs thirteen of the thirty-two sets; $KB5$ absorbs three; $T$, $B$ and $S4$ absorb two each; and the remaining ten logics have one name apiece.

Finding fifteen groups on finite frames proves that there are at least fifteen logics, since frames that separate two axiom sets separate their logics. That there are at most fifteen — that the sets grouped together really generate the same logic — needs the implications in the next section to hold on every frame, of every size, which a short argument shows for each. The finite computation finds the answer; the arguments confirm it.

The implications behind the collapse #

Six implications between the frame conditions account for every coincidence.

Reflexive implies serial: a world that sees itself sees something, so $T$ makes $D$ redundant. Symmetric and transitive implies euclidean: if a world sees $u$ and $v$, then $u$ sees the world by symmetry and so sees $v$ by transitivity. Symmetric and euclidean implies transitive, by a similar two-step argument, so $B$ with either $4$ or $5$ gives the other. Reflexive and euclidean implies symmetric — a world seeing $u$ also sees itself, so $u$ sees the world — and then transitive, so $T$ with $5$ is already $S5$. And serial, symmetric and transitive implies reflexive: a world sees some $u$, $u$ sees it back, and by transitivity it sees itself.

The five failures in the figure are refuted by tiny frames: a single world that sees nothing is symmetric without being serial; two worlds, one seeing the other and itself, the other seeing only itself, are reflexive and transitive without being euclidean. Every non-implication among these five conditions is refuted by a frame of at most three worlds, which is why three-world frames suffice to separate the fifteen logics.

The axioms are thus like a small algebra in which some products collapse. That is the reason the classical modal systems acquired so many names for so few logics: in the decades after C. I. Lewis named $S4$ and $S5$, several different axiomatisations of each were proposed and compared, and the frames show at a glance which of them coincide.

The implications also explain the name cube. Sort the thirty-two axiom sets by how they treat $D$ and $T$ — neither, $D$ only, or $T$ — and each of the three levels is a cube of eight corners, one for each choice of $B$, $4$ and $5$. On the bottom level, without $D$ or $T$, the eight corners give six logics, because $B$ with $4$, $B$ with $5$ and all three coincide. On the middle level, with $D$, they give five new logics and three corners that are already $S5$. On the top level, with $T$, they give only $T$, $B$, $S4$ and $S5$, because $T$ with $5$ is $S5$ whatever else is added. Six, five and four, with $S5$ shared between the upper two, make fifteen — the three cubes nested inside one another, with their corners folded together wherever an implication forces it.

Each logic also has a largest set of axioms among those that generate it — the set closed under all six implications — and naming a logic by that closed set removes the ambiguity: $S5$ is $DTB45$, $KB5$ is $B45$, $S4$ is $DT4$. The fifteen closed sets are exactly the fifteen logics, and the cube’s order is inclusion among them.

How many frames each logic allows #

Each logic is a class of frames, and the classes can be measured.

$K$ allows all 512 frames on three worlds and $S5$ only five. On four worlds the gap widens to all 65,536 frames against fifteen, and it keeps widening: the number of relations on $n$ labelled worlds is $2^{n^2}$, while the number of equivalence relations grows roughly like $(n/\ln n)^n$, far more slowly, so the share of frames that validate $S5$ shrinks towards nothing as the number of worlds grows — and since every $S5$ frame validates every logic below it, that share is the smallest in the cube. Every axiom cuts the frames down, but not independently: $T$ allows the 64 reflexive frames, and adding $D$ changes nothing, because reflexive frames are already serial. The counts are another way to see the order of the cube — a logic higher up allows fewer frames than every logic below it — and a way to see how strong each axiom is. Seriality removes a third of the frames; transitivity removes two-thirds; euclideanness, nine-tenths.

The counts also measure something about reasoning. The fewer frames a logic allows, the more formulas it validates and the fewer distinctions it can draw. In S5 nesting boxes and diamonds adds nothing — there are only six distinct modalities — while in $K$ every depth of nesting is different. A logic with fewer frames is a logic in which more things collapse.

Frames that tell the logics apart #

Every line in the cube is a strict inclusion, and each can be witnessed by a small frame on which the smaller logic’s axioms hold and the larger logic’s fail.

A single world that sees nothing separates $K$ from $D$: the formula $\Box p \to \Diamond p$ fails there, because every box is true vacuously and every diamond false. Two worlds, one seeing the other, the other seeing itself, satisfy $D$ and fail $T$. Three worlds, each seeing itself and one seeing the other two, fail transitivity and separate $T$ from $S4$. Two reflexive worlds with a one-way arrow are a preorder that is not an equivalence, and separate $S4$ from $S5$.

Each picture is also a countermodel to a formula. The frame separating $S4$ from $S5$ makes $\Diamond p \to \Box\Diamond p$ false at the world with the one-way arrow, when $p$ is true only at that world: from there $p$ is possible, but the other world, which cannot see back, has no $p$ in view — and a formula refuted by some frame of a logic is not a theorem of it. Countermodels found by search are how the cube’s strictness is usually established, and the finite model property guarantees that for these logics a search through finite frames always finds one when one exists.

The frame counts have familiar names further down the cube. The $S4$ frames are the preorders — reflexive and transitive relations — of which there are 29 on three labelled worlds and 355 on four, and every finite preorder is a set of clusters arranged in a partial order, which is exactly the structure of an order that leaves some comparisons open. The $KB5$ frames are clusters with some worlds seeing nothing; the $B$ frames, reflexive and symmetric, are simple graphs with a loop at every vertex, eight of them on three labelled worlds. Each corner of the cube is a familiar combinatorial family wearing a modal name.

Clusters: the frames of S5 #

At the top of the cube the frames are simple enough to describe completely.

An $S5$ frame is an equivalence relation: the worlds split into clusters, and within each cluster every world sees every other, itself included. On three worlds there are five ways to do that, and on four there are fifteen, the Bell numbers that count the ways of splitting a set into groups; the computation confirms that the $S5$ frames on four worlds are exactly those fifteen. In $S5$ a world’s view is its own cluster, so $\Box p$ says “$p$ holds throughout this cluster”, and that is why boxes nested inside boxes add nothing: every world in the cluster sees the same cluster.

$KD45$, now the standard logic of belief in the tradition Jaakko Hintikka began in 1962, has frames that are clusters plus outsiders: a world may lie outside every cluster provided it sees into exactly one. Belief differs from knowledge in exactly that respect — a believer’s own world need not be among the worlds compatible with what is believed, since beliefs can be false — and the frames say so in a picture: the outsider’s arrows point into a cluster that does not contain it. On three worlds there are seventeen such frames, against five for $S5$.

What finite frames cannot settle #

The computation finds fifteen classes among frames with up to four worlds, and that number is a lower bound for logics. It becomes the exact answer only together with the six implications, which hold on frames of every size by the arguments given; the computation tests them on small frames, which is a check, not a proof. Without those arguments, the possibility would remain that two axiom sets agreeing on small frames differ on some large one.

There is also the question of which logics are complete for their frames at all. For these five axioms completeness is a theorem — all are Sahlqvist formulas, whose canonical frames satisfy their conditions, as Henrik Sahlqvist showed in 1975 — but there are axioms with no property of the arrows at all, and for logics built from those, comparing frame classes says nothing about whether two axiom sets prove the same formulas. The cube is clean because its five axioms are among the best-behaved there are.

The figures also compare logics by frames, not by models, and the difference matters. A single model — a frame with a choice of which letters are true where — can satisfy an axiom’s instances without its frame having the axiom’s property, because the particular valuation may happen to avoid every counterexample. Two models that the modal language cannot tell apart can sit on frames with quite different properties. Validity on a frame means truth under every valuation, and it is only at that level that the axioms correspond exactly to the five conditions; the computation checks the conditions directly for that reason, rather than testing formulas under particular valuations.

And the cube is a small corner of a vast space. There are uncountably many normal modal logics; even the logics containing $S4$ form a lattice of uncountable size, studied in detail since the 1970s. The fifteen here are the ones generated by five particular axioms, and their simplicity is a property of that choice.

Still open: how hard each logic is to use #

The fifteen logics differ in how hard their reasoning problems are, and for some the picture is complete: deciding whether a formula is satisfiable is complete for polynomial space in $K$, $T$ and $S4$, as Richard Ladner showed in 1977, and only NP-complete in $S5$ and $KD45$, because a model can always be found with one cluster and a few outsiders. For many logics beyond the cube, the exact complexity of satisfiability is open, and even for natural extensions of these fifteen — adding a second modality, or a fixed-point operator, or axioms relating knowledge and time — the boundary between the tractable and the intractable is still being mapped. The cube is the part of the map that is finished.

Fifteen from thirty-two #

Adding any combination of the axioms D, T, B, 4 and 5 to the basic modal logic gives only fifteen different logics, because the axioms are properties of the arrows between worlds and some properties force others. Every frame with up to four worlds — 66,066 of them — sorts the thirty-two combinations into those fifteen; six short implications explain every coincidence, from reflexive implying serial to serial, symmetric and transitive implying reflexive; tiny frames separate every neighbouring pair; and at the top, $S5$’s frames are the ways of splitting worlds into clusters, five on three worlds and fifteen on four.