The boundary at three variables

The refinement hierarchy measures how many variable names are needed to separate two structures, and finds that no fixed number is enough. A different question can be asked of the same resource, and the answer is sharp in the other direction: two names are enough for satisfiability to be decidable, and three are not.

That is a strange place for a boundary. A sentence with two variable names can be arbitrarily long — the names are reused, so $\exists x\, \big(P(x) \wedge \exists y\, (R(x,y) \wedge \exists x\, (R(y,x) \wedge \cdots))\big)$ nests as deep as wanted. What two names cannot do is hold three things in view at once, and that turns out to be the whole difference.

What a name buys #

The resource being counted is not the number of quantifiers but the number of names, and the distinction is worth getting right first.

A sentence like every point has a neighbour whose neighbours include a point of degree three needs three things named at once in its natural writing: the point, its neighbour, and the neighbour’s neighbour. Writing it with two names means one of them has to be recycled, and recycling loses whatever it was holding.

So a $k$-variable sentence describes a structure by a walk with $k$ markers, moving one marker at a time and never seeing more than $k$ points together. The matching game is the $k$-pebble game, played in the figure above: Spoiler picks up a pebble and places it anywhere in either structure, Duplicator answers in the other, and the position must stay consistent.

Duplicator surviving forever means no $k$-variable sentence separates the structures, which is the same correspondence the original game has with quantifier depth, one resource over.

The figure’s three rows are each a small demonstration of that. A four-cycle and a six-cycle are both connected, both two-regular, and both bipartite; two pebbles see nothing but the relation between the two points they hold, and every configuration they can reach in one is matched in the other. Three pebbles win by walking a triangle’s worth of the structure — three points whose mutual relations pin the size down — and the difference between the two columns is exactly that one extra thing held in view.

The small-model property #

The decidability result rests on one fact and the fact is a count.

Fix a vocabulary with finitely many relation symbols, all of arity at most two — which is the setting two-variable logic lives in, since a sentence with two names cannot mention a three-place relation usefully anyway.

A point’s 1-type is the set of one-place facts true of it: which unary predicates hold, and whether $R(x,x)$ holds for each binary $R$. With $u$ unary symbols and $b$ binary ones there are $2^{u + b}$ possible 1-types.

A pair’s 2-type is the set of two-place facts true of the ordered pair, together with the two 1-types. There are exponentially many of those too, in the same parameters.

And a two-variable sentence cannot see anything else. Its truth in a structure is determined by which 1-types are realised and which 2-types are realised between points of each pair of 1-types — because two names never hold three points, so no fact about a triple can be stated.

That gives the theorem. Scott’s normal form rewrites any two-variable sentence as a conjunction of a universal part $\forall x \forall y\, \chi$ and finitely many statements $\forall x \exists y\, \psi_i$, and from a model one can build a small one: keep one witness for each $\exists$ requirement of each realised 1-type, and discard everything else. The result is a model of size exponential in the sentence’s length, and it satisfies the same sentence.

So satisfiability is decidable by a bounded search: enumerate structures up to that size and test. And the complexity has been pinned down — the problem is complete for nondeterministic exponential time, so the exponential blow-up is not an artefact of the argument.

Why three names lose it #

The third name buys the ability to say this, that, and the other, and that is enough to encode a grid.

With three names one can write down the axioms of a structure with two functions whose compositions commute — for all $x$, the $f$ of the $g$ of $x$ equals the $g$ of the $f$ of $x$ needs $x$, $f(x)$ and $g(x)$ named together — and such a structure is a grid. Once a grid is available, a Turing machine’s computation history can be laid out on it, with one row per step, and a sentence can demand that the layout obey the machine’s transition rule.

A sentence that is satisfiable exactly when a machine halts is a reduction from the halting problem, so satisfiability for three-variable sentences is undecidable. That is the same undecidability proof search inherits from its one unbounded rule, arriving from the other side: there the question is whether a search terminates, here whether a model exists, and the two are the same question by completeness. The reduction is due to Kahr, Moore and Wang in 1962, in the form of the classical decision problem — the question, going back to Hilbert’s Entscheidungsproblem, of which quantifier prefixes give a decidable satisfiability problem.

Two variables sit exactly on the boundary. They cannot express the commuting condition, cannot encode a grid, cannot lay out a computation, and their sentences therefore have no way to force an infinite or unbounded structure.

Scott’s normal form, which is where the bound comes from #

The small-model argument is stated above in a sentence and the sentence hides the one construction that makes it work, which is worth setting out because the whole bound is read off it.

Every two-variable sentence is equivalent to one of the shape

$$\forall x \forall y\; \chi(x,y) \;\wedge\; \bigwedge_{i=1}^{m} \forall x \exists y\; \psi_i(x,y),$$

with $\chi$ and the $\psi_i$ quantifier-free. Getting there costs new unary predicates — one for each subformula that has to be named — so the rewritten sentence is longer, linearly, and the equivalence is over structures expanded by those predicates.

That shape is what the small model is built from. Take any model. For each 1-type actually realised, pick one point of it. For each such point and each of the $m$ existential requirements, pick one witness. Throw everything else away and repair the relations between what is left.

The size that leaves is the number of realised 1-types times $m+1$, and the number of 1-types is exponential in the vocabulary — hence exponential in the sentence’s length, and no worse.

The repair step is the part that needs the two-variable restriction. Relations between two kept points can be set arbitrarily because no sentence in the fragment constrains a triple, so there is no consistency condition to satisfy beyond what the universal part demands, and the universal part is checkable pair by pair. With three variables the repair fails immediately, since a triple’s relations are constrained by the sentence and cannot be set independently.

That is the whole of the difference in one paragraph, and it is worth noticing that it is a statement about repairing rather than about expressing. Two variables cannot say anything about a triple, so a construction is free to do what it likes with triples — and that freedom is what makes the model small.

What two variables can and cannot say #

It is worth collecting examples, because the class is larger than the bound suggests and smaller than one would guess.

Expressible with two names. Every point has a neighbour. No point is its own neighbour. The relation is symmetric. Every point with property $P$ has a neighbour with property $Q$. All of modal logic — which is the reason two-variable logic is studied at all, since a modal formula translates into two variables and its good behaviour is inherited. That translation is why the fragment matters outside logic: the description logics behind ontology languages, and several database query fragments, are modal in shape, and their decidability is this theorem.

Not expressible with two names. The relation is transitive — that needs $x$, $y$ and $z$ together. There is a triangle, for the same reason: a triangle is three points and their three relations, and separating the graphs that have one from those that do not is precisely what the third pebble buys. The graph is connected, which is beyond any fixed number of variables without counting. And the grid axioms above.

The transitivity case is the sharp one. Two-variable logic with a transitivity requirement imposed on one relation is still decidable; with two transitive relations it is undecidable. So the boundary is not only about the count of names — it moves with what the relations are required to be, and the results in that area are a patchwork rather than a line.

That figure is the essay’s central distinction drawn twice. Quantifier depth and variable count are independent resources, and the original game measures the first while this measures the second.

Counting, and where the boundary moves #

Adding counting quantifiers — there exist at least seventeen $y$ such that — changes the picture in a way worth recording, because it is the one direction that costs nothing.

Two-variable logic with counting is still decidable. The finite model property survives, with a worse bound, and satisfiability remains in nondeterministic exponential time. That was shown by Grädel, Otto and Rosen in 1997, twenty years after the plain case, and the proof is substantially harder.

Which matters because counting is what the refinement hierarchy is about. The refinement hierarchy corresponds to $k$-variable logic with counting, and the results there are about expressive power at every $k$; this result is about decidability at $k = 2$. The two questions are asked of the same fragments and have nothing to do with each other — one is settled for all $k$ and negatively, and the other is settled at $k = 2$ and positively.

And the boundary is not the same for expressiveness. Two variables with counting express strictly more than two without, and the gap is exactly the ability to count neighbours — which is one-dimensional colour refinement, the first level of that hierarchy. So the same fragment sits at the bottom of one hierarchy and on the far side of a decidability boundary, and its two reputations have no connection.

What the bound costs in practice #

The decision procedure is a bounded search over structures of exponential size, which is decidable and is not usable, and the gap between those two words is worth a paragraph because it is the usual state of affairs in this area.

The complexity is exactly nondeterministic exponential time. Grädel, Kolaitis and Vardi settled that in 1997: there is a procedure, its cost is exponential, and no better is possible — the lower bound matches, so the exponential is the problem’s rather than the method’s.

With counting quantifiers it stays the same, which is the surprise: adding the ability to say at least seventeen costs nothing in complexity class, though the proof is much harder and the bound on the model’s size is worse.

And with an equivalence relation or a transitive relation it changes in every direction. One transitive relation: still decidable. Two: undecidable. One equivalence relation: decidable, and the complexity is lower. Two: decidable, three: undecidable. The results are a patchwork and there is no rule covering them, which is the honest description of the subject past the main theorem.

What that means for the practical fragments — the description logics, the query languages — is that each one’s decidability has to be established separately, and the two-variable theorem is a starting point rather than a cover. Being decidable and being computable are separate achievements, and the second one is where the implementations live.

The classical decision problem, of which this is a piece #

Two variables is one entry in a longer table, and the table is worth knowing because its shape is unusual.

Hilbert’s question — is there a procedure deciding whether a first-order sentence is satisfiable — was answered negatively by Church and Turing in 1936. The follow-up question, which prefix classes are decidable, was pursued for the next thirty years and closed completely.

The decidable cases are the prefix classes $\exists^*\forall^*$, $\exists^*\forall\exists^*$, $\exists^*\forall^2\exists^*$ over a vocabulary without function symbols, and the two-variable fragment. Everything else is undecidable, including $\forall^3\exists$ and $\forall\exists\forall$.

So the boundary is a short list rather than a principle, and the two-variable fragment is the one entry on it defined by a resource rather than by a prefix shape. That is why it has survived as an object of study while the prefix classes have not: it is closed under the operations one wants, it contains modal logic, and it has applications in description logics and in database theory where the prefix classes have none.

Three variables is the first place all of this stops, and after sixty years there is nothing between two and three to look for.

It is worth noticing what the table’s shape says. The decidable prefix classes are all shallow — a block of existentials, a bounded block of universals, another block of existentials — so they are classes where the alternation is bounded rather than the vocabulary. The two-variable fragment is the odd one: its sentences have unbounded alternation and bounded width. Two completely different resources, each of which happens to deliver decidability when bounded, and no argument covering both.

Three small pairs, and a claim about every sentence #

Three pairs of small graphs is not the theorem. The games are played out exhaustively and their verdicts are exact for those pairs, and the theorem is about all sentences with two names over all structures. What the figure shows is the resource behaving as described at a size a search can reach.

The finite model property is not drawn at all. The claim is that a satisfiable sentence has a model of a computable size, and both the sentence and the model are objects with no picture — one is a string and the other is a structure of exponential size. Everything in the section that states it is prose — which is the standing division here, where the game is drawable and the theorem it measures is not.

And the undecidability at three variables is a reduction. It works by encoding a machine, which is a construction rather than an observation, and no figure on this page contains anything of it.

The two-pebble game is drawn as a verdict rather than as a game. Each table row is the outcome of a search over every move in a tree of positions, and a reader sees survives or loses and nothing of the strategy behind it, which is the usual limitation of drawing an exhaustive result.

Still open: what the game has closed and what it has not #

The game set out to measure what a logic can say, and the measurement has held up over seven results: quantifier depth, the zero-one law, locality, refinement, second-order quantification on words, the hierarchy’s strictness, and now decidability.

Two debts remain from the account of words and both are still open in the same form. The dot-depth hierarchy — which level of quantifier alternation a given regular language sits at — is decidable at the first two levels and open beyond, despite the outer boundary being completely understood. And trees rather than words, where the analogue of Büchi’s theorem is Rabin’s and is one of the deepest results in the subject, is understood but its consequences are not exhausted.

What this adds is a third, and it is the sharpest. The decidability boundary at two variables is understood and the reason it is there is not. There is no principle explaining why two names give a finite model property and three do not — only the proofs, one positive and one negative, meeting in a place nothing predicted.

Two resources, counted separately #

The habit is to ask which resource a limitation is a limitation on.

A sentence has a length, a quantifier depth and a variable count, and all three are finite. The original game shows depth being the binding constraint; the refinement hierarchy shows the variable count being binding for a completely different question; and this page shows the variable count deciding something neither of them touches.

The three resources are independent and a fragment is defined by bounding one of them. Bounding depth gives a finite set of sentences and nothing interesting. Bounding variables leaves infinitely many sentences of unbounded depth, and produces both the strict hierarchy above and the decidability boundary here.

So the question worth asking of any expressive limit is not what can this language say but which of its resources was exhausted — and the answer decides whether the limit is about how much the language sees at once, or how far it can look.