The distance a sentence can see

A sentence about a graph names some points and says how they are joined. It can say them in any order, nest the quantifiers as deeply as it likes, and refer back to earlier choices. What it cannot do is look far.

That sounds like a metaphor and is not. There is a number, computed from the sentence’s quantifier depth alone, such that everything the sentence can detect happens within that many steps of the points it has chosen. Anything the graph does further away than that is invisible to it — and since the number depends only on the depth, a graph big enough to have room beyond that radius can be altered out there without the sentence noticing.

This rung is that statement and its main consequence. The consequence is that no first-order sentence says the graph is connected, and unlike the zero-one law’s inexpressibility results, this one has to be proved by hand, because almost every dense random graph is connected and the law is therefore silent about it.

What a neighbourhood is #

Fix a graph and a point in it. The neighbourhood of radius $r$ around that point is every point reachable in at most $r$ steps, together with the edges among them. Radius one is the point and everything adjacent to it; radius two adds everything adjacent to those.

The neighbourhood is a graph in its own right, and it is a graph with a marked point — the one it was built around. Two neighbourhoods count as the same when there is an isomorphism between them carrying one marked point to the other. In a long cycle every neighbourhood of radius $r$ is a path of $2r + 1$ points with the middle marked, whatever point it was built around and whatever the cycle’s length, provided only that the cycle is longer than $2r + 1$ so the path does not close up on itself.

That proviso is the whole of what the figures check. A cycle of fourteen and a cycle of nineteen have exactly the same neighbourhoods at radius four; a cycle of seven and a cycle of nineteen do not have the same neighbourhoods at radius four, because the smaller one wraps.

What the theorem below counts is not neighbourhoods but types of neighbourhood, and how many points realise each. A cycle of fourteen realises one type fourteen times; a cycle of nineteen realises the same type nineteen times. Those numbers differ, and the theorem is arranged so that the difference does not matter: counts above a threshold determined by the depth are all treated as the same, on the reasoning that a sentence with $d$ quantifiers can point at $d$ points and so cannot distinguish many from more. That is the second half of the locality idea and it is easy to skip past. The first half says a sentence sees only nearby; the second says it cannot count beyond its own depth. Both are needed, because a sentence that could count exactly would notice fourteen against nineteen without ever looking further than one step.

One more thing follows from the definition and is used constantly below. A neighbourhood is determined by the graph, not by any labelling of it, so two points of the same graph can have the same neighbourhood type, and in a cycle every point does. That uniformity is what makes cycles the standard example: there is exactly one type to count, so agreeing on the profile reduces to both cycles being long enough, and nothing has to be checked point by point. In a less regular graph the profile is a list of types with a count against each, and two structures agree when every entry matches or both entries are above the threshold.

The theorem #

Hanf’s theorem, in the form used here. There is a radius $r$, depending only on the quantifier depth $d$, such that two structures agreeing on the number of neighbourhoods of radius $r$ of each shape — where numbers above some threshold count as the same — satisfy the same sentences of depth $d$. The standard bound is $r = (3^d - 1)/2$.

For cycles the counting is trivial. Every neighbourhood has the same shape, so two cycles agree on the profile as soon as both are longer than $2r + 1$ and both have more copies than the threshold, which a long cycle does automatically.

The bound grows fast, and that is not an artefact of a lazy proof. Depth one gives radius one; depth two gives four; depth three gives thirteen.

The reason to state the bound rather than skip it: it is the part that makes the theorem uniform. For any particular depth one can usually do far better by playing the game directly, and the figures below do exactly that. But some bound depending only on the depth is what turns a family of separate arguments into a theorem, and it is what makes the following move legal — take any sentence at all, read off its depth, and construct a pair of structures it cannot separate.

Connected is not a first-order property #

Here is the construction. One cycle with $2L$ points is connected. Two cycles with $L$ points each, side by side, are not. They have the same number of points, the same number of edges, and — provided $L$ is long enough — the same neighbourhoods at every radius a sentence of the given depth can reach.

So no sentence of depth three says connected. Now suppose some sentence $\varphi$ of depth $d$ did say it, for whatever $d$. Take $L$ larger than the threshold for depth $d$, build the two structures, and $\varphi$ must give them the same answer — while one is connected and one is not. Contradiction, and the sentence does not exist. The cycles grow with the depth, which is why increasing the depth does not help.

Duplicator’s strategy on that pair is worth spelling out, because it is short and it is where the radius earns its keep. Keep a running promise: after $j$ rounds, the points chosen in the one structure and the points chosen in the other stand at the same distances from one another, or at distances that are both larger than the radius still in play. Spoiler picks a point; Duplicator answers with a point at matching distances from every previously chosen point, which is possible exactly because each cycle has enough room left — an arc of the required length that has not been used. When the game ends, the promise says the chosen points induce the same pattern of edges, which is what surviving means. The strategy only fails when the arcs run out, and the arcs run out only when the cycles are short relative to the number of rounds.

The shape of that argument is worth separating from its content. It is not that connectivity is complicated, or that nobody has found the right sentence. It is that any candidate sentence hands over its own depth, and the depth is enough to build the pair that defeats it.

Both figures play every game out. Nothing is inferred from the theorem and then drawn; the search is the evidence, and the rule $2^{k-1} + 1$ is checked against it at every length rather than used in its place.

What locality does and does not forbid #

The reach of the argument is wider than connectivity, and the pattern is always the same: a property that depends on arbitrarily distant parts of a structure agreeing is not first-order.

Reachability. Whether two named points are joined by a path of any length. The path can be as long as the graph, and no fixed radius covers it.

Acyclicity. Whether a graph has a cycle anywhere. A long cycle looks locally identical to a long path.

Two-colourability. Whether the points can be split into two sides with no edge inside a side. An odd cycle is not two-colourable and a long even cycle is, and locally they are indistinguishable.

Parity of the number of points. Already excluded by the zero-one law for a different reason, and excluded again here: the cycles of length $2L$ and $2L + 1$ have identical neighbourhoods.

What locality does not forbid is anything bounded. Every point has degree at most three, there is a triangle, no two points of degree five are adjacent — all of these are first-order, and all of them are decided inside a fixed radius. The line between the two lists is exactly the line the theorem draws, and it is a useful one to have drawn: it says which graph properties can be checked by a procedure that looks only at a bounded neighbourhood of each point, which is a statement about parallel and distributed computation as much as about logic.

Every sentence is a combination of local ones #

Locality has a second and sharper form, which says not merely that a sentence cannot see far but exactly what shape a sentence must have.

Gaifman’s theorem. Every first-order sentence is equivalent to a boolean combination of statements of the form there are $k$ points, pairwise more than $2r$ apart, each satisfying a formula that only refers to its own neighbourhood of radius $r$, with $k$ and $r$ computed from the sentence.

Read that as a normal form. A sentence may be written with quantifiers nested any way at all, and it can always be rearranged into: pick some points that are far apart; check something purely local at each. Nothing else is available. The scattered points are how a first-order sentence achieves whatever global reach it has, and the reach is limited to there exist several mutually distant places where such-and-such holds locally.

That form explains both lists above at once. There is a triangle is already local at radius one with $k = 1$. Every point has degree at most three is the negation of a local statement with $k = 1$. Connectivity is not of that form for any $k$ and $r$, and neither is reachability, because both are claims about a chain of points each near the last — the opposite of a claim about points far apart.

It also explains why the failures are so robust. To defeat a candidate sentence one does not have to guess what it says; it is enough to build two structures with the same scattered local pictures, which is what a pair of long cycles is.

Where the game is easier than the theorem #

The chains show the same phenomenon in the simplest possible setting, and they show why the locality bound is loose. Hanf’s radius for depth three is thirteen; on chains the game itself is won from seven elements upwards, and on the cycle pair from five points upwards. The bound is what a proof needs when the structures are arbitrary; the game is what a proof uses when the structures are known.

Reading the two together makes the distinction the whole ladder rests on. The game measures a particular pair and gives an exact answer. Locality measures a depth and gives a guarantee that holds for every pair. The first is what settles an instance; the second is what settles a language.

The looseness has a practical reading. Hanf’s bound answers how large must the structures be so that no sentence of this depth can separate them, with no information about the sentence beyond its depth. A game played on a specific pair answers the same question with full knowledge of the structures. The first number is thirteen; the second is five. Neither is wrong, and the gap between them is the price of the theorem’s uniformity.

Why the locality is there at all #

It is reasonable to ask where the restriction comes from, since nothing in the syntax of first-order logic mentions distance.

The answer is in the strategy the game supplies. When Spoiler picks a point, Duplicator answers with a point whose neighbourhood looks the same — and with each round, the radius Duplicator has to match shrinks, because there is less game left in which a discrepancy could be exposed. A sentence of depth $d$ gets $d$ moves; each move can only relate what it picks to what has been picked before, at a distance the remaining moves could traverse; and the geometric shrinking of the required radius is where the $3^d$ comes from.

That explanation also predicts what breaks it. Add anything to the language that reports a global fact and the locality goes. With a linear order on the points available, a sentence can say things no local view supports, and the game changes completely: ordered structures have their own theory and their own games, and the innocuous-looking addition of $<$ is enough to make the zero-one law of the previous rung fail as well. Counting quantifiers do the same. So locality is not a fact about first-order logic in the abstract; it is a fact about first-order logic over a relational signature with nothing built in.

The modal case is the same phenomenon with the restriction made explicit rather than derived. A modal formula can only follow arrows, so its locality is in the syntax rather than a theorem about it, and the depth of nesting is literally the distance it can travel. Everything good about the modal language — its decidability, its finite model property — traces to that restriction being built in rather than proved.

Deciding and saying are different questions #

One more distinction, because this rung is easy to misread as a claim about difficulty.

Connectivity is trivially decidable. Start anywhere, walk everywhere reachable, and see whether anything is left over; the work is linear in the size of the graph. Euler settled a connectivity question about bridges in 1736 and the argument is a paragraph. Nothing here says connectivity is hard. It says it is unsayable in a particular language, and the language happens to be one whose sentences have a fixed size while graphs do not.

That is the same distinction a search that must terminate turns on, and the same one separating a property from a procedure everywhere in logic: a procedure may loop, branch and revisit, and a sentence gets a fixed number of quantifiers and one pass. The languages that can say connected are the ones that restore something the first-order language lacks — a fixed-point operator that iterates the walk, or second-order quantifiers that name the reachable set outright. Both are strictly stronger, and both give up the properties that made the first-order case tractable.

The general moral, which is worth carrying past this ladder: two structures that satisfy the same sentences need not be alike, and the gap between them is where a language’s expressive limits live. Locality is a description of that gap for one language, made precise enough to compute with.

What this does not settle #

The theorem gives a radius and a threshold; it does not give the best radius, and the gap between what it proves and what a game shows is large. Nothing here computes the true threshold for an arbitrary property, and for most properties nobody knows it.

It says nothing about infinite structures, where neighbourhoods can be infinite and the counting argument has nothing to count.

And it says nothing about what happens once the structures come with an order. That case is genuinely different rather than merely harder: with a built-in order, first-order logic captures a real complexity class, the locality argument fails, and separating what can be said from what cannot becomes a question nobody has answered. The pleasant situation on this rung — a clean theorem, a searchable game, an exact threshold — is a feature of the plain relational setting.

What survives all of that is the method. The game converts a statement about a language into a search over moves; locality converts a search over moves into a statement about distance; and a statement about distance is something a picture of two rings can carry. The measurement was never of the sentences. It was of how much of a structure a fixed number of quantifiers can touch.