How many worlds a formula can need

A model can be enormous and a formula can be small, and the gap between those two facts is where this rung lives. Nothing stops a modal formula from being satisfied in a model with infinitely many worlds — take any model at all, and add a thousand worlds nothing points at, and the formula is still true where it was. The question is whether it has to be. If every satisfiable formula is satisfiable somewhere small, and small can be bounded by something read off the formula, then modal validity can be tested by enumeration, and a logic that looked like a claim about all models becomes a finite search.

The construction that does it is called filtration, and it is the reverse of the one that builds worlds out of sentences. There, nothing was given and a model was manufactured from the syntax. Here a model is given — any model, of any size — and the syntax is used to decide which of its worlds were ever distinguishable in the first place.

What a formula can ask about #

Fix a modal formula. Take its subformulas, and the subformulas of those, down to the letters. The result is a finite set closed under subformulas, and it is the whole of what the formula can ask about: every step of evaluating it consults one of those, at one world or another.

Call that set the closure. For $\Box\Box p$ the closure is $\{p, \Box p, \Box\Box p\}$, three formulas. For a formula with twelve subformulas the closure has twelve. The point is not which formulas are in it but that the count is finite and known before any model is looked at.

Now ask what a world in a model is, as far as that closure can see. It is an answer to each question: true or false for each of the closure’s formulas. That is a vector of bits, one per formula, and the number of possible vectors is two to the power of the closure’s size. Two worlds carrying the same vector are, to that formula, the same world. No sequence of steps in evaluating the formula can begin at one and end differently than at the other, because every step reads only the closure.

That is the whole idea. What remains is to check that identifying such worlds actually produces a model in which the formula still says what it said — which is not obvious, since the identification also has to decide where the arrows go.

Identifying the worlds it cannot tell apart #

The worlds of the new model are the classes: one for each vector that some world of the original actually realises. There are at most $2^{|\Sigma|}$ of them for a closure $\Sigma$, and usually far fewer, because most vectors are not realised by anything.

The letters are easy. A letter is in the closure, so all worlds of a class agree about it, and the class inherits the answer without ambiguity.

The arrows are the delicate part, because the original model’s arrow relation does not descend to the classes on its own. The choice made here is the smallest one that could possibly work: a class sees another class when some world of the first sees some world of the second. That is a real choice and not the only one — the largest sensible relation puts an arrow wherever the boxed formulas permit it, and both are filtrations. What makes a relation a filtration is a pair of conditions: it must contain the image of the original relation, and it must not add arrows that break the boxed formulas of the closure. The smallest relation satisfies both by construction.

One check is worth doing before trusting any of it, and the figures do it exhaustively: worlds share a class exactly when no formula of the closure tells them apart. Those are two different statements — one is about how the classes were computed, the other about what they mean — and they agree only if the vectors were read correctly. On the eighteen-world chain that is three hundred and twenty-four comparisons, one for each ordered pair of worlds, and every one of them is made before the picture is drawn. The habit is cheap and it catches the mistake this construction is most prone to, which is a class that has quietly merged two worlds a formula could have separated.

The comparison of the two figures is the argument in miniature. Nothing about the model changed between them. What changed is what the language was allowed to ask, and the number of worlds that survived changed with it — three under a closure of three formulas, two under a closure of two. The collapse is not a simplification of the model. It is a measurement of the formula.

The truth lemma, checked #

The claim that makes the construction worth anything: for every formula $\varphi$ in the closure and every world $w$ of the original model,

$$M, w \models \varphi \quad \text{if and only if} \quad M_f, [w] \models \varphi.$$

Read it in the direction that matters. If a formula is satisfied somewhere in a huge model, it is satisfied at the corresponding class of the quotient, and the quotient has at most $2^{|\Sigma|}$ worlds. So a satisfiable formula is satisfiable in a model whose size is bounded by the formula itself. That is the finite model property, and it is what makes the logic decidable, since a decision procedure can enumerate models up to that size and check each one.

The proof is induction on the formula’s structure, and the box case is the only one that does any work. If $\Box\psi$ holds at $w$ and the class $[w]$ sees $[v]$, then some $w'$ in $[w]$ sees some $v'$ in $[v]$; since $w'$ agrees with $w$ on $\Box\psi$, which is in the closure, $\psi$ holds at $v'$; since $v'$ agrees with $v$ on $\psi$, it holds at $v$; and by induction it holds at $[v]$. The other direction runs backwards along the same chain.

The figures do not cite that argument. Each of them evaluates every formula of the closure at every world of the model and at every class of the quotient, and compares the two answers directly — fifty-four comparisons in the first figure, thirty-six in the second, and a failure anywhere would stop the figure being drawn at all. That is worth insisting on, because the truth lemma is exactly the kind of statement that looks obviously true and is false for the wrong choice of arrows.

The bound is about the formula, not the model #

Here is the part that is easy to state and easy to underrate. The quotient’s size is bounded by $2^{|\Sigma|}$, and $\Sigma$ comes from the formula. The model plays no part in the bound at all.

That is why the theorem survives the jump to infinite models, which is the case it was written for. A chain of eighteen worlds could have been searched exhaustively without any of this. An infinite model cannot, and the construction never consults the model’s size — it consults the vectors, of which there are at most $2^{|\Sigma|}$ whether the model has eighteen worlds, twenty-four, or uncountably many.

Two different models, then, and neither of them near the bound. That is the usual state of affairs: $2^{|\Sigma|}$ is a ceiling that almost nothing reaches, since most vectors are incoherent — no world can answer $\Box p$ with yes and $\Box\Box p$ with no while seeing only worlds that answer $\Box p$ with yes. The bound survives because it does not have to be tight to make the search finite.

What the collapse invents #

A construction that throws information away has to be watched for what it puts back. Filtration does put something back, every time, and the figures report it.

The chain of eighteen worlds runs forward and stops. No world of it can be returned to: every arrow goes to a later world, so the model has no cycle anywhere. Its quotient has one — two classes that see each other — because the class of even worlds and the class of odd worlds are each realised many times over, and an arrow from one even world to an odd one and back from a later odd world to a later even one become, after the collapse, an arrow out and an arrow back.

The consequence is measurable and the figure measures it. Ask how far a world can see: in the chain, a world can see ahead exactly as far as the chain is long, and after eighteen steps there is nothing left to look at. In the quotient the answer is forever. The two models therefore disagree about the formula that says there is something eighteen steps ahead — the shortest such formula is found by searching upwards from one step, and the figure reports where it first appears.

That is not a defect. It is the exact statement of what the lemma promises. The truth lemma covers the closure and nothing else, and the separating formula lies far outside a closure of three. The collapse buys finiteness and pays in structure, and the currency is precisely the formulas nobody asked about.

The payment matters, and there is a rung of this ladder where it is fatal. Provability logic is sound exactly on transitive frames with no cycles, and a filtration that invents a cycle has produced something that is not a frame of that logic at all. Completeness there needs a construction that keeps the acyclicity, which is why the standard treatment for it is a filtration through a closure enlarged to make transitivity survive, rather than the smallest relation used here. The same care is what separates the easy logics from the awkward ones: a filtration always preserves the closure, and only some filtrations preserve the frame conditions.

Filtration is not bisimulation #

A reader who has met the relation that no formula can see through may reasonably ask what is new here. Bisimulation also identifies worlds no formula distinguishes. Why a second construction?

The two are related and are not the same, and the difference is which quantity is fixed.

Bisimulation is formula-independent. Two bisimilar worlds satisfy the same modal formulas, all of them, of every depth. That is a strong guarantee and it comes at a price: the bisimulation quotient of a model can still be infinite. Bisimilarity does not bound anything, because there is no finite budget anywhere in its definition.

Filtration is formula-relative. It fixes a finite closure first and then collapses, so the quotient’s size is bounded — and the guarantee is correspondingly weaker, holding only for the closure. The two constructions sit on opposite sides of a trade: unlimited guarantee with no bound, or bounded size with a limited guarantee.

The comparison also explains why filtration is the one that proves decidability. A decision procedure needs a bound, and only one of the two supplies it.

Two ways to get a finite model #

The finite model property has now been reached twice on this ladder by different routes, and the two are worth setting side by side, because they answer different questions and are often confused.

The canonical construction starts with a consistent formula and no model at all, and manufactures worlds out of sets of formulas. It proves completeness: if a formula is not refutable in any model, it is provable. Because the version taken over a finite closure produces a finite model, it delivers the finite model property as a by-product.

Filtration starts with a model that already exists and shrinks it. It proves nothing about provability at all. What it gives is the statement that satisfiability transfers downward, and it gives it for any model, including ones nobody built — which is what is needed when the model arrives from somewhere else, as it does when a modal formula is used to describe a program, a game, or a partial order that was specified independently of any logic.

The distinction is between manufacturing a small model and finding one inside a large model. The first is a fact about the proof system; the second is a fact about models, and it is what makes the small model relevant to the large one that was actually of interest.

What the finiteness buys #

Put the pieces together and a decision procedure falls out. To decide whether a modal formula is valid, look for a model refuting it; if one exists at all, one exists with at most $2^{|\Sigma|}$ worlds, where $\Sigma$ is the formula’s closure; enumerate the models of that size and check. The search is finite, so validity is decidable. That much has been available since the finite canonical model, and filtration is what extends it from models built out of syntax to models found in the wild.

The arithmetic of that procedure is discouraging and worth stating honestly. A formula with twenty subformulas gets a bound of about a million worlds, and the number of models on a million worlds is beyond astronomical. The bound proves decidability; it does not describe how anyone decides anything. Real procedures search for a refuting model directly, the way a tableau does, building only the worlds a failed proof forces into existence and stopping when a branch closes.

There is a second reason not to take the enumeration literally, and it is more interesting than the size. What the theorem hands over is a bound on the number of worlds, and a search wants a bound on the number of models — which means the arrows as well, and the arrows are what a bound on worlds says nothing about. Enumerating every relation on a million worlds is not merely large; it is the wrong object to enumerate, since almost every one of those relations refutes nothing. The procedures that work run the other way round, letting the formula itself say which arrows are needed and never writing down a world the formula did not demand.

What the bound does is guarantee that such a search can stop. Without the finite model property a tableau that keeps generating worlds might be building a genuine infinite countermodel, and no amount of running it would settle the question. The theorem is what licenses a search to give up. That is a role the same idea plays elsewhere: an infinite tree with finite levels has an infinite branch is the statement that makes the opposite bet safe, and both are results about when a search may conclude something from having found nothing.

What this does not settle #

Three limits, each of which has been reached by asking a question this construction almost answers.

It says nothing about which logic. Everything above concerns satisfiability in all models. A logic with frame conditions — reflexive, transitive, symmetric — needs a filtration that keeps those conditions, and whether one exists is a question per logic rather than a general theorem. Transitivity is kept by enlarging the closure; the acyclicity that provability logic demands needs more care still; and there are logics with no finite model property at all, which are exactly the ones this method cannot reach.

It says nothing about the first-order case. The game that measures quantifier depth is the corresponding instrument for first-order logic, and the corresponding theorem is false: first-order validity is undecidable, and a first-order formula can be satisfiable only in infinite models. Modal logic escapes because it is the fragment that sees along arrows and nothing else, which is the same restriction the correspondence between axioms and frame properties is about, viewed from the computational side.

It says nothing about how large a countermodel must be. The bound is exponential, and for the basic logic that is close to right — deciding satisfiability there is complete for polynomial space, so an efficient procedure is not merely undiscovered but would collapse complexity classes if found. The gap between finite and feasible is where the practical work sits, and none of it changes the statement proved here, which is that the search is finite at all.

That is the shape of the result. A formula asks finitely many questions; worlds that answer them identically are, to that formula, one world; collapse them and the formula survives while everything it never asked about does not. The finite model property is not a fact about models being secretly small. It is a fact about formulas being small, and about how little of a model a small formula can ever reach.