Tarski's Real Arithmetic Is Decidable

In 1931, Kurt Gödel detonated a bomb under mathematics: no consistent formal system strong enough to express basic arithmetic can prove all truths about the integers. Some statements are simply undecidable — neither provable nor disprovable from the axioms.

Seventeen years later a Polish–American logician named Alfred Tarski showed that a closely related universe escapes this doom entirely. The theory of real closed fields — first-order statements about the real numbers using +, ×, 0, 1 and the ordering — is complete and decidable. Every such statement can be settled by a mechanical procedure.

The key tool is quantifier elimination: any statement of the form "there exists a real x such that…" or "for all real x…" can be transformed, step by step, into an equivalent statement with no quantifiers — a plain polynomial comparison that a computer can evaluate directly. The procedure always terminates, and it always gives the right answer.

This is not a minor technical footnote. It means that every geometric theorem about points, lines and circles expressible in first-order logic has a computable proof search — a fact that powers computer algebra systems, robot motion planning and formal verification today.

Tarski's procedure decides any first-order statement about real numbers by eliminating quantifiers one by one. Below are several statements of the form ∃x · p(x) ≥ 0 where p(x) is a polynomial. Select one and watch the algorithm decide it.

<p class="hint">{{hint}}</p>
<div class="picker">
  <label for="stmt">{{choose_label}}</label>
  <select id="stmt">
    <option value="0">∃x · x² + 1 ≥ 0</option>
    <option value="1">∃x · x² + 1 ≤ 0</option>
    <option value="2">∃x · x² − 2 ≥ 0</option>
    <option value="3">∃x · −x² + 4 ≥ 0</option>
    <option value="4">∃x · x² − 5x + 6 ≤ 0</option>
    <option value="5">∃x · x³ − x ≥ 0</option>
    <option value="6">∀x · x² ≥ 0</option>
    <option value="7">∀x · x² + 1 > 0</option>
  </select>
</div>
<button id="decide" type="button">{{btn_decide}}</button>
<div id="steps" class="steps"></div>
<div id="verdict" class="verdict"></div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; padding: .5rem; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .8rem; line-height: 1.5; }
.picker { display: flex; flex-direction: column; gap: .3rem; margin-bottom: .7rem; }
label { font-size: .85rem; font-weight: 600; color: #333; }
select { font: 15px system-ui, sans-serif; padding: .4rem .6rem; border: 1px solid #bbb;
         border-radius: 6px; background: #fff; color: #1d3557; max-width: 340px; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem 1.1rem;
         background: #1d3557; color: #fff; border: none; border-radius: 8px; cursor: pointer;
         margin-bottom: .8rem; }
button:hover { background: #274472; }
.steps { display: flex; flex-direction: column; gap: .45rem; }
.step { background: #f0f4f8; border-left: 3px solid #5a7088; border-radius: 0 6px 6px 0;
        padding: .45rem .7rem; font-size: .88rem; line-height: 1.5; }
.step b { color: #1d3557; }
.step code { background: #dce6ef; padding: .05rem .3rem; border-radius: 4px;
             font: 13px ui-monospace, monospace; }
.verdict { font-size: 1.1rem; font-weight: 700; margin-top: .7rem; min-height: 1.5em; }
.verdict.true { color: #0a7d33; }
.verdict.false { color: #c92f3c; }

// Code not found

The key insight: checking whether a specific real number satisfies a polynomial inequality is trivial (just evaluate). Deciding a statement with quantifiers is the hard part — the algorithm eliminates "∃x" by computing the discriminant conditions under which a real solution exists, reducing the problem to a quantifier-free formula. It always terminates with a definitive TRUE or FALSE.

Tarski's 1951 result is remarkable — but the original procedure is doubly exponential in the number of quantifier alternations. A statement with n nested quantifiers may require time proportional to $2^{2^{n}}$ to decide, which is astronomical for even modest n.

This was the state of affairs until 1975, when George Collins introduced Cylindrical Algebraic Decomposition (CAD). CAD decomposes real space into cells where every polynomial in the formula has constant sign, then checks each cell. It is still exponential in the number of variables, but far more practical than Tarski's original method.

• Tarski's original (1951): doubly exponential — decidable, not practical.
• Collins' CAD (1975): singly exponential ($2^{2^{n}}$ → $2^{n}$), the basis of modern computer algebra.
• Lower bound: Ben-Or, Kozen and Reif (1986) proved the problem is PSPACE-hard and in EXPTIME — so no polynomial-time algorithm is expected.

Compare this with integer arithmetic (Peano arithmetic): it is undecidable — not merely slow, but impossible to decide algorithmically (Gödel 1931, Church and Turing 1936). The contrast with real arithmetic is stark. The reason? The real line is dense and has no smallest positive element, so the induction principle that makes integers so expressive (and so hard) simply doesn't apply.

See also the halting problem for the other side of the coin: a decision problem that is genuinely impossible rather than merely slow.

Tarski's theorem is not merely a logical curiosity — it is the theoretical backbone of several active engineering fields:

• Computer algebra systems: tools like Mathematica, Maple and SageMath use variants of CAD to solve polynomial systems, find real roots and simplify algebraic expressions involving inequalities.
• Robot motion planning: can a robot arm move from configuration A to B without hitting obstacles? This is a statement about the reachability of points in real space — decidable by Tarski's framework. Schwartz and Sharir (1983) applied CAD to automate this.
• Formal geometry provers: Wu's method and Gröbner basis approaches decide geometric theorems (collinearity, circle tangency) automatically. The decidability of real closed fields guarantees such provers terminate.
• Satisfiability modulo theories (SMT): modern SMT solvers like Z3 use quantifier-free fragments of real arithmetic daily, handling constraints in program verification and hardware design.
• Optimization over semi-algebraic sets: the feasibility of polynomial programs and sum-of-squares proofs rests on the decidability of the underlying real arithmetic.

The contrast with P vs NP is instructive: that question asks how fast a problem is solvable; Tarski answered whether a whole class of problems is solvable at all — and the answer was yes.

Gödel's incompleteness theorem cast a long shadow over the 1930s: it said that no machine could ever decide all truths of arithmetic. Tarski's answer, two decades later, was subtle and precise — which arithmetic you ask about matters enormously.

Add the single axiom that every positive real has a square root (the "real closed field" axiom), and you gain completeness. Drop down to the integers, and you lose it. The boundary between decidable and undecidable runs right through the number line.

Tarski's theorem — proved in 1951 — remains one of the most satisfying results in mathematical logic: a complete algorithm that decides every geometric truth expressible in first-order logic. Its successors, from Collins' CAD to modern SMT solvers, carry that power into everyday engineering. Whenever a computer algebra system tells you "no real solution exists" or a motion planner guarantees a collision-free path, it is standing on Tarski's shoulders.