1. Two Even Numbers

In the summer of 1954, a twenty-six-year-old logician put a very small mathematical world inside a very large machine. Martin Davis was working at the Institute for Advanced Study in Princeton. Its vacuum-tube computer had 1,024 words of memory. Instructions, input, intermediate expressions: everything had to fit.

Most computers were then doing numerical calculation. Davis wanted his to decide statements. Give it a sentence from a certain language of arithmetic, and it would follow a prescribed procedure toward a correct yes or no. The underlying algorithm came with a termination guarantee. The actual computer, of course, had no guarantee of possessing enough memory to complete every instance. That difference would become the experiment's central lesson.

Davis later remembered its proudest achievement with affectionate understatement: it established that adding two even numbers gives another even number. A roomful of equipment had demonstrated something a child could grasp. Yet the intellectual achievement was not that elementary result. It was the possibility of entrusting an entire class of questions to one uniform method.

Why this class? And why, if the guarantee was so powerful, was the practical achievement so modest?

For the first answer, go back twenty-five years, to Warsaw. On September 24, 1929, the First Congress of Mathematicians of the Slavic Countries was in its second day. A twenty-four-year-old Warsaw student, Mojżesz Presburger, presented a result obtained before he had completed his master's degree. The conference programme placed his talk at 10:30 that morning.

This was no provincial gathering. Abraham Fraenkel spoke about Cantor; Alfred Tarski gave two talks. Most participants were Polish, but visitors also came from Japan and Texas. The proceedings accepted five European languages, particularly German and French. Afterward, some participants took a sleeping car to Poznań, where Kazimierz Kuratowski continued the mathematical conversation with topology.

Presburger's contribution occupied ten pages, with a short supplement elsewhere in the proceedings. Its subject was the completeness of an arithmetic of integers whose only operation was addition. A footnote dated the result to May 1928 and identified Tarski as the person who had suggested the problem.

Hilbert's circle was then pursuing the decision problem: could an entirely mechanical procedure settle the relevant logical questions, without ingenuity at each step? The precise Entscheidungsproblem concerned logical validity, not an unrestricted oracle for every imaginable mathematical truth. But the larger hope was unmistakable: replace inspired judgment with a procedure whose instructions anyone could follow.

Tarski assigned a sharply delimited version of that hope to a student. Presburger returned a positive answer. Within his fragment of arithmetic, every sentence could be settled, and an effective method would settle it after finitely many steps. Before an electronic implementation existed, its logical blueprint was already on paper.

The preceding episodes have mostly followed guarantees coming apart: contradictions in unrestricted set formation, quarrels over foundations, Gödel's obstruction to complete effective theories strong enough for arithmetic. Presburger's result points in another direction. Obtained in 1928 and presented in 1929, it preceded Gödel's 1931 paper. Closure was possible. The question was what had to remain outside.

2. Questions the Language Cannot Ask

Suppose the only available coins have values three and five. Can they make eleven? Yes: two threes and a five. Can they make seven? No. Is every sufficiently large amount possible? Yes: every integer from eight onward can be formed with nonnegative numbers of those coins.

Presburger arithmetic can express all these questions. It can also decide them. The coefficients three and five are fixed: three copies of a variable mean repeated addition, not multiplication of two independently varying quantities.

The language can speak about zero and one, sums, equality, order, and quantifiers such as “there exists” and “for every.” Order may be included explicitly or defined in an appropriate presentation. It can compare differences, specify a remainder modulo seven, or require several linear conditions to hold together. This is a functioning mathematical country, not a few ruins left after subtraction of the interesting parts.

What it cannot define is the general relation between three variables saying that one is the product of the other two. Nor can it uniformly define the square numbers, the primes, or divisibility with a variable divisor. Individual numerical facts are another matter: one can name a particular square or prime. The missing resource is a formula that picks out precisely all such numbers.

The distinction is stronger than difficulty in finding a proof. There is no question in this language that does the required job. In one variable, definable subsets of the natural numbers are eventually periodic: beyond some point their membership pattern repeats with a fixed period. Squares and primes do not have that form. They cannot be recovered merely by being ingenious with longer additions.

Loss of expressive power is not loss of deductive power. A system may settle every question it can formulate while being unable to formulate many questions we care about.

Three terms need keeping apart. Completeness, in the present sense, says that for every sentence the theory proves either it or its negation. Decidability says that one algorithm determines membership in the theory and always terminates. Feasibility concerns the resources needed to carry this out.

Under suitable hypotheses, completeness gives decidability. If a consistent theory has effectively enumerable axioms and is complete, enumerate its proofs. Given a sentence, wait until a proof of it or of its negation appears. Completeness ensures that one eventually does; consistency ensures they do not both appear. This argument provides termination, not a useful timetable.

Presburger's own method was more informative than blind enumeration. Its effective completeness argument supplied a way to decide truth in the intended arithmetic structure. That is the sense in which a proof delivered a machine along with its theorem.

Completeness does not mean omniscience. It means that no sentence within the chosen language remains unsettled. The restriction “within” carries much of the result. A less expressive language may make completeness easier to obtain, although no general numerical law says that every small-looking language is decidable.

Feasibility asks something different again. A procedure can be guaranteed to finish yet require more time or storage than any actual machine could provide. Complexity theory makes that distinction mathematical; engineering confronts it materially. Princeton's 1,024 words would expose the gap well before the sharp lower bounds arrived.

3. Removing a Quantifier

The organizing operation behind Presburger's procedure is quantifier elimination. A formula mentioning an unknown quantity is transformed into an equivalent condition that no longer quantifies over it.

For example, ask whether there is an integer x such that x + x = a. The answer is exactly that a is even. We have replaced a search for x with a condition on a alone.

There is an important technical qualification. “Even” is not magically a new quantifier-free expression in the bare language of addition. Presburger quantifier elimination is normally carried out in an expanded language containing predicates for divisibility by fixed integers, or congruence conditions. Those predicates are themselves definable in the original language. Adding them does not enlarge the sets we can ultimately describe; it makes the elimination process expressible without hidden quantifiers.

The resulting condition can therefore mention that a leaves remainder zero on division by two, but no longer mention a candidate x. The procedure repeatedly converts quantified linear arithmetic into Boolean combinations of inequalities and fixed-modulus conditions.

A similar move works in a different world. Is there a real x with x² = a? Exactly when a is nonnegative. Over the reals, the unknown can disappear into the condition a ≥ 0. Over the integers, that answer would be wrong. Both the operations and the domain matter.

Tarski showed that first-order statements built from real polynomial equations, inequalities, and quantifiers admit this kind of elimination. Addition and multiplication are both available. For a sentence with no free variables, continued elimination leaves something whose truth can be directly determined.

Elementary geometry enters through coordinates. Points become finite tuples of real numbers. Collinearity, perpendicularity, circles, and distance relations can be written with polynomial equations and inequalities. Geometric propositions that admit such first-order formulations consequently enter the decision procedure too.

Not every statement ever called geometry enters with them. Arbitrary sets of points, arbitrary functions, and unrestricted higher-order quantification exceed the language. The boundary is drawn by the formal vocabulary, not by the name on a university department's door.

An existential statement appears to demand a search through infinitely many candidates. If no candidate works, that search might never end. Elimination replaces it with a finite condition whose equivalence has been proved. It succeeds here because these structures have special mathematical regularities, not because all infinite searches are secretly finite.

Nor does the procedure necessarily supply understanding in the form a mathematician wants. The output may be enormous and aesthetically unrewarding. But it reveals something beyond a yes or no. It describes the shapes of sets that formulas can define. Model theory would make that structural information one of quantifier elimination's central uses: the method tells us not just which assertions hold, but what sorts of objects a language is capable of isolating.

4. The Boundary Is Not a Multiplication Sign

If deleting multiplication helps, perhaps multiplication is the culprit. Two examples defeat that explanation.

Skolem arithmetic keeps multiplication on the natural numbers while discarding addition, and is decidable. Tarski's theory of real closed fields keeps addition, multiplication, and order, and is decidable too. Neither operation by itself has a fixed logical destiny.

The dangerous combination is ordinary addition and multiplication acting together on the integers or natural numbers. Together they support elaborate coding: finite sequences, proofs, and stages of computation can be represented arithmetically. This is the expressive machinery behind the preceding episode's self-reference.

Presburger arithmetic remains below that threshold. Its escape from Gödel's hypothesis is not inconsistency, and not a refusal to make its axioms effective. It lacks the required arithmetic strength. That is why its completeness is no counterexample to incompleteness.

Tarski's real algebra offers a revealing test. Inside the ordered-field language of the reals, the integers are not definable as a set. If they were, one could restrict quantification to them and recover the forbidden arithmetic within a supposedly decidable theory.

The expression x³ + y³ = z³ looks the same on either side of that divide. Allow real values, and it belongs to real algebra; insist that the variables range over integers, and it belongs to a much less tame domain. This particular equation is not itself undecidable. It illustrates the change of domain through which a general class of difficult integer questions becomes available.

Hilbert's tenth problem made that class explicit: find a general procedure deciding whether an arbitrary polynomial with integer coefficients has an integer solution. Davis had been pursuing it since his student years. While he implemented a decision procedure in Princeton, he was also helping investigate the boundary beyond which no such procedure could exist.

Work by Davis, Hilary Putnam, and Julia Robinson prepared the way. Yuri Matiyasevich supplied the final ingredient in 1970. His first public presentation took place in Leningrad on January 29; Grigori Tseitin helped carry the result onward. The answer was negative: no algorithm solves every instance of Hilbert's tenth problem.

Davis thus worked on both sides of the boundary—building one machine and helping prove the impossibility of another. There is no contradiction. The machines were being asked different questions.

Church and Turing had already established in 1936 that first-order validity has no general decision procedure. Trakhtenbrot's 1950 theorem showed that restricting attention to finite structures does not rescue the unrestricted finite-model validity problem either. Finiteness of each object does not mean a bounded collection of objects to inspect.

Meanwhile, decidable territories persisted: additive arithmetic, real algebra, algebraically closed fields, and later many structures understood through automata. Their mechanisms differ. Logic's landscape is not a single ladder ascending from easy to impossible. It is a map of fragments and extensions, with researchers seeking large decidable regions on one side and surprisingly small undecidable expansions on the other.

5. Warsaw, and a Book Delayed

Presburger belonged to a dense intellectual community. The broader Lwów–Warsaw school grew from Kazimierz Twardowski's teaching. In the interwar period it included Kazimierz Ajdukiewicz, Tadeusz Kotarbiński, Stanisław Leśniewski, Jan Łukasiewicz, and Tarski. Warsaw's logicians worked amid students and younger colleagues such as Adolf Lindenbaum and Presburger.

Presburger was a participant, not merely a name attached to one result. He prepared Łukasiewicz's mathematical-logic lectures for publication from the spoken course. Journals such as Fundamenta Mathematicae provided institutional channels, while other Polish mathematical centres had their own publications.

The network extended beyond Poland. Tarski visited Vienna in 1930 and again in 1935; Rudolf Carnap came to Warsaw in 1930. The names from the foundational controversies belong to overlapping relationships, not separate national boxes.

A bibliography conceals the difficulty of Tarski's employment. Born Alfred Teitelbaum, he changed his surname in 1923 and converted to Catholicism, despite lacking religious belief. Identification with Poland and the barriers facing Jews in academic employment formed part of that decision's setting. After earning his doctorate in 1924, he combined university teaching appointments with years of school teaching. Standard biographical accounts report an unsuccessful application for a chair at Lwów in 1939. Such accounts agree on the larger fact: international mathematical stature did not bring him a secure Polish professorship. Stanford's scholarly biography documents that contrast.

Tarski obtained his decision method for real algebra around 1930, with antecedents in courses from 1926–28. Students heard parts of the work long before a broad readership could buy it.

A Paris publication was planned for 1939. War prevented it. RAND revived the manuscript in 1948, with J. C. C. McKinsey helping prepare and revise it; a revised edition followed in 1951. The publication history is recorded in the original RAND report. A result developed before the war entered circulation through an American research organization tied to military funding.

The wartime interruption has a clear cause. The earlier interval between discovery and planned publication has no comparably simple explanation established here. A historian should leave that space open rather than fill it with a plausible story.

Presburger's own record becomes much less complete. Born in Warsaw on December 27, 1904, he finished secondary school in 1923, entered the university, and received his master's degree in October 1930. Jan Zygmunt's 1991 biographical study drew heavily on surviving university records. Registration papers, courses, and graduation documents preserve an institutional outline of the young man.

The end of his life is less certain than the beginning. A Polish Jew, he was murdered during the Holocaust, probably around 1943. The exact date and place, and the course of his last years, remain uncertain. That uncertainty is part of the history, not a detail to be tidied away.

Procedures growing from a paper he wrote in his twenties have run on successive generations of machines. His own final journey cannot be reconstructed with comparable precision.

6. A Different Bargain

Back in Princeton, Davis discovered that a short description of an algorithm need not imply a small computation. Converting formulas into a suitable normal form could multiply their components. Combinations expanded into combinations of combinations. Available memory disappeared.

His later recollection says that the program consumed the tiny store and could handle only elementary examples. The discouragement was practical, not a refutation of Presburger. Finite termination on an idealized machine had never promised completion on this particular one.

In 1956, Allen Newell, J. C. Shaw, and Herbert Simon pursued another approach. Their Logic Theorist searched for proofs of propositions from Whitehead and Russell's Principia Mathematica. It used selective strategies: try promising directions and avoid exploring everything indiscriminately.

A discovered proof could be checked. Failure to discover one, however, did not establish that none existed. The sacrificed guarantee was completeness of the search and assured success, not permission to issue false proofs. “No proof found” and “not a theorem” are different answers.

This distinction matters for the episode's recurring ledger. Some methods guarantee an answer for every admissible input but become too expensive. Others trade exhaustive search for useful performance on selected cases. Heuristics do not automatically entail unsound reasoning.

Hao Wang challenged the assumption that algorithms had to be hopelessly slow. Born in Jinan in 1921 and educated at the wartime Southwest Associated University in Kunming, he later pursued logic in the United States. During the summer of 1958 he worked with an IBM 704 at IBM's laboratory in Poughkeepsie.

One program proved more than two hundred theorems from the first five chapters of Principia Mathematica in about thirty-seven minutes. Twelve thirteenths of that time went to input and output; the actual proving occupied under three minutes. Wang set out the timings in “Toward Mechanical Mathematics”, published in 1960.

He also made an uncomfortable methodological point. Showing that heuristics outperform a particularly inefficient algorithm establishes little about the relative power of heuristics and algorithms in general. The baseline matters.

Wang drew another lesson from the results: theorems people actually prove may use only a small part of a theory's full expressive resources. A large mathematical subject can contain a practically important, tractable fragment. The worst difficulties available in principle need not be present in every working example.

In 1983 he received the first IJCAI milestone award for automated theorem proving. Davis later dedicated his account of early automated deduction to Wang. The disagreement had become part of a shared history. Neither successful examples nor discouraging experiments were enough by themselves; one had to ask exactly what the program was being given and exactly what its guarantees covered.

7. The Cost Is a Separate Question

By the early 1970s, the two approaches faced related but distinct difficulties. James Lighthill's 1973 review of artificial intelligence for Britain's Science Research Council emphasized combinatorial explosion. Programs impressive on carefully limited examples could fail when possibilities multiplied at realistic scale.

In 1974, Michael Fischer and Michael Rabin established a more precise obstruction for Presburger arithmetic. They were not criticizing one implementation. Their lower bound applied to any general decision method in the relevant computational model: some sufficiently large inputs require doubly exponential resources. A typical scale is 2 raised to a quantity that itself grows exponentially with input length.

This is a worst-case theorem. It does not say that every sentence of a given length is hard, or that each extra symbol literally squares every program's runtime. It says that no universally fast decision algorithm escapes suitable families of difficult inputs. Their work also related decision difficulty to the possible lengths of proofs under specified assumptions.

Derek Oppen's 1978 upper bound supplied a complementary guarantee: a general procedure exists within a triply exponential deterministic-time bound. Upper and lower bounds do not coincide merely because both are enormous. Oppen's paper states the distinction explicitly.

Lighthill and Fischer–Rabin were therefore not proving the same thing. One assessed the limitations of a research programme's contemporary methods; the other established a mathematical limitation for a sharply defined problem. Their juxtaposition makes the cost visible at two scales without turning an empirical assessment into an impossibility theorem.

Real algebra had its own expensive success. Tarski's original procedure established decidability but was impractical. George Collins's cylindrical algebraic decomposition, introduced in 1975, made complete real-algebraic methods much more usable. It partitions real space into finitely many cells on which relevant polynomial signs behave consistently.

The number of cells can grow doubly exponentially in the number of variables. Davenport and Heintz's 1988 work showed an intrinsic doubly exponential obstruction for general quantifier elimination: some equivalent quantifier-free descriptions must themselves become immense. That output-size result must not be casually identified with every decision problem over the reals. Later improvements reduced unnecessary projection and decomposition work, exploited special forms, and avoided constructing information a particular question did not need.

Wu Wen-tsun made another selective bargain. In Beijing during 1976–77, he began developing mechanized methods for geometry based on polynomial equations. General statements involving inequalities and order were not his initial target. Restricting the class of questions enabled effective treatment of many substantial geometric theorems, with degeneracy conditions handled carefully.

Wu described ancient Chinese algorithmic mathematics, especially The Nine Chapters and Liu Hui's 263 commentary, as an intellectual predecessor. That was Wu's historical interpretation of his programme, not proof that modern algebraic algorithms had simply survived unchanged from antiquity. His preface on mathematics mechanization also recalled Wang's rapid machine proofs.

Decidability promises eventual correct termination. It does not promise seconds, a lifetime, or the resources of a physical universe. Practical usefulness concerns the actual distribution of problems, machines, and available resources. A dreadful worst case can coexist with an indispensable tool. Wang's lesson returns: useful problems need not inhabit the worst corner of a theory.

8. A Ledger with Three Columns

Closure can be obtained, but “buying” is our retrospective metaphor. Presburger and Tarski were studying structures, not negotiating prices for certainty.

Presburger obtained a complete decidable additive arithmetic by working in a language that cannot express much of number theory. Tarski obtained a decision procedure for real algebra and the elementary geometry it encodes. His language includes multiplication but cannot define the integers. In both cases the guarantee depends on what the domain and language permit.

Their longest afterlives include disciplines that did not yet have their present shape. Quantifier elimination became central to model theory. Presburger arithmetic became useful in program analysis, where array indices, loop counts, and linear relations between integers arise constantly. David Cooper's 1972 algorithm made an important practical improvement, and variants entered proof assistants and verification tools.

These uses should change how we hear the word “limited.” A restriction may omit nearly everything a number theorist wants and still capture a large part of what a verification system needs.

The author's proposed ledger has three columns. The first records what questions a system can ask. The second records what its guarantees actually are: sound answers, completeness of search, or guaranteed termination. The third records the resources required.

Davis had a theoretical decision guarantee and collided with implementation cost. Logic Theorist pursued selective proof search without guaranteeing that it would find every available proof. Wang demonstrated that a well-chosen decidable fragment could offer both rigorous guarantees and impressive speed. Wu narrowed the geometric problem class to obtain effective methods.

Later systems moved among these possibilities. Work by Davis, Putnam, and colleagues helped develop procedures for propositional satisfiability, whose descendants became important in hardware and software verification. Other systems accept far broader requests while offering weaker guarantees. Calling both kinds “intelligent” tells us little about their entries in the ledger.

No theorem says every possible trade-off must resemble a simple three-way conservation law. The rigorous negative results apply to specified languages, theories, and computational models. In particular, sufficiently expressive effective arithmetic cannot have a sound total decision procedure for all its truths. That precise barrier supports the metaphor; the metaphor must not replace it.

A system answering every question it can formulate may be powerful, or its questions may be severely restricted, or both. To assess it, count the excluded questions as well as the answered ones. Then ask whether its promise is a proof, a decision, or a useful guess—and how much fulfilling that promise costs.

Two gaps remain in this account's chronology. War stopped Tarski's planned Paris book. Genocide ended Presburger's life, leaving its final date uncertain. Those are not limitations of a formal language. They are losses inflicted on the people who built one. The next episode returns to the institutions from which people could be removed while the mathematical symbols remained.