Four quantifiers, one of them blind

Every row, or one column began this sequence with the difference between for every row there is a column and there is a column for every row, and it ended with a reformulation. A sentence $\forall x\, \exists y\; R(x, y)$ says exactly that there is a function $f$ with $R(x, f(x))$ for every $x$: the witness $y$ is chosen once $x$ is known, so it is a function of $x$. That move — replacing each “there is” by a function of the "for every"s to its left — is called Skolemisation, and it says something precise about what the order of quantifiers means. In $\forall x\, \exists y\, \forall u\, \exists v\; \varphi$ the witness $y$ is a function of $x$, and the witness $v$ a function of $x$, $y$ and $u$ together, because all three stand to its left.

The order forces a particular pattern of dependence, and it is not the only pattern one could want. Leon Henkin asked in 1961 about the sentence in which $y$ depends on $x$ and $v$ depends on $u$, and nothing else: two lines of quantifiers side by side, neither able to see the other.

$$\begin{pmatrix} \forall x\; \exists y \\ \forall u\; \exists v \end{pmatrix} \varphi(x, y, u, v) \quad\text{means}\quad \exists f\, \exists g\; \forall x\, \forall u\;\; \varphi(x, f(x), u, g(u)).$$

No arrangement of four quantifiers in a single line produces that dependence. Whichever of $y$ and $v$ comes second can see the other’s line. The branching form is therefore something new, and the question is how much new. The answer, found by Herbert Enderton and by Wilbur Walkoe independently in 1970, is startling: everything that can be said with existential second-order logic — with “there is a relation such that” — can be said with first-order formulas under branching prefixes. There is a relation such that showed that this is exactly the class of properties a nondeterministic machine checks in polynomial time. One quantifier made blind to two others reaches all of it.

The same matrix in a line and branching #

The clearest case uses no relation at all — only equality. Take the matrix

$$\varphi = (x = u \to y = v) \;\wedge\; (y = u \to v = x) \;\wedge\; x \ne y.$$

Read in a line, $\forall x\, \exists y\, \forall u\, \exists v\; \varphi$ is easy to satisfy on any set with two or more points. Given $x$, choose any $y$ different from it. Given $u$, choose $v$ by cases: if $u$ is $x$, take $v = y$; if $u$ is $y$, take $v = x$; otherwise take anything. The three clauses of $\varphi$ are then satisfied, because the choice of $v$ looked at $x$ and $y$ to decide which case it was in.

Read branching, the sentence asks for two functions $f$ and $g$ with $\varphi(x, f(x), u, g(u))$ for all $x$ and $u$. Setting $u = x$, the first clause says $g(x) = f(x)$ for every $x$: the two functions are the same. The third clause says $f(x) \ne x$: no point is fixed. And setting $u = f(x)$, the second clause says $f(f(x)) = x$: applying $f$ twice returns to the start. A function with those properties pairs the points off — each point with its image, which is paired back with it — and such a pairing exists exactly when the number of points is even.

So the branching sentence, built from four quantifiers and the equals sign, says the set has an even number of points. No first-order sentence in a line can say that. A game that decides what can be said proved it with the games of Ehrenfeucht and Fraïssé: for any sentence with $k$ quantifiers, two sets of more than $k$ points each are indistinguishable by it, whatever their parity. There is a relation such that said “even” by adding a relation and asking for it to be a perfect matching. Here the relation is not mentioned. It is the function $f$, conjured by the shape of the prefix.

Every small set, searched #

The claim can be checked on every small set by trying every function. On $n$ points there are $n^n$ functions from the points to themselves, and up to four points every pair $(f, g)$ — $n^{2n}$ of them — can be tried as well.

The counts are the double factorials: on $2m$ points there are $(2m - 1)(2m - 3) \cdots 3 \cdot 1$ pairings, since the first point can be paired with any of $2m - 1$ others and the rest paired recursively. The search finds 1 on two points, 3 on four, 15 on six, and none on 1, 3, 5 or 7. The 65,536 pairs on four points include exactly three winners, each with $g = f$ — the forced equality from the first clause, confirmed rather than assumed. In a line, the sentence is false only on a single point, where $x \ne y$ cannot be met.

The table is small, and it would be easy to read it as a curiosity about one sentence. What it shows in general is that the branching prefix carries the power of a hidden “there is a function”, and that the function is not the one Skolemisation always provides. A linear prefix also has Skolem functions, but they are functions of everything to their left, and that dependence on everything is what keeps first-order logic weak: a function that may look at all the earlier choices can always be built one case at a time, which is what the linear strategy above did. A function forbidden to look is a global object — a single $f$ that must work for every $x$ simultaneously — and global objects are what second-order logic quantifies over.

The sizes a sentence with only equality can pick out #

The sizes at which a sentence can come true measured spectra: for a sentence about a relation, the set of sizes at which some relation makes it true. A sentence that mentions no relation at all, only the equals sign, has a spectrum too — the sizes of the sets on which it is true — and for first-order sentences in a line that spectrum is dull. Any two sets with more than $k$ points satisfy the same sentences with $k$ quantifiers, so the spectrum of a sentence with nothing but equality in it is either a finite set of sizes or contains every size from some point on. “At least three points” and “at most five points” can be said, and Boolean combinations of such statements, and nothing else.

Branching sentences with only equality are not dull in this way. The even sentence has the even numbers as its spectrum, neither finite nor eventually everything. And the general answer follows from Enderton and Walkoe’s theorem by a short argument: a branching sentence with only equality says “there are relations such that” something first-order holds, and the sizes at which that is true are exactly the spectrum of the first-order sentence about those relations. So the spectra of branching sentences that use nothing but equality are precisely Scholz’s spectra — all of them: the primes, the powers of two, the sizes at which a projective plane exists, every set of sizes that a nondeterministic machine recognises in time exponential in the length of the number. The relation symbols that the earlier essay needed to write those sentences can be dispensed with; the blind quantifiers manufacture them out of equality.

That is a useful way to see what the branching prefix is doing. A first-order sentence in a line can only count, and only up to its own number of quantifiers. A branching sentence can build structure — a pairing, a successor function, a grid — on a set that has none, and then ask first-order questions of what it has built.

Why the line can cheat #

The difference between the two readings can be seen in one table. Fix a choice of $y$ for each $x$ — say, on five points, $y = x + 1$, the next point round — and ask what $v$ must be for each pair $(x, u)$.

Each row has two constrained cells. In row $x$ the cell $u = x$ demands $v = x + 1$, and the cell $u = x + 1$ demands $v = x$; all other cells accept anything. In a line, $v$ is chosen after $x$ is known, so it can read the row and answer it. Branching, $v$ is chosen knowing only $u$, so it must give one answer for a whole column, and column $u$ is constrained twice — by the row $x = u$, which wants $v = u + 1$, and by the row $x = u - 1$, which wants $v = u - 1$. The demands agree only if $u + 1 = u - 1$, which on five points never happens. With a rotation every column clashes; with any $f$, a column $u$ is consistent exactly when $f(u) = f^{-1}(u)$, and an $f$ consistent everywhere is its own inverse.

The table is a picture of what independence costs. A quantifier that can see its predecessors works locally, one situation at a time. A quantifier that cannot must commit to a policy, and policies have to be compatible across situations that the quantifier cannot tell apart. That is the same constraint that made the guessers of infinitely many guessers, finitely many wrong choose a representative for each class of sequences they could not distinguish: a player who cannot see part of the position must act the same way in every position that looks the same.

A game neither player wins #

Quantifiers have a reading as a game, and the branching ones bring the game an unusual feature. In the game for $\forall x\, \exists y\, \forall u\, \exists v\; \varphi$, a player called Abelard chooses $x$, a player called Eloise replies with $y$, Abelard chooses $u$, and Eloise replies with $v$; she wins if $\varphi$ holds. The sentence is true when Eloise has a winning strategy and false when Abelard has one, and for ordinary first-order sentences on finite sets one of them always does. For the branching sentence, Eloise must choose $v$ without knowing $x$ or $y$ — as if she were a team of two who cannot confer, one answering the first line and one the second.

Abelard’s strategies are a first point $x$ and a rule choosing $u$ for every possible $y$ — $n \cdot n^n$ of them — and each was tried. To win, a strategy must defeat every strategy of Eloise’s. But against any fixed strategy of Abelard’s only one play takes place, and Eloise can win that play: she chooses some $y \ne x$, Abelard’s rule produces some $u$, and one value of $v$ satisfies the matrix for that $u$. Abelard therefore never has a winning strategy on two or more points. On three and five points Eloise has none either. The sentence is neither true nor false.

This is the observation that Jaakko Hintikka and Gabriel Sandu built into independence-friendly logic in 1989: once quantifiers can be blind to one another, the game they describe has imperfect information, and games of imperfect information can be undetermined. The law of the excluded middle fails, and with it the usual meaning of negation. The negation of the branching even sentence — the sentence in which the players swap roles — is not “the set has an odd number of points”; on three points both it and the original are untrue. The properties branching sentences can express are closed under “and” and “or” but not under “not” — provably not on arbitrary sets, as the next example shows, since “infinite” is expressible and “finite” is not. On finite sets the question is a famous one: the class is exactly what a nondeterministic machine can verify, and whether it is closed under complement is the question of whether NP equals co-NP.

Four quantifiers that say infinite #

A second matrix shows the reach of the prefix more dramatically. With a constant $a$ for one point, take

$$\varphi = (x = u \leftrightarrow y = v) \;\wedge\; y \ne a.$$

Branching, the first clause with $u = x$ forces $g = f$ again, and then reads as $f(x) = f(u)$ exactly when $x = u$: the function is one-to-one. The second clause says it never takes the value $a$. A one-to-one map of a set into itself that misses a point is Dedekind’s definition of an infinite set, and on any finite set it is impossible by the pigeonhole principle — $n$ points mapped one-to-one into $n - 1$ cannot all have different images. On the whole numbers $f(n) = n + 1$ does it, missing $0$. So the four quantifiers say “the set is infinite”. In a line, the same matrix holds on every set of two or more points, by the same trick of reading the row.

No first-order sentence in a line says “infinite”, and the reason is the compactness theorem, which a number larger than every number used to build its non-standard numbers. If some sentence held exactly on infinite sets, its negation would hold on every finite set, and compactness would then give the negation an infinite model — a contradiction. The branching sentence escapes the argument because branching logic is not closed under negation: “finite” is not a branching sentence, and compactness, which does hold for existential second-order sentences, is never confronted with it.

The two examples, even and infinite, are not tricks of the particular matrices. Enderton and Walkoe’s theorem says that every existential second-order sentence — “there are relations $R_1, \dots, R_k$ such that” followed by a first-order statement — is equivalent to a first-order matrix under some branching prefix, usually with longer lines than two. Relations are coded as functions, functions are supplied by blind quantifiers, and the first-order matrix checks that the functions cohere.

What the blindness costs to check #

The power comes at a price, and the price is the price of nondeterminism.

To check a linear sentence with four quantifiers on $n$ points, evaluate the game: at most $n^4$ plays, a polynomial. To check the branching form by brute force, search over functions: $n^n$ candidates for $f$, each tested against $n^2$ pairs. Andreas Blass and Yuri Gurevich showed in 1986 that no general shortcut should be expected — even narrow branching prefixes produce sentences whose checking on finite structures is NP-complete. A single blind quantifier converts a problem that is easy because it can be solved locally into one that is hard because a global object has to be found.

The figures in this essay could exhaust the functions because the sets are tiny: at seven points $7^7 = 823{,}543$ functions take a fraction of a second. At twenty the count is $10^{26}$, beyond any search, and at that point the even sentence remains decidable only because its particular matrix has a simple meaning — a pairing exists when the count is even — that a mathematician can see. For a general branching sentence there is no such insight to fall back on, which is exactly what NP-completeness says.

The contrast with the linear prefixes is instructive. Six sentences from two quantifiers showed how much the order of a linear prefix matters; a quantifier is a shadow read “there is” as projection, and the shadows of first-order formulas over the real numbers stayed tame. A branching prefix is a projection along a function rather than a coordinate, and the shadows it casts are the shapes of NP.

The function was always there #

There is a sense in which nothing in this essay is new to anyone who has read every row, or one column. Skolemisation already turned every linear sentence into a statement that certain functions exist, and on infinite sets the passage from for every $x$ there is a $y$ to there is a function choosing $y$ from $x$ is exactly the axiom of choice, as the choice nobody can write down described. What makes a linear sentence first-order rather than second-order is not the absence of functions but the shape of their arguments. Every Skolem function of a linear prefix takes as arguments all the universal choices to its left, and a function with that much information can be replaced, as far as truth is concerned, by a sequence of local decisions.

A branching prefix withholds arguments. The function $g$ in the even sentence must answer $u$ without $x$, and a function that withholds information cannot be replaced by local decisions: it must be a single coherent object. The whole gap between first-order and existential second-order logic lies in which arguments a witness is allowed to read, and Henkin’s notation is the device that lets the gap be stated with a picture of two lines.

Does language branch? #

Hintikka thought that branching quantifiers are not an exotic invention but something ordinary speech already contains. His example of 1973 was the sentence some relative of each villager and some relative of each townsman hate each other. On its natural reading the relative chosen for a villager does not depend on which townsman is in question, and vice versa — exactly the dependence of Henkin’s prefix. If that reading is right, English is not first-order, and an adequate semantics for it must reach into second-order logic.

The claim was contested at once. Dov Gabbay and Julius Moravcsik disputed the branching reading in 1974, and Jon Barwise argued in 1979 that the most convincing examples of branching in English involve quantifiers like “most” or “exactly half” rather than “some” and “each” — there the branching reading and every linear reading genuinely come apart. The debate has never been fully settled, partly because judgments about such sentences are unstable: a speaker can hear Hintikka’s sentence one way on one day and another way the next.

What is settled is the logic. A prefix in which some choices cannot see others is a precise object, its expressive power is exactly existential second-order logic, its model-checking problem is NP-complete, and its games can be undetermined. The equals sign alone, under four such quantifiers, separates even from odd and finite from infinite. All of it was available in first-order logic’s own notation, missing only the permission to draw the quantifiers in two lines.

Still open: the smallest prefixes that reach everything #

Enderton and Walkoe’s theorem uses branching prefixes of whatever width and length the coding needs. How small can they be made? The prefix in this essay — two lines of one $\forall$ and one $\exists$ — already says “even” and “infinite”, and Blass and Gurevich found narrow prefixes whose checking is NP-complete. Between the linear prefixes, which say only first-order things, and the wide ones, which say everything existential second-order logic can, lies a hierarchy of shapes studied by Michał Krynicki, Marcin Mostowski and others, and which shapes express which properties — on finite sets, with and without relation symbols — is settled for some and open for others. It is a classification with known endpoints and an unmapped middle.

A second question is about the value of an undetermined game. If the players may randomise, a game of imperfect information has a value in the sense of von Neumann’s minimax theorem, and Merlijn Sevenster and Sandu proposed in 2010 to read that value as a degree of truth: the branching even sentence on three points is true to some probability strictly between nought and one. Values have been computed for small sentences and families of them; a general account of which numbers arise as the values of first-order matrices under branching prefixes, and how they behave as the set grows, is not yet in hand.