A language that can name a set

The rungs below measure first-order logic against graphs. Measure it against words instead — a sequence of letters, read as positions in order, each carrying a letter — and something unusual happens: the answer is completely known, in two theorems, and the two theorems are about different logics.

A word is a small structure. Its positions are ordered, and each has a letter. A sentence about words can say there is a position holding an a with a b somewhere after it, and the set of words satisfying a sentence is a language.

Which languages are definable? First-order logic gives one answer, monadic second-order logic — which may also quantify over sets of positions — gives another, and the gap between them is exactly the reason automata exist.

The word “monadic” is doing work and is worth unpacking now rather than later. Second-order logic in general quantifies over relations of any arity — over sets of pairs, sets of triples — and full second-order logic on words is far too strong to be useful: it defines languages no machine recognises, and nothing about it is decidable. Restricting to sets of single positions is what keeps the class exactly at the automata, and that restriction is the whole difference between a theorem and a mess.

The first-order side, and what it cannot say #

Take the language of words of even length. An automaton with two states decides it: flip between them at every letter and accept in the first. Nothing simpler is possible and nothing is required.

No first-order sentence defines it, and the game proves it in three lines.

Suppose a sentence $\varphi$ of quantifier depth $k$ said the length is even. Take words of length $2^k$ and $2^k + 1$ — one even, one odd, so $\varphi$ must separate them. The figure says Duplicator survives the $k$-round game on any pair of words longer than $2^k - 1$, so no depth-$k$ sentence separates them. Contradiction.

That the argument runs over words of a single letter is worth noticing. All the structure a sentence could exploit — which letters, in which order — has been removed, and what is left is a row of indistinguishable positions. If a sentence cannot count in that setting it cannot count anywhere, since every richer setting contains it. The same trick appears in the zero-one law, where the structures compared are random and therefore featureless.

Every sentence has some depth, and the counterexample is built from the depth, which is the same move connectivity’s inexpressibility uses on graphs. The difference is that here the structures are as simple as structures get — a row of identical letters — and the sentence still cannot see the parity of how many.

What the sets buy #

Monadic second-order logic adds one thing: quantification over sets of positions, with a predicate saying whether a position belongs to a set.

That is enough to say even, and the sentence is a description of the automaton. Assert that there is a set $S$ of positions such that the first position is in $S$, no two consecutive positions are both in $S$ or both out of it, and the last position is not in $S$. The set is the record of which states the automaton passes through, and the conditions are its transition rule and its acceptance condition.

That translation is completely general, which is Büchi’s theorem: a language of words is definable in monadic second-order logic exactly when a finite automaton recognises it. One direction is the translation above — a run of an automaton is a tuple of sets, one per state, and the transition rule is a first-order condition on them. The other direction builds an automaton from a sentence by induction, with the set quantifiers becoming the subset construction.

So the sets are not an abstract strengthening. A set variable is a run of an automaton, and second-order quantification over it is the automaton’s non-determinism.

Reading the thresholds #

The figure’s three numbers are worth reading rather than accepting, because the rule behind them is short and it says exactly how the budget is spent.

On words over a single letter — chains — the game is entirely about length. Duplicator’s strategy is to keep the chosen positions at matching distances from each other and from the ends, treating any distance beyond what the remaining rounds can traverse as “far”. With $k$ rounds left, a distance of at least $2^k$ is unreachable and can be matched by any other unreachable distance; anything shorter has to be matched exactly.

So Spoiler’s plan is a bisection. Pick the middle of the longer word; Duplicator must answer near the middle of the shorter; the two halves now differ in length as the wholes did, and one round has been spent halving the discrepancy. After $k$ rounds a discrepancy of one can be exposed only if the words were shorter than $2^k$ to begin with.

That gives the threshold exactly: words of $2^k - 1$ letters and longer survive $k$ rounds, which is what the search finds at 1, 3 and 7 without being told the rule. Turning it round, separating a word of a thousand letters from one of a thousand and one takes ten quantifiers, and separating parity at every length takes more than any fixed number.

The bisection is worth carrying because it is the whole reason the bound is logarithmic rather than linear. A sentence does not have to walk along a word; it can name positions anywhere, and naming the middle is the most informative thing it can do.

Deciding it by algebra instead #

The game proves one language undefinable. A general criterion needs something else, and the something else is a piece of algebra that decides the question by computation.

Two words are equivalent for a language when no context tells them apart: putting either one between the same prefix and suffix gives the same verdict. The equivalence classes form a monoid under concatenation — the language’s syntactic monoid — and it is finite exactly when the language is regular.

Schützenberger’s theorem: a regular language is first-order definable exactly when its syntactic monoid is aperiodic, meaning no element has a non-trivial cyclic orbit under repeated multiplication by itself.

The monoid is worth recognising as an object rather than a device. It is a set with an associative multiplication and an identity, which is a group with the inverses dropped — and the dropping is what makes the class large enough to hold the languages. A monoid in which every element does have an inverse is a group, and a group is exactly the counter the theorem forbids.

The criterion turns an undecidable-looking question — is there a sentence? — into a finite computation. Build the monoid, look for a cycle, and the answer is settled. That is the same conversion the game performs, done once and for all rather than instance by instance.

Why a group is the obstruction #

The condition looks technical and says something plain: a group inside the monoid is a counter, and first-order logic cannot count without bound.

Parity’s monoid is the group of order two, and its elements are “an even number of letters so far” and “an odd number”. Multiplying by $a$ moves between them and never settles, which is what a period of two means. The language’s whole content is the position in that cycle.

Compare contains ab, whose monoid has five elements and no cycle at all. Once a word contains ab, adding letters never removes it; the classes record how much of the pattern has been seen, and the record only ever moves forwards. A monoid with no group is a monoid in which everything eventually stops changing, and a first-order sentence — which has finitely many quantifiers and can only refer to finitely many positions — can check a condition that stops changing.

Read that way the two theorems on this rung fit together exactly. Automata can count modulo something, because a cycle of states is a counter, and the cycle is a cyclic group inside the monoid. First-order logic cannot, because its sentences are finite and fixed. Monadic second-order logic can, because a set variable is a run of the automaton, and the automaton does the counting.

What first-order logic does define #

The languages first-order logic defines have three descriptions and it is worth listing them, because a class of objects with three unrelated descriptions is a class worth trusting.

Star-free. Built from single letters and the empty word by union, concatenation and complement, with no star. Contains ab is $\Sigma^{*}ab\Sigma^{*}$, and $\Sigma^{*}$ is the complement of nothing, so it is star-free despite the notation.

Aperiodic. The syntactic monoid has no non-trivial group, as computed above.

First-order definable. A sentence with quantifiers over positions.

McNaughton and Papert proved the three coincide, and the proof in each direction is substantial. The class excludes parity, excludes an even number of a’s, excludes every genuine modular condition, and includes essentially every pattern-matching condition anybody writes down.

The practical reading is worth having. A regular expression without a star is a search pattern of the kind a person writes by hand; a star is what turns a pattern into a loop, and a loop is what a fixed sentence cannot simulate. So the boundary between first-order and second-order on words is the boundary between describing a pattern and running a loop — which is why the second-order sentence above needed the automaton’s run written out as a set, and could not have got it any other way.

It is also worth saying what the theorem does not say. Star-free is not the same as “written without a star”: $(aa)^*$ has a star and is not star-free, while $\Sigma^*ab\Sigma^*$ has two and is. The class is defined by what can be written, over all ways of writing it, and deciding membership by inspection is exactly what the monoid criterion replaces.

A hierarchy nobody has finished #

The picture on words is complete at the two ends and unfinished in the middle, which is worth stating so the completeness is not overstated.

Between first-order and monadic second-order sits a hierarchy indexed by how the quantifiers alternate. Sentences of the form for all … there exist … with a fixed number of alternations define a strictly smaller class than sentences with more, and the hierarchy is known to be infinite — the dot-depth hierarchy, and it is strict.

What is not known is how to decide, given a regular language, which level it sits at. The first level was settled in the 1970s, the second only in 2014, and the general question is open. So “is there a first-order sentence?” is decidable and “is there one with three alternations?” is not known to be, which is an unusual state for a subject where the outer boundary is completely understood.

The reason for the difficulty is worth naming, because it is the same reason the outer boundary is easy. Schützenberger’s criterion works because “no group anywhere in the monoid” is a condition on the monoid’s structure, checkable by looking at every element’s powers. The levels of the hierarchy correspond to conditions that are not structural in that way — they constrain how the monoid is built out of simpler pieces, and recognising a decomposition is harder than recognising a subobject.

That is a general shape and it recurs whenever an algebraic classification is used to settle a logical question. A property closed under taking parts is easy to test; a property about how parts fit together is not, and every level of this hierarchy past the first is of the second kind.

The automaton, written out #

The claim that a set variable is a run of an automaton is worth doing once in full, on the smallest case, because after that the general theorem is bookkeeping.

The automaton for even length has two states, called in and out, starts in out, and swaps at every letter. It accepts when it finishes in out.

The sentence says: there is a set $S$ of positions such that the first position is in $S$; for every two consecutive positions, exactly one of them is in $S$; and the last position is in $S$.

Read $S$ as the set of positions at which the automaton is in the state in. The first clause is the transition from the start state on the first letter. The second is the transition rule at every subsequent step. The third is acceptance. A word has such a set exactly when the automaton accepts it, and the set is unique — because the run is determined.

Every clause after the first quantifier is first-order: it speaks of positions, their order, and membership of $S$. So the sentence is one existential set quantifier followed by a first-order condition, which is the general shape Büchi’s translation produces, and the number of set variables is the number of states.

That also explains why the converse direction is the hard one. Turning a sentence into an automaton has to handle nested set quantifiers, and each one costs a subset construction — so the automaton’s size is a tower of exponentials in the sentence’s size. The equivalence is exact and the translation is not cheap, which is a distinction worth keeping.

What the pictures cannot show #

The games are played out on words over one letter, up to nine letters and depth three. That is enough to exhibit the threshold $2^k - 1$ and check it three times; the theorem is about all depths.

The monoids are built by comparing words of up to five letters across contexts of up to three. That is a truncation, and it happens to give the right monoid for these three languages because they are small; a language whose syntactic monoid needs longer words would be reported wrongly, and nothing in the figure would say so.

And the translation between automata and sentences is described and not drawn. Both directions are inductions over syntax, and an induction over syntax is not a picture.

Where the ladder goes next #

This rung closes the ladder: the game, the zero-one law, locality, the game as an algorithm, and the game measuring a second language.

Named here as debts. Trees rather than words, where the same programme runs again and the answer — Rabin’s theorem — is one of the deepest results in the subject. And the dot-depth hierarchy, whose decidability is the open question above.

Sideways, the game in its original form is the first rung, the same game as a graph algorithm is the rung below, the locality that plays the same role on graphs is the third, and a group inside a monoid is what a generator’s powers run through.

What is worth carrying away #

When a language cannot express something, the useful question is what resource it is short of rather than what sentence it is missing.

First-order logic cannot say even, and the reason is not that the right sentence has not been found. It is that a sentence has a fixed number of quantifiers, a fixed number of quantifiers is a fixed budget of positions, and parity is a property no fixed budget of positions detects. The game turns that sentence into a proof.

The habit worth taking is to look for the algebraic shadow of an expressive limit. Schützenberger’s criterion is the same limit written as a property of a finite monoid, and it converts a question about all sentences into a computation on a table — which is what makes the boundary decidable rather than merely described.

The corollary is about the value of several descriptions. Star-free, aperiodic and first-order are three definitions with nothing obviously in common, and their coincidence is what makes the class robust: a boundary that three unrelated formalisms draw in the same place is a boundary in the subject rather than in anybody’s notation.