A quantifier is a shadow

Every row, or one column read there is a $y$ such that $R(x, y)$ on a grid as a question about a row: does it contain a mark? Six sentences from two quantifiers arranged every sentence of that kind in one diagram. Both worked with finite grids, where the question is settled by looking. This essay takes the same reading to the real numbers, where the grid has infinitely many rows and columns — and finds that the reading turns a quantifier into a geometric operation with a name.

Take a relation between two numbers, $a$ and $x$, drawn as a set of points in the plane. There is an $x$ with $R(a, x)$ asks, for each $a$, whether the vertical line at $a$ meets the set. The $a$ for which it does are the set’s shadow on the $a$-axis, its projection. An existential quantifier is a projection, and eliminating it means describing the shadow without mentioning the thing that cast it.

The shadow of a curve #

The equation $x^2 + ax + 1 = 0$ relates two numbers, and the pairs $(a, x)$ that satisfy it form a curve — two branches, one on each side. For a given $a$ the equation has a solution exactly when the vertical line at $a$ crosses the curve, which in the grid means exactly when the column at $a$ contains a marked cell. The strip under the grid marks those columns, and it is two pieces: $a \le -2$ and $a \ge 2$.

That strip is the answer to the quantified question, and it has been written without a quantifier. “There is an $x$ with $x^2 + ax + 1 = 0$” is the same statement as “$a^2 \ge 4$”. The equivalence is not new — it is the discriminant, $a^2 - 4$, whose sign what the coefficients already know read off without finding any root. What is new is the point of view: the discriminant is a machine that removes a quantifier. It turns a question about the existence of an $x$ into an inequality about $a$ that can be checked by arithmetic.

The figure decides each column by testing whether the curve crosses any of its cells, which is a search; the discriminant decides it by a single subtraction. The two answers agree in every column, and the agreement is the theorem.

For every x, and there is an x #

A universal quantifier is a shadow too, of the complement. For every $x$, $P(a, x)$ fails exactly when there is an $x$ with not-$P(a, x)$ holds, so the set of $a$ making the universal statement true is everything outside the shadow of the set where $P$ fails.

The two sentences in the figure are about the quadratic $x^2 + ax + b$, now with two parameters. Some $x$ makes it zero holds on and below the parabola $b = a^2/4$; every $x$ makes it positive holds strictly above it. They are exact complements, because a quadratic with positive leading coefficient either dips to zero somewhere or stays positive everywhere — and both are described by the one polynomial $a^2 - 4b$, with the quantifier gone and only its sign remaining.

Each cell was decided by brute force, trying 801 values of $x$, and then compared with the inequality. The brute force is only possible because the quadratic’s behaviour at large $x$ is known; the inequality needs no search at all. That is the practical value of elimination: a question about infinitely many $x$ becomes a question about finitely many coefficients.

Elimination comes with cases #

The answer is not always a single inequality. Allow the leading coefficient to vary as well, and ask whether $ax^2 + bx + c = 0$ has a real solution.

When $a$ is not zero, the equation is quadratic and the answer is the discriminant, $b^2 - 4ac \ge 0$ — on one slice the region below a parabola, on the other the region above one, because the sign of $a$ flips which side counts. When $a$ is zero the equation is $bx + c = 0$, which has a solution whenever $b$ is not zero and, if $b$ is zero, only when $c$ is too. So the quantifier-free version is

$$\bigl(a \ne 0 \text{ and } b^2 - 4ac \ge 0\bigr) \text{ or } \bigl(a = 0 \text{ and } (b \ne 0 \text{ or } c = 0)\bigr).$$

That is the general shape of an eliminated formula: polynomial equations and inequalities, combined with and, or and not. The middle slice of the figure is shaded everywhere except the line $b = 0$ — and on that line only at $c = 0$ — which is how a degenerate case looks when the formula is drawn.

The shadow can have corners #

The boundary of a shadow need not look like the graph of a polynomial, even though it always is one in disguise.

For the quartic $x^4 + ax + b$ the minimum over $x$ can be found by calculus, and the equation has a solution exactly when that minimum is at most zero. The boundary comes out as $b = 3(|a|/4)^{4/3}$ — a curve with a cusp at the origin and a fractional power in it, which does not look like anything a polynomial inequality could describe. Cube both sides and it becomes $256 b^3 = 27 a^4$, and the region is $b \le 0$ or $256 b^3 \le 27a^4$. The two numbers 256 and 27 are exactly the ones in the quartic’s discriminant, which is the resultant of the polynomial with its own derivative, as a shared root, found without finding it computed: a double root is where the shadow’s edge is.

Tarski’s theorem: every shadow is tame #

The examples so far eliminated one quantifier from a particular formula by knowing something about quadratics or quartics. Alfred Tarski proved in the 1930s — with the full proof published in 1948 — that this always works. Every statement about real numbers built from polynomial equations and inequalities, with any number of quantifiers, is equivalent to one with no quantifiers at all, and there is a procedure that finds it. Abraham Seidenberg gave a second proof in 1954, and the geometric form of the theorem carries both names: the shadow of any set described by polynomial inequalities is again described by polynomial inequalities.

The consequence Tarski cared about is decidability. A sentence with no free parameters, once its quantifiers are eliminated, becomes a combination of statements like $3 > 2$, which can be checked. So there is an algorithm that decides the truth of every sentence of this kind about the real numbers — a fact a countable field that passes for the line used to show that a countable field and the real line cannot be told apart by such sentences.

The procedure is expensive. George Collins’s method of 1975 decomposes space into cells on which every polynomial involved has constant sign, and its cost grows doubly exponentially with the number of variables; James Davenport and Joos Heintz showed in 1988 that the doubling is unavoidable in the worst case, because the eliminated formula itself can be that long. Tame is not the same as small.

It is nonetheless used. Questions of the form is this polynomial inequality true for every choice of these variables arise in checking that a mechanical linkage cannot jam, that a control system stays stable for every setting of its parameters, and that a geometric theorem holds for every configuration of its points; each is a universal sentence about real numbers, and a quantifier-elimination procedure settles it outright, with no search over cases and no possibility of missing one. For small numbers of variables — the two or three the figures here use — the doubly exponential cost is affordable, and the answer is a proof rather than a sample.

Over the complex numbers, shadows are simpler still #

The real numbers are not the only field where quantifiers can be eliminated, and comparing them with the complex numbers shows what the inequalities were for. Over the complex numbers, there is an $x$ with $x^2 + ax + 1 = 0$ is true for every $a$ — every polynomial of positive degree has a root, as a loop that cannot miss the middle proved by following an image curve round the origin. The shadow of the curve is the whole axis, and the quantifier is eliminated in favour of the word true.

With two equations the question becomes interesting again. Two polynomials in $x$ have a common complex root exactly when their resultant vanishes, which is the determinant built from their coefficients: there is an $x$ with $f(x) = 0$ and $g(x) = 0$ is equivalent to a single polynomial equation in the coefficients. Claude Chevalley’s theorem generalises this: over the complex numbers, the shadow of any set described by polynomial equations is described by polynomial equations and their negations — never by inequalities, because the complex numbers have no order for an inequality to use.

That is the division of labour. Over an algebraically closed field such as the complex numbers, eliminating a quantifier produces equations and not-equal conditions; over the real numbers it also produces inequalities, because a real polynomial can fail to have a root by staying on one side of zero, and which side is an inequality. The parabola boundaries in the figures above are the real numbers’ version of a resultant, with the sign of the discriminant doing work that over the complex numbers never arises.

Over the whole numbers, a shadow can be anything #

Change the numbers the quantifier ranges over from the reals to the whole numbers, and the picture changes completely.

There are whole numbers $x, y \ge 2$ with $n = xy$ is an existential statement about $n$, and its shadow is the set of composite numbers. The empty columns are the primes, and the pattern of gaps is as irregular as crossing out the composites found it: no polynomial inequality in $n$ describes it, and no quantifier-free formula of the real-number kind could.

It goes much further. Yuri Matiyasevich proved in 1970, completing work by Martin Davis, Hilary Putnam and Julia Robinson, that every set of whole numbers that a computer can list is the shadow of a polynomial equation — the set of $n$ for which some whole numbers $x_1, \dots, x_k$ make a fixed polynomial vanish. The primes are one such set, and in 1976 James Jones, Daihachiro Sato, Hideo Wada and Douglas Wiens wrote down an explicit polynomial in 26 variables whose positive values are exactly the primes.

The route to that theorem is itself a story about a quantifier’s reach. David Hilbert asked, as the tenth of his problems of 1900, for a procedure deciding whether a polynomial equation has a whole-number solution — assuming there must be one. Davis, Putnam and Robinson showed in 1961 that every listable set is the shadow of an exponential equation, one that allows unknowns in the exponents, so the whole question came down to whether exponentiation itself is the shadow of an ordinary polynomial equation. Julia Robinson had shown that it would be enough to find one polynomial relation whose solutions grow exponentially but not too fast. Matiyasevich found it in the Fibonacci numbers: the relation “$v$ is the $2u$-th Fibonacci number” is the shadow of a polynomial system, and the Fibonacci numbers grow like powers of the golden ratio, which is exactly the growth Robinson needed.

Because some listable sets cannot be decided — there is no procedure that always says whether a number belongs — some shadows of polynomial equations over the whole numbers are undecidable. That is the negative answer to Hilbert’s tenth problem: there is no algorithm that takes a polynomial equation with whole-number coefficients and says whether it has a whole-number solution. Over the reals the same question is decided by Tarski’s procedure. The quantifier is the same word in both cases; what it ranges over decides whether its shadows are tame or wild.

Why the reals are tame and the integers are not #

The difference has a clean explanation. The whole numbers can express multiplication by quantifying over them — $z$ is the product of $x$ and $y$ and $x$ is a whole number are both statements available inside the language — and that is enough to encode arbitrary computation, as the proof of Gödel’s incompleteness theorem shows in the sentence that says it has no proof. The real numbers cannot define the whole numbers with polynomial inequalities: every set of reals a quantifier-free formula describes is a finite union of intervals and points, and the whole numbers are not.

So over the reals every definable set of numbers is a finite union of intervals — a set of real numbers the shadow of a polynomial can produce is always simple in shape — and computation cannot be encoded. Over the whole numbers a single existential quantifier in front of a polynomial reaches every listable set. The discriminant and the prime-representing polynomial are the two ends of the same idea: one shadow is an interval, the other is the primes.

What the grids cannot show #

Infinitely many rows. Every grid here is finite, and each column’s mark was found by a search over a bounded range of $x$ — 801 or 1,601 values. On the real line the rows are infinitely many and a search could miss a solution far away; the case-split figure had to widen its range because the linear slice’s solution runs off to thirty. The inequality has no such problem, and that is the point of it, but the pictures are only as good as the range searched: a bounded search can prove that a solution exists and can never, by itself, prove that none does.

Several quantifiers. The figures eliminate one quantifier from sentences with one or two parameters. Tarski’s theorem covers any number of quantifiers, alternating freely, and the eliminated formulas grow very fast. No drawing shows what the shadow of a shadow of a shadow looks like in several dimensions.

Why the prime polynomial works. The last figure draws the composites as a shadow of a simple relation, divisibility. The polynomial whose values are the primes is a far more elaborate object, built by encoding the verification of primality as a system of equations, and nothing in the figure resembles it.

Still open: shadows over the fractions #

Over the real numbers, whether a polynomial equation has a solution is decidable. Over the whole numbers it is not. Over the rational numbers — fractions — nobody knows. Whether there is an algorithm that takes a polynomial equation with whole-number coefficients and decides whether it has a solution in fractions is one of the central open problems of the subject.

It would follow from Matiyasevich’s theorem if the whole numbers could be defined inside the fractions by a single existential formula, and whether they can is unknown. For curves, the question of which ones have rational points is the domain of deep conjectures about elliptic curves; for the circle it was settled long ago, as every triple on one circle found — a line through one rational point finds all the others. Between the circle, where the answer is a picture, and arbitrary equations, where it may be undecidable, the fractions sit in a gap nobody has closed.

A shadow cast on a line #

A quantifier asks whether a column contains a mark, which is to ask for the shadow of a set on an axis. Over the real numbers every shadow of a polynomial set is again polynomial — the discriminant for a quadratic, $256b^3 \le 27a^4$ for a quartic, cases when a leading coefficient can vanish — and Tarski’s theorem makes that a procedure that decides every such sentence.

Over the whole numbers the same shadow can be the primes, or any set a computer can list, and whether a polynomial equation has a whole-number solution cannot be decided. What separates the two is what the quantifier ranges over, and for the fractions, halfway between, it is not known which side they fall on.