The axiom is the shape of the graph

Ordinary logic has connectives that combine statements, each of them a function from truth values to truth values. Add one that does something else: an operator $\square$ read as necessarily, applied to a statement to make another statement. The immediate problem is that nothing in the truth tables says what it means.

Is $\square p \to p$ true? If necessarily means provably, arguably; if it means obligatorily, plainly not. Is $\square p \to \square\square p$ true? That depends on what necessity is about, and for a century there was no way to settle such questions except by arguing about the words.

The answer, from 1959, is that each axiom corresponds to a property of a graph, and the argument about words becomes a question about arrows.

Worlds, arrows, and one operator #

A frame is a set of points, called worlds, with arrows between them. A model adds an assignment saying which statements are true at which worlds. Then

$\square \varphi$ is true at a world $w$ exactly when $\varphi$ is true at every world that $w$ points to.

and its companion $\Diamond\varphi$ — possibly — is true at $w$ when $\varphi$ holds at some world $w$ points to.

That is the whole semantics, and the interpretations follow from what the arrows are taken to be. Arrows meaning is a possible future of make $\square$ into always will be. Arrows meaning is consistent with what is known at make it is known. Arrows meaning is a permitted continuation of make it is obligatory. One definition, and the disagreements move into the graph where they can be examined.

Each axiom is a property of the arrows #

Now the result that makes the subject a subject. Take the axiom $\square p \to p$ — whatever is necessary is true. It holds at every world of a frame, under every assignment of truth values, exactly when every world points to itself.

One direction is easy: if $w$ points to itself and $\square p$ holds at $w$, then $p$ holds at every world $w$ points to, including $w$. The other direction is the interesting one, and it is a construction: if $w$ does not point to itself, make $p$ true at every world except $w$. Then $\square p$ holds at $w$ — every world it points to has $p$ — and $p$ does not. The axiom fails.

The same pattern runs down the list, and the correspondences are the reason the axioms have the names they do:

The hero figure decides all twenty-five cells by brute force and compares each verdict with the corresponding property of the arrows, checked on the frame itself. A disagreement between the two would mean the correspondence was wrong, and the figure would refuse to draw.

What that buys #

The correspondence converts a question of interpretation into a question with an answer.

Somebody who says necessity is provability in arithmetic is asserting something about the arrows, and the assertions can be checked. Provability is transitive, so the axiom $\square p \to \square\square p$ holds; it is not reflexive, because a system can prove something false about itself only if it is inconsistent, and indeed the sentence that says it has no proof is exactly a place where $\square p \to p$ fails as a schema. So provability logic keeps the transitivity axiom and drops the reflexivity one, and that is not a stipulation — it is forced.

Somebody who says necessity is obligation is asserting the arrows are serial — every situation has at least one permitted continuation — and nothing more. So obligation logic keeps only $\square p \to \Diamond p$: what is obligatory is permitted. Dropping reflexivity is what makes it possible to say something is obligatory and not the case, which is the whole point of a logic of obligation.

Somebody who says necessity is knowledge has the hardest case, because the natural axioms make knowledge reflexive, transitive and euclidean at once, which forces the arrows to be an equivalence — and the consequences of that are strong enough to be controversial. An equivalence relation says an agent knows exactly which block it is in and nothing finer, so whatever is not known is not known to be not known either, which is a strong claim about an agent and one that a system asked about itself has good reason to doubt.

The other direction: reading a frame off a formula #

The correspondence has been used one way so far — an axiom is assumed and a property of the arrows follows. It runs the other way as well, and that direction is where it earns the word correspondence.

Take a frame and ask which of the five axioms hold on it. The answer is a subset of the five, and it is decided by five checks on the arrows rather than by any search over formulas. A frame that is reflexive and transitive validates the first two and, unless it is also symmetric, not the third. So a class of frames determines a logic, and the logic can be read off the geometry.

That makes it possible to design a logic. Decide what the arrows should mean, work out which properties they have, and the axioms follow — rather than choosing axioms and hoping the resulting system describes the intended thing.

The failure in the figure is worth reading, because it is the clearest illustration of what an arrow’s direction does. The axiom says: if $p$ holds here, then from anywhere reachable, $p$ is possible. That needs a way back. On a one-way chain there is none, so a world that has $p$ is invisible from its own future, and the axiom breaks at exactly the place where the return path is missing.

Where the tower stops #

There is a question the semantics settles immediately and that is almost unanswerable without it: how many distinct modalities are there?

The language can build $\square$, $\square\square$, $\square\square\square$ and so on, and $\Diamond\square$, $\square\Diamond$, and every other string. Are these different statements or the same one?

On a frame with no special properties, every string is a different statement and the language has infinitely many modalities. On a frame that is an equivalence — every world sees a whole block and nothing else — the tower collapses at the first step: $\square\square p$ and $\square p$ are true at exactly the same worlds, under every assignment, and there are only six distinct modalities in the entire language.

That is a substantial fact about a logic, and it is decided here by evaluating a few hundred cases. Deciding it syntactically — proving in the axiom system that $\square\square p \leftrightarrow \square p$ — is possible and is a great deal more work.

Six modalities, and why that number #

The collapse on an equivalence relation is worth carrying out, because the count that results is small enough to list and the listing explains the whole phenomenon.

Where the arrows are an equivalence, every world sees exactly its own block and nothing else. So $\square p$ at a world means p holds throughout this block, which is a property of the block rather than of the world. Applying $\square$ again asks whether that block-property holds throughout the block — which it does or does not, uniformly, so $\square\square p$ and $\square p$ agree everywhere.

The same argument makes $\Diamond\Diamond p$ agree with $\Diamond p$, and $\square\Diamond p$ with $\Diamond p$, and $\Diamond\square p$ with $\square p$. Every string of boxes and diamonds therefore reduces to its last symbol, and the modalities available are: nothing, $\square$, $\Diamond$, and the three negations of those. Six.

On a bare chain nothing collapses. $\square p$ says p holds at the next world; $\square\square p$ says p holds two along; and those are different claims about different worlds, so the tower is infinite and the language has infinitely many distinct things to say. The figure decides which of the two situations holds by evaluating three depths at every world under every assignment, and the answer for each frame is a fact about the frame.

The moral is the one the whole correspondence keeps producing. A question about the language — how many modalities are there — turns out to be a question about the arrows, and the arrows are finite and can be looked at.

Where it fails, and what it needs #

Not every axiom corresponds to a frame property. The correspondence is a happy fact about the standard five, not a theorem about all formulas. There are modal axioms whose class of frames cannot be described by any condition on the arrows expressible in first-order terms, and there are frame properties no modal formula picks out. The general theory of which is which is a subject of its own.

A frame property is not the same as a proof system. Showing an axiom holds on a class of frames is one half; showing that everything holding on that class is provable from the axiom is the other, and it needs a construction — the canonical model — that this page does not draw. Both halves together make a completeness theorem, and there are logics with the first and not the second.

The valuations are finite here because the frames are. Checking an axiom at every world under every assignment means $2^n$ assignments for $n$ worlds, which is a search this site is happy to perform at four or five worlds and could not perform at forty. A general claim about all frames is not established by any of these searches; what they establish is the correspondence on the frames drawn.

A logic is a class of frames, and several classes give the same logic. The correspondence sends a property to an axiom, and different properties can validate the same formulas — the finite frames of a class often validate exactly what the whole class does, which is what makes a search over small frames informative at all. That is a theorem about each logic rather than a general fact, and where it fails a small search proves nothing.

And one propositional letter is not always enough. The countermodels above use a single letter $p$, which suffices for the five axioms drawn. Some correspondences need more, and a search over assignments to one letter would report a spurious agreement.

Where it came from #

Modal logic as a formal system is C. I. Lewis’s, from 1918, and for forty years it had axioms and no semantics. Systems were proposed, named S1 through S5, and compared by which theorems they proved — with no way to say what any of them was about and no way to show a formula unprovable except by an ad hoc construction.

Saul Kripke published the semantics in 1959, at nineteen. The move is exactly the one this essay is built on: introduce a set of worlds and a relation, define truth at a world, and the axioms become properties. Within a few years every one of Lewis’s systems had a completeness theorem and the comparisons became easy.

It is worth recording that Kripke was not quite first. Similar ideas appear in Kanger’s and Hintikka’s work of the same period, and Carnap had something related in the 1940s. What Kripke supplied was the relation — earlier attempts let every world see every other, which collapses the interesting distinctions, and the arrows are what make the correspondence possible.

The same semantics turned out to fit a logic with no modal operator at all: the middle that is not excluded reads the same worlds and arrows as stages of knowledge, and gets intuitionistic logic. One picture, two subjects, and a great deal of the interest in modal logic since has come from the second.

What the pictures cannot show #

The frames drawn here have three to five worlds, because a picture of arrows becomes unreadable above that. Nothing about the correspondence is limited to small frames, and nothing in the figures demonstrates the general statement.

The searches are over assignments to one propositional letter. A reader who takes a green cell in the table to mean “this axiom is valid on this frame” is right; a reader who takes it to mean “the search would have found any counterexample” needs the clause about more letters.

And no figure here shows a logic being complete. The correspondence is one half of the standard story, and it is the half a picture can carry: an axiom evaluated on a frame is a finite check, and a proof system reaching everything valid is a construction over all frames at once.

The ladder from here #

Below: a formula is a corner of a cube, where a truth assignment is a point and a connective is a function on them, and the middle that is not excluded, where the same frames carry a different logic. Sideways: two worlds that both obey the rules, where a set of axioms fails to pin down a structure, and the tree that closes, where validity is decided by a search rather than by a model. Above: completeness by canonical models, Sahlqvist’s theorem on which axioms correspond, and the provability logic in which the fixed points are unique.

What is worth carrying away #

An argument about what a word means can sometimes be replaced by an argument about a picture, and the replacement is worth making because pictures can be checked. Is necessity transitive has no answer; are the arrows transitive has one, once the arrows have been specified, and specifying them is what the disputants were failing to do.

The general move is to give an interpretation a mathematical home. Once necessity lives on a graph, every disagreement about it becomes a disagreement about which graphs are the right ones, and that is a disagreement two people can settle by writing down what they mean.