A machine that carries one bit

Arithmetic with addition alone found that every question about whole numbers that can be phrased with addition, equality and the quantifiers “for all” and “there exists” has an answer that can be computed. Mojżesz Presburger proved it in 1929 by eliminating quantifiers: each “there exists” can be traded for a condition on remainders, until nothing is left but a check a computer can do. That essay mentioned, in its last pages, that the same sets of numbers are exactly those a finite machine can read. This essay takes that second route seriously, because it is a different method of proof and it reaches further.

The method rests on one observation about addition: checking a sum needs almost no memory.

Write $x = 13$, $y = 11$ and $z = 24$ in base two, one above another, padded with zeros to the same length. Read the columns from the right. Each column is three bits, one from each number. The column is consistent with $z = x + y$ exactly when the top two bits plus the carry from the previous column leave the bottom bit when halved, and the new carry is what is left over. Nothing else about the earlier columns matters — not how many there were, not what digits they held, only whether they left a one to carry. A machine that remembers only the carry, one bit, can check any sum of any size.

Addition as a machine with two states #

That machine can be drawn in full.

It has two states, “carry 0” and “carry 1”. From “carry 0”, the columns $000$, $011$ and $101$ keep the carry at nought — nothing, or a single one that lands in $z$ — and the column $110$ moves to “carry 1”, since $1 + 1$ is $0$ with one carried. From “carry 1” the columns $010$, $100$ and $111$ keep it, and $001$ returns to “carry 0”. Any other column contradicts the sum and the machine stops. It must start and finish with no carry.

The figure checks it on every pair of numbers below $64$, offering the true sum and two false ones, and it accepts exactly the true sums. A finite automaton — a machine with a fixed, finite number of states, reading its input one symbol at a time — recognises the relation $x + y = z$, and it needs only two states to do it.

Machines combine, and quantifiers become guesses #

Having a machine for addition is the starting point. The power of the method is that machines can be combined in exactly the ways sentences are built.

“And” is running two machines side by side, each in its own state, and accepting when both accept: the product of the machines. “Not” is swapping the accepting and rejecting states of a machine that never stops early. “There exists a $y$” is the interesting one. A machine for a formula about $x$ and $y$ reads two tracks of bits. To decide “there exists $y$ such that…”, erase the $y$ track and let the machine guess each bit of $y$ as it goes: it accepts if some sequence of guesses leads to acceptance. That is a nondeterministic machine, and a standard construction, which a language that can name a set used for sets of positions in words, turns it back into an ordinary one by tracking every set of states the guesses could have reached.

“For all” is “not there exists not”. So every sentence built from addition, equality, “and”, “not” and the quantifiers turns into a machine, step by step, and a sentence with no free variables turns into a machine that reads nothing and either accepts or does not. That decides the sentence. J. Richard Büchi introduced the method in 1960, and it gives a proof of Presburger’s theorem that never mentions remainders at all: a quantifier is a shadow described “there exists” as projection, and in this setting the projection is erasing a track.

One sentence, decided #

It helps to follow the method through one sentence. Take “every number is even or one more than an even number”:

$$\forall x\ \exists y\ \big(x = y + y \ \lor\ x = y + y + 1\big).$$

Start inside. The formula $x = y + y$ is the addition machine with the $z$ track set to $x$ and both summand tracks set to $y$ — equivalently, the doubling machine drawn below, which checks that $x$’s bits are $y$’s bits shifted up one place. The formula $x = y + y + 1$ is the same with a one added, which the machine handles by starting in “carry 1” instead of “carry 0”. “Or” is the product machine accepting when either part does.

Next, “there exists $y$”: erase the $y$ track and let the machine guess it. The guessing machine accepts a string of $x$’s bits exactly when some $y$ makes the formula true, and after the subset construction it turns out to be the machine that accepts every string: whatever $x$ is, halving it and rounding down gives a $y$ that works. Finally, “for all $x$” is “not there exists $x$ not”, and since the machine accepts everything, its complement accepts nothing, the existential over that accepts nothing, and its complement accepts everything. The sentence is true.

For a sentence like this the answer is obvious. The method does not care: the same four operations, applied to a sentence nobody can see through, still end with a machine that accepts or does not, and the answer is read off without insight.

Machines for more than addition #

The method is not tied to addition. Any relation that a machine can recognise, read in base two, can be added to the language, and the sentences built from it remain decidable.

“$x$ is a power of two” is easy for a machine in base two: a power of two is a single one followed by zeros, and a machine with two states, plus a dead state for a second one, recognises it. But it cannot be said with addition alone. Arithmetic with addition alone showed that every set addition can define is eventually periodic — from some point on it repeats with a fixed period — and the powers of two are not. So a machine can see something that Presburger’s formulas cannot.

A little more is possible. The relation “$y$ is the largest power of two dividing $x$” — which picks out the lowest one in $x$’s binary expansion — draws a ruler: every odd number is divisible only by $1$, every second even number by $2$ and no more, and so on. A two-state machine recognises it by reading $x$ and $y$ together and demanding that $y$’s single one sit exactly at $x$’s first one. Adding this relation to addition gives Büchi arithmetic, and every sentence in it is decidable by the same method. Alexei Semenov showed in 1977 that adding just “$x$ is a power of two” keeps arithmetic decidable, the fact arithmetic with addition alone closed on; the machines explain why.

How small the machines are #

The machines for these basic relations are tiny, and that is what makes the method work.

Each machine in the table is built directly, checked against its property on every small input, and then shrunk to the fewest states that do the same job by merging states that behave identically on every future input. “$x$ is even”, “$x$ is a power of two”, “$x$ is a multiple of 3”, “$x = 2y$” and “$x + y = z$” each need three states, one of them a dead state. None of these counts depends on how large the numbers are. That is the whole point: a fixed, finite memory handles every number at once, and so a machine can answer a question about all whole numbers.

The price is paid elsewhere. Each “there exists” can multiply the number of states exponentially when the guessing machine is turned back into an ordinary one, and a sentence with several alternating quantifiers can need a machine of staggering size. Michael Fischer and Michael Rabin proved in 1974 that no method at all can decide Presburger arithmetic in less than doubly exponential time in the worst case. Decidable is not the same as fast. In practice the sentences people want to decide are usually far from the worst case, and programs that build these machines routinely handle sentences whose machines have millions of states, because the blow-up that the lower bound guarantees for some sentences rarely appears in the sentences that arise from real questions.

Reading from the other end #

The machines here read digits from the least significant, the order in which carries flow. Reading the other way, from the most significant digit, addition still needs only finite memory, but the machine must work differently: at each column it does not yet know whether a carry will arrive from the columns to its right. So it guesses — keeps track of both possibilities, “a carry is coming” and “no carry is coming” — and checks each guess against the next column. The guesses cost nothing extra, because there are only two of them, and the subset construction turns the guessing machine back into an ordinary one of about the same size.

That symmetry is a general fact. A set of binary strings recognised by a finite machine reading left to right is also recognised by one reading right to left — the reversal of a regular language is regular — though the second machine can be larger. For the relations of arithmetic the two directions are equally good, and the choice is only a matter of which machine is easier to draw.

The difference matters for a human doing long addition, who writes the digits from the right because that is where the carries start. A machine that may guess does not need to: nondeterminism lets it read in whatever order the input arrives, which is exactly the freedom the quantifier “there exists” was translated into.

Why the squares would break it #

The machines have a limit, and it is exactly where arithmetic with addition alone found the edge of decidability. Add “$x$ is a square” to the language, and arithmetic becomes undecidable, because multiplication can be defined from squares and addition:

$$xy = \tfrac12\big((x + y)^2 - x^2 - y^2\big),$$

and with multiplication, Gödel’s incompleteness and Turing’s undecidability apply in full. So no machine can recognise the squares in base two. If one could, the method would decide full arithmetic, which no algorithm can read what a program does shows to be impossible. The impossibility of a machine for squares is proved by its consequences, not by staring at the binary digits of $1, 4, 9, 16, 25, \ldots$ — although the digits do look patternless, and the gaps between squares grow in a way no fixed memory can track.

The boundary is therefore sharp and slightly surprising. Powers of two: yes. The largest power of two dividing a number: yes. Squares: no. What the machines can see is exactly what fits in a finite memory read digit by digit, and a relation as simple-looking as “is a square” does not.

When two formulas say the same thing #

Machines give one more thing for free. Two formulas in the language define the same set of numbers exactly when their machines accept the same strings, and whether two finite machines accept the same strings can be decided: shrink each to its fewest states, as the table above did, and a machine with the fewest states is unique up to renaming, so the two either match state for state or they do not.

So not only is every sentence decidable, but every question of the form “do these two formulas mean the same?” is decidable too. The six ways of arranging two quantifiers that six sentences from two quantifiers drew — “for every $x$ there is a $y$” against “there is a $y$ for every $x$”, and the rest — can each be turned into a machine for a given relation, and their agreements and disagreements read off by comparing machines. For the relations of addition, the logic of quantifier order becomes the combinatorics of finite machines.

Theorems proved by machine #

The method is not only a theoretical device. Programs that build these machines from sentences are used to prove theorems about sequences that are themselves defined by machines — automatic sequences, like the Thue–Morse sequence, which records whether each number has an even or odd count of ones in binary. Questions such as “does this sequence contain a block that repeats three times in a row?” become sentences in Büchi arithmetic extended by the sequence, and a program builds the machine and reads off the answer.

Jeffrey Shallit and his collaborators have used a program called Walnut to prove, this way, dozens of results about such sequences that had resisted hand proof, some of them conjectures that had stood for years. The proofs are machines with thousands or millions of states, checked by computer; they are rigorous and unreadable, a trade that four colours, and a proof nobody can read described for a different theorem. Sequences like the one the orbit written as a word followed are often of exactly this kind.

What the machines and tables cannot show #

Each machine is checked on a finite range. The figures test every drawn machine against its property on every input up to a stated size; that it is right for all inputs follows from its construction, which reads one column at a time and never depends on the length.

The decision method is described, not run on a sentence. Building the machine for a sentence with several quantifiers involves products, projections and the subset construction, and even small sentences produce machines too large to draw; the figures show the building blocks, and the argument shows how they combine.

Base two is a choice. Everything works in any base, and the sets recognisable in two bases that are not powers of a common number are exactly the eventually periodic ones — Cobham’s theorem, which arithmetic with addition alone quoted. The powers of two are machine-readable in base two and not in base three.

Still open: addition and the primes #

What happens if “$x$ is prime” is added to addition, instead of powers of two or squares? No finite machine recognises the primes in any base — they are not eventually periodic and their gaps are irregular — so the method does not apply, but that does not settle whether the resulting arithmetic is decidable.

It is not known. A decision procedure for addition with the primes would settle questions such as the twin prime conjecture and Goldbach’s conjecture, since each is a sentence in that language: “for every $x$ there is a prime $p > x$ with $p + 2$ prime”, and “every even number above $2$ is a sum of two primes”. Patrick Bateman, Carl Jockusch and Alan Woods showed in 1993 that, assuming Dickson’s conjecture — a statement about many linear expressions being prime together, of which the twin prime conjecture is the simplest case — the arithmetic of addition and primes is undecidable. Unconditionally, whether a machine or any other method can decide it is open, and it cannot be settled without first settling questions about primes that have been open for centuries.

A carry is enough #

The habit worth keeping is to ask how much memory a check needs.

Adding two large numbers looks like it needs the whole numbers. Checking an addition needs one bit, carried from column to column. That single observation turns addition into a two-state machine, and machines combine the way sentences do, so every sentence about addition becomes a machine that can be run. Decidability, here, is the finiteness of a carry, and the limits of the method are exactly the relations — squares, primes — that no finite carry can track.