Two diagrams the language cannot tell apart

The first rung read each modal axiom as a property of the arrows. The obvious follow-up is to ask what else the language can say, and the answer is unusually clean: it can say exactly what a bisimulation preserves, and nothing more.

A bisimulation is a relation between the worlds of two models. Related worlds must agree on every propositional letter, and every arrow from one of them must be answerable by an arrow from the other landing on a related world — in both directions. Where such a relation exists linking two worlds, they are indistinguishable to the language.

The three clauses #

Writing $w \sim v$ for the relation between a world of one model and a world of the other, the conditions are:

Atoms. $w$ and $v$ satisfy exactly the same propositional letters.

Forth. For every $w'$ reachable from $w$ there is a $v'$ reachable from $v$ with $w' \sim v'$.

Back. For every $v'$ reachable from $v$ there is a $w'$ reachable from $w$ with $w' \sim v'$.

That is all. The clauses say the two worlds look the same now and can keep looking the same forever, and the recursion in forever is what makes the definition strong enough to be exactly right.

The relation is not required to be a function, an injection, or anything else structural. Two models of wildly different sizes can be bisimilar, and the hero’s upper pair — two worlds against four — is the smallest example.

Why it is exactly the right notion #

Two claims are needed and they pull in opposite directions.

Bisimilar implies indistinguishable. By induction on the formula. For a letter it is the atoms clause. For a conjunction or a negation it follows from the parts. For $\Box\varphi$: if $\Box\varphi$ holds at $w$ and $v'$ is reachable from $v$, then Back gives a $w'$ reachable from $w$ with $w' \sim v'$; $\varphi$ holds at $w'$ by assumption, so by induction at $v'$; so $\Box\varphi$ holds at $v$.

Indistinguishable implies bisimilar, for finite models. Take the relation satisfies the same formulas. It obviously satisfies Atoms, and Forth holds because if some successor $w'$ of $w$ had no matching successor of $v$, then for each successor $v'$ of $v$ there is a formula true at $w'$ and false at $v'$; conjoining those finitely many formulas and putting a diamond in front gives a formula separating $w$ from $v$.

The second argument uses finiteness twice, and the failure on infinite models is genuine: there are infinite models that satisfy the same formulas and are not bisimilar. Repairing that needs modal formulas of infinite length or a saturation condition, and it is the standard place where the finite and infinite theories part — the same division a proof system meets when its models grow.

The pair with no bisimulation #

The lower pair in the hero is the smallest interesting failure, and the reason it fails is worth tracing.

The left model has one world with two successors, both dead ends. The right has one world with two successors, each of which has a successor of its own. No letters anywhere.

Try to relate the two starting worlds. Forth requires each right-hand successor to be matched by a left-hand one; the left-hand ones are dead ends and the right-hand ones are not; so the matched pair fails Forth at the next step, because the right-hand successor has an arrow and the left-hand one has none.

The failure propagates one step down, which is exactly what a formula of modal depth two detects. The figure searches formulas in order of size and finds $\Box\Diamond\top$: true at the right-hand root because every successor has a successor, false at the left-hand root because neither does.

What the search actually does #

The figure evaluates every formula up to the drawn depth on both models of each pair, and the two halves of that do different jobs.

On the bisimilar pair it checks agreement — the relation was computed by refining, and the formula sweep is an independent confirmation that the refinement produced a genuine bisimulation. Two routes to one claim, and the second would catch a bug in the first.

On the non-bisimilar pair it finds the separating formula rather than quoting one, taking the first in the enumeration that disagrees. That the smallest witness is found rather than chosen is the difference between a demonstration and an illustration.

The enumeration is capped, and the cap is stated in the generator’s own comment: building every conjunction and disjunction of everything below squares the pool at each level — two, sixteen, five hundred and seventy-six, six hundred thousand — so a capped pool taken in size order is used instead. It still finds the smallest separating formula, because that formula is small.

Bisimulation is an equivalence, and refining finds the largest one #

Two structural facts make the notion usable, and both are worth stating because the definition alone does not make them obvious.

The union of bisimulations is a bisimulation. Each clause is an existential requirement, so a pair satisfying it in one relation still satisfies it in a larger one. Therefore there is a largest bisimulation between any two models — the union of all of them — and two worlds are bisimilar exactly when that largest relation links them.

It can be computed by refining. Start with every pair agreeing on the letters and repeatedly delete any pair failing Forth or Back with respect to the current relation. The relation shrinks, so on finite models the process stops, and what it stops at is the largest bisimulation.

That is what the generator does, and the reason the loop terminates is the reason it is the right answer: deleting a pair can only make other pairs fail, never make a failing pair succeed, so the fixed point reached is the greatest one.

Refining to a fixed point is the standard shape for computing a greatest relation, and the same algorithm under another name minimises a finite automaton by merging states nothing can tell apart. Two objects that no observation separates are one object, and finding the coarsest such partition is what both computations do.

The game reading #

There is a second description that is more memorable and says the same thing.

Two players, on two models with a marked world each. Spoiler picks a model and moves along an arrow from its marked world; Duplicator must move along an arrow in the other model. The marked worlds update, and the round repeats. Duplicator loses if the letters ever disagree, or if Spoiler makes a move Duplicator cannot answer.

Duplicator has a strategy surviving $n$ rounds exactly when no formula of modal depth $n$ separates the two worlds, and a strategy surviving forever exactly when they are bisimilar.

The same device settles first-order expressive power, where the moves pick elements rather than following arrows and the rounds count quantifier depth. The two games are close relatives and the modal one is the more restricted: Spoiler must move along an arrow rather than pointing anywhere at all, which is exactly the sense in which modal logic sees less. The restriction is what buys decidability: a language that can say anything about a structure cannot be decided, and one that can only follow arrows can.

What the language cannot say #

The characterisation immediately settles a list of questions that would otherwise each need their own argument.

Modal logic cannot count worlds. The bisimilar pair has two worlds and four, so no formula distinguishes sizes.

It cannot say a world has exactly two successors. Duplicating a successor produces a bisimilar model, so any formula true of one is true of the other.

It cannot express irreflexivity. A reflexive point and an infinite chain of distinct points are bisimilar, so no formula holds at one and fails at the other. That is worth pausing on, since the first rung read axioms as frame properties and irreflexivity is a perfectly good frame property with no axiom.

And it cannot express connectedness, or that an arrow chain terminates, for the same kind of reason. Each of those would separate bisimilar models.

Depth is what the game counts #

The rounds of the game count something specific, and it is worth naming because it is the quantity every statement here is graded by.

The modal depth of a formula is the maximum nesting of boxes and diamonds in it: $p$ has depth zero, $\Box p$ depth one, $\Box\Diamond\top$ depth two. It is not the length — a huge conjunction of letters still has depth zero — and it is exactly the number of arrows a formula can look along.

So Duplicator surviving $n$ rounds means no formula of depth $n$ separates the worlds, and a formula of depth $n$ is precisely a description of the first $n$ steps of the arrow structure. Depth is distance, and the language sees a bounded distance for each formula and every distance across all of them.

That reading explains why the lower pair in the hero needs a formula of depth two. The two models agree completely on what is reachable in one step — both roots have successors, none of which carries a letter — and disagree on the second step. Duplicator survives one round and loses the second.

It also explains the finite-model repair of van Benthem’s theorem. On a finite model there are only finitely many formulas of each depth up to equivalence, so agrees at every depth can be turned into a single formula, and the equivalence-implies-bisimilar direction goes through.

Which fragment of first-order logic it is #

The precise statement is van Benthem’s, and it is the cleanest theorem in the subject.

Every modal formula translates into a first-order formula about the arrow relation, with one free variable: $\Box\varphi$ at $x$ becomes for every $y$ with $xRy$, $\varphi$ at $y$. So modal logic is a fragment of first-order logic, and the translation is mechanical.

Van Benthem’s theorem is the converse. A first-order formula with one free variable is equivalent to the translation of a modal one exactly when it is invariant under bisimulation.

So the modal language is not an arbitrary restriction of first-order logic; it is the whole bisimulation-invariant part of it. Every property a modal formula can express is bisimulation-invariant, by the induction above, and every bisimulation-invariant first-order property is modally expressible, by van Benthem.

That is why the language has good properties. Its decidability, its finite model property, and its robustness under model transformations all trace to the same source: it sees only what a bisimulation preserves, and bisimulation-invariant properties are the well-behaved ones.

The two tables read together say something the first rung could not. An axiom corresponds to a frame property; a frame property is modally expressible only when it is preserved by the transformations bisimulation allows; and irreflexivity, which is a perfectly ordinary property of arrows, is not. So the correspondence of the first rung runs one way and not the other, and this rung is why.

Unravelling, and the tree that is always available #

One consequence is used constantly and deserves naming.

Every model is bisimilar to a tree. Take a world $w$ and build the model whose worlds are the finite paths from $w$, with an arrow from a path to any one-step extension and the letters copied from the endpoint. The map sending each path to its endpoint is a bisimulation.

So no modal formula can tell any model from its unravelling, and any question about satisfiability can be asked about trees only. That is the standard first move in half the proofs in the subject: assume the model is a tree, since it costs nothing.

A restriction that is free is the most valuable kind, and this one is free precisely because trees are as expressive as anything, in the only sense the language can measure. It also explains the irreflexivity item above: unravelling a reflexive point gives an infinite chain with no loops at all.

Where the notion escaped from #

Bisimulation was invented three times in a decade, by people who were not talking to each other, and the coincidence says something about the notion.

Van Benthem introduced it in 1976 for exactly the purpose above: characterising the modal fragment of first-order logic. Park and Milner arrived at it around 1980 in the theory of concurrent processes, where the question was when two programs behave the same — and the answer was that they should be able to answer each other’s steps, forever. Aczel used it in 1988 to build a set theory in which sets can contain themselves, where two such sets are equal exactly when a bisimulation relates their membership graphs.

Three subjects, one definition. The common structure is that in each case the objects are described by what can be observed of them step by step, and two objects should count as the same when no sequence of observations separates them.

That is a genuinely useful heuristic. Wherever a theory’s objects are inspected by repeated local moves, the right notion of sameness is a bisimulation, and the wrong ones are isomorphism — too fine, since it counts things the language cannot — and equality of observations at each finite depth — too coarse, as the infinite counterexample shows.

Why the notion is the right size #

One more remark, because there is a natural objection to bisimulation being the answer.

The objection: why not simply say two worlds are equivalent when they satisfy the same formulas? That is a perfectly good relation and it is decidable on finite models.

The reason is that the formula-based relation is defined in terms of the language, so it cannot be used to say anything about the language without circularity. Bisimulation is defined purely in terms of the models — arrows and letters — and mentions no formulas at all. That is what makes the equivalence between them a theorem rather than a definition.

A characterisation is only useful when its two sides are stated in independent vocabularies. Here one side is syntactic and the other is structural, and every application of the theorem uses that independence: to show something is inexpressible, build a bisimulation, which is a construction on models and needs no formula at all.

What the pictures cannot show #

The bisimulation itself is not drawn. The relation between the two upper models is computed by refinement in the generator and reported through its consequences; a picture of dotted lines between two diagrams would be readable and would not be checked.

The formula sweep is a count. Seven hundred and seventy-two formulas evaluated on both sides is the caption’s number, and the reader sees the conclusion rather than the sweep.

And the theorem is about all formulas. The figure checks up to a stated depth. That the agreement continues forever is the induction above, and no finite search reaches it.

Where the ladder goes next #

Bisimulation says what the language can distinguish among models that exist. The next rung asks where models come from, and answers that they can be built out of the syntax itself: worlds made of sets of sentences, with an arrow wherever the boxed commitments line up, and the surprising fact that in such a model a formula is true exactly where it was assumed.

Sideways: the first rung is where the frames came from, and the first-order game is the same device measuring a wider language.

What is worth carrying away #

The useful description of a language is not what it can say but what it cannot tell apart.

Listing a language’s expressible properties is an open-ended job with no natural stopping point. Naming the equivalence it respects is a single definition, and it settles every question of the form can this be expressed at once, in both directions.

The pattern generalises well beyond modal logic. First-order logic respects elementary equivalence, measured by one game; modal logic respects bisimulation, measured by another; and in each case the invariance is easy to state and the expressibility questions it answers are not.

There is a second habit in the same place, and it is about what a negative result costs. Proving that a language can say something takes one formula. Proving that it cannot takes an argument about all formulas, and the only economical way to run such an argument is to find an invariance the language respects and an example that violates it. Two structures that a system cannot separate are the standard tool for every impossibility of this kind, and a bisimulation is the version of that tool cut to this language’s size.