The axiom with no property of the arrows

The first rung’s table was assembled one row at a time: here is $\Box p \to p$ and here is reflexivity, here is $\Box p \to \Box\Box p$ and here is transitivity, each pairing checked by hand. The obvious question is whether the pairing is a procedure.

It is, for a large class, and Sahlqvist’s theorem of 1975 says so: an axiom of a stated syntactic shape has a first-order condition on the arrows computable from it by a mechanical substitution, and the axiom is valid on exactly the frames satisfying that condition.

The recipe, in outline #

The substitution algorithm is worth seeing even without its side conditions, because the idea is a single move repeated.

Take $\Box p \to \Box\Box p$ and suppose it fails at a world $w$ on some frame. Then $\Box p$ holds at $w$ and $\Box\Box p$ does not, so there are worlds $v$ and $u$ with $wRv$, $vRu$, and $p$ false at $u$.

Now choose the valuation to be as unhelpful as possible: let $p$ be true exactly at the worlds $w$ can reach. That is the minimal valuation making the antecedent true, and it is the whole trick — the algorithm substitutes it for the letter and the formula’s variables disappear.

With that valuation, $\Box p$ holds at $w$ by construction, and $p$ false at $u$ means $w$ cannot reach $u$. So the failure says: there exist $v, u$ with $wRv$, $vRu$, and not $wRu$ — which is the negation of transitivity.

The letter has been eliminated and what is left is a sentence about the arrows. That is the algorithm: replace each propositional letter by the minimal valuation making the antecedent hold, and read off the condition.

Why the sweep is the right check #

The recipe’s output could be wrong, and the figure does not take it on trust. For each axiom it enumerates every relation on one, two, three and four worlds — sixty-six thousand and sixty-six of them — and for each asks two questions independently.

Is the axiom valid on this frame? That means checking every valuation of its letter at every world, which for four worlds is sixteen valuations.

Does the stated condition hold? That is a direct test on the relation.

The figure refuses to draw unless the two answers agree at every single frame. A correspondence claimed and a correspondence swept are two different things, and only the second would catch a recipe applied wrongly.

The counts in the last column are worth reading. Reflexivity holds on $4{,}165$ of the frames, seriality on $50{,}978$, transitivity on $4{,}180$, symmetry on $1{,}098$, the euclidean condition on $354$. Those are the counts of relations with each property, and they arrive as a by-product of the check.

The axiom the recipe misses #

The last row is $\Box\Diamond p \to \Diamond\Box p$, called McKinsey’s axiom, and it is not of Sahlqvist shape.

The reason is visible in the algorithm. The minimal-valuation trick needs the antecedent to be built from letters under boxes with no diamonds in the way, so that the smallest valuation making it true is a well-defined set of worlds. In $\Box\Diamond p$ the letter sits under a diamond inside a box, and there is no smallest valuation: making $\Diamond p$ true at each successor can be done in many incomparable ways.

So the recipe does not apply, and the question becomes whether some other condition works. The figure answers it negatively over a stated catalogue: for each of eight standard conditions it looks for a frame satisfying the condition and refuting the axiom, or the reverse, and finds one every time.

Then it does something stronger. It searches for two frames of the same size that agree on every condition in the catalogue and disagree about the axiom, and it finds a pair. That is a demonstration that the catalogue is insufficient, which is more than eight separate mismatches.

Doing one substitution completely #

The recipe is easier to trust after one row is run end to end, so here is $\Diamond\Box p \to \Box\Diamond p$, which produces confluence.

Suppose it fails at $w$. Then $\Diamond\Box p$ holds — so there is $v$ with $wRv$ and $\Box p$ true at $v$ — and $\Box\Diamond p$ fails, so there is $u$ with $wRu$ and $\Diamond p$ false at $u$.

The minimal valuation making the antecedent’s inner part true is: let $p$ hold exactly at the successors of $v$. Then $\Box p$ is true at $v$ by construction. And $\Diamond p$ false at $u$ means no successor of $u$ is a successor of $v$.

So the failure says: there are $v$ and $u$ both reachable from $w$ with no common successor. Negate it and the condition is that any two worlds reachable from one have a common successor — confluence, sometimes called the Church–Rosser property.

Every step was mechanical once the minimal valuation was chosen, and choosing it is the only creative act in the procedure. The figure then checks the result against every relation on up to four worlds, and confluence holds on $24{,}598$ of them.

What the search shows and what the theorem says #

The distinction is worth being careful about, because the figure’s conclusion is weaker than the true statement and the caption says so.

The search establishes: no condition in this particular list of eight defines McKinsey’s axiom.

The theorem establishes: no first-order condition whatever on the accessibility relation defines it — not one anybody has written, and not one anybody could.

The gap between those is not closed by a bigger catalogue, because the space of first-order conditions is infinite. What closes it is an argument about first-order logic itself, and the standard one uses the same invariance the second rung is about: construct two frames that are elementarily equivalent — no first-order sentence separates them — on one of which the axiom is valid and on the other not. Since a first-order definition would separate them, none exists.

A search can refute a candidate and cannot exhaust a language, and running the search anyway is worth it because it makes the shape of the failure concrete before the abstract argument arrives.

What “defines” means here #

Two notions are in play and conflating them makes the theorem sound stranger than it is.

An axiom defines a class of frames: those on which it is valid. Every axiom does this, McKinsey included, and the class is perfectly well specified.

The question is whether that class is first-order definable — whether some sentence in the language of one binary relation picks out exactly those frames. For the seven Sahlqvist axioms it is, and the recipe produces the sentence. For McKinsey it is not.

So the axiom is not defective and its class is not mysterious. What is true is that modal logic and first-order logic, applied to the same frames, have overlapping but different reach: modal formulas define frame classes, first-order sentences define frame classes, and neither collection contains the other.

The second rung showed one half of that non-containment — irreflexivity is first-order and not modal. This rung shows the other half.

Two frames that no first-order sentence separates #

The abstract argument is worth an outline, since it is the one that actually settles the case and it uses a standard tool.

Take the frame whose worlds are the natural numbers with $mRn$ when $m < n$, and take a second frame obtained by adding a copy of the integers above it — worlds $0, 1, 2, \ldots$ followed by a full copy of $\mathbb{Z}$, ordered so everything in the tail is above everything in the front.

Those two are elementarily equivalent: no first-order sentence about the order relation distinguishes them, which is the standard fact that first-order logic cannot express well-foundedness. Their difference is that one has an infinite descending chain in its upper part and the other does not.

McKinsey’s axiom is valid on one and not the other, because its truth turns on whether every world can reach one whose possibilities are settled — and that is exactly what the descending chain destroys.

So a first-order definition of the axiom would separate two frames no first-order sentence separates, which is a contradiction. The same construction settles several other non-definability questions, and it is the standard shape: exhibit an elementary equivalence the modal formula sees through.

That the argument needs infinite frames is not incidental. On finite frames every modally definable class is first-order definable, essentially because a finite frame can be described completely by a first-order sentence. The whole phenomenon lives at infinity, which is why the sweep over small frames could only ever be suggestive.

The conditions, and where each comes from #

The seven that work are worth listing with their readings, since each is a familiar property arriving from a formula.

$\Box p \to p$ gives reflexive: what is necessary is true, so a world must see itself.

$\Box p \to \Diamond p$ gives serial: necessity implies possibility, so every world must see something.

$\Box p \to \Box\Box p$ gives transitive: what is necessary is necessarily necessary.

$p \to \Box\Diamond p$ gives symmetric: what is true is necessarily possible.

$\Diamond p \to \Box\Diamond p$ gives euclidean: what is possible is necessarily possible.

$\Box\Box p \to \Box p$ gives dense: between any two related worlds there is a third.

$\Diamond\Box p \to \Box\Diamond p$ gives confluent: two worlds reachable from one have a common successor.

Each of those is a one-line sentence about arrows produced by a mechanical substitution, and every one is checked against the axiom over the whole sweep. The mechanical part is what makes the theorem worth having: without it each row is a small exercise, and there are as many rows as there are axioms anybody might propose.

Sahlqvist’s shape, stated #

The class the theorem covers can be described, and it is broad enough to include essentially every axiom in use.

A Sahlqvist antecedent is built from letters and negated letters using conjunction, disjunction, diamonds and boxes, subject to the restriction that no positive occurrence of a letter sits inside a diamond that sits inside a box. A Sahlqvist formula is such an antecedent implying a formula positive in every letter.

All seven axioms above qualify. McKinsey’s does not, and it fails on exactly the restriction named — its $p$ sits under a diamond under a box.

The theorem then says two things at once: the frame condition is first-order and computable, and the logic axiomatised by such formulas is complete for the frames satisfying it. The second half is what makes the theorem a workhorse: it removes the need for a separate completeness proof of the kind the previous rung constructs for every new axiom.

What McKinsey’s axiom is about #

It is worth saying what the axiom means, since it is otherwise an arbitrary string.

$\Box\Diamond p \to \Diamond\Box p$ reads: if $p$ is possible from every world in view, then some world in view has $p$ necessarily. Informally, if something can always happen then somewhere it must.

That is a statement about being able to settle a matter, and the frames it holds on are, roughly, those where every world can reach a world that is either a dead end or a self-loop — an atomic frame, where possibilities eventually resolve. That description is second-order rather than first-order, which is the theorem, and the informal reading makes the shape of the failure plausible: it quantifies over what is eventually reachable, and eventually is not first-order.

An axiom asking about the eventual behaviour of arrows is asking for something first-order logic cannot say about arrows, which is the same limitation that stops first-order logic expressing connectedness or well-foundedness — and an infinite tree’s infinite path is where that limitation is usually first met.

Why the theorem is used constantly #

Sahlqvist’s result is one of the few in the subject that gets applied rather than admired, and it is worth saying what the application looks like.

Somebody proposes a modal logic — a set of axioms — for some purpose: reasoning about time, about knowledge, about what a program does. Two questions follow immediately. What do the frames look like? And is the logic complete for them?

Without the theorem each question needs its own work: the first a substitution done by hand and checked, the second a canonical model construction verified against the axioms. With it, both are settled by inspecting the syntax of the axioms — if they are of Sahlqvist shape, the frame condition is computed and completeness is free.

Nearly every logic anybody proposes is of that shape, because the shape is what people naturally write. So in practice the theorem turns two theorems per logic into a syntactic check, and the logics it does not cover are the ones known by name — McKinsey’s, and the provability logic of the next rung.

A theorem that removes routine work for the common case and leaves the exceptions named is the most useful kind, and the exceptions being few and famous is what makes the situation tidy rather than merely partial.

What the pictures cannot show #

The sweep is a number. Sixty-six thousand relations checked, with two independent answers agreed at every one, is one line of the caption. What a reader sees is a table of eight rows.

The pair witnessing the failure is not drawn. The generator finds two frames agreeing on every catalogue condition and disagreeing about the axiom, and reports that it found them. Drawing them would show two small graphs and the disagreement is a fact about valuations over them.

And the theorem itself is not the search. Everything the figure establishes is about frames of at most four worlds and a catalogue of eight conditions. The statement that no first-order condition defines the axiom is a theorem about all frames and all conditions, and it is proved elsewhere by an argument no drawing carries.

Where the ladder goes next #

Three rungs have treated modal logics as proposals about what necessity might mean, checked against classes of frames. The last one is different: there is a modal logic that is not a proposal at all but a complete description of a fact about arithmetic — what a formal system can prove about its own proofs — and its frames turn out to be the transitive ones with no cycles.

Sideways: the first rung’s table is what this rung mechanises, and bisimulation is the other direction in which the two languages fail to contain each other.

What is worth carrying away #

A correspondence that holds in every checked case can still fail to be a theorem, and the difference is worth finding out about early.

Seven axioms, seven conditions, all verified over sixty-six thousand frames — and the eighth axiom has no condition at all. Nothing about the first seven predicted that, and no amount of further checking of the first seven would have found it.

There is a second lesson about where to look for a counterexample. The failure here lives at infinity, on frames with infinite descending chains, and every finite check agreed with every candidate condition. A property that holds in every small case and fails at infinity is the standard shape of such a failure, and the standard reason a search cannot settle a definability question.

What decides such questions is a structural property of the axioms rather than evidence about them, and Sahlqvist’s contribution is a syntactic test that says in advance which axioms will behave. A test that can be applied by looking at the formula is worth a great deal more than a table of successful cases, and it is worth more still because it is honest about its own boundary: an axiom failing the test is not thereby undefinable, it is merely outside what the recipe guarantees, and deciding it needs the separate argument this rung sketches.