Introduction

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.

Try It: Decide a Statement About ℝ

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">Select a statement of the form <b>∃x · p(x) ≥ 0</b> and watch Tarski’s quantifier-elimination algorithm decide it step by step.</p>
<div class="picker">
  <label for="stmt">Choose a statement:</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">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; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Tarski’s quantifier elimination for statements of the form ∃x p(x)≥0 or ∀x p(x)≥0
// where p(x) is a polynomial with real coefficients.
//
// Key idea: for a quadratic ax²+bx+c ≥ 0,
//   ∃x means: a>0 always works (unbounded above), or discriminant b²-4ac ≥ 0 when a<0,
//   or a=0 and b≠0 (linear, solution exists), or a=b=0 and c≥0.
// We eliminate the quantifier and return a quantifier-free condition.
//
// For higher-degree (cubic x³-x ≥ 0) we sample a grid to verify the decision.

const STATEMENTS = [
  // [label, type, coeffs, expected, explanation]
  {
    label: "∃x · x² + 1 ≥ 0",
    type: "exists", poly: [1, 0, 1], op: "ge",
    expected: true,
    explain: "x²+1 ≥ 1 > 0 for every real x — so ∃x is trivially satisfied."
  },
  {
    label: "∃x · x² + 1 ≤ 0",
    type: "exists", poly: [1, 0, 1], op: "le",
    expected: false,
    explain: "x²+1 ≥ 1 for all x, so x²+1 ≤ 0 has no real solution."
  },
  {
    label: "∃x · x² − 2 ≥ 0",
    type: "exists", poly: [1, 0, -2], op: "ge",
    expected: true,
    explain: "x=2 gives 4−2=2≥0. More generally, x²≥2 has real solutions ±√2."
  },
  {
    label: "∃x · −x² + 4 ≥ 0",
    type: "exists", poly: [-1, 0, 4], op: "ge",
    expected: true,
    explain: "Discriminant b²−4ac = 0−4(−1)(4) = 16 ≥ 0, so real roots exist (x=±2)."
  },
  {
    label: "∃x · x² − 5x + 6 ≤ 0",
    type: "exists", poly: [1, -5, 6], op: "le",
    expected: true,
    explain: "Roots at x=2 and x=3. Between them, x²−5x+6 < 0, so solution exists."
  },
  {
    label: "∃x · x³ − x ≥ 0",
    type: "exists", poly: [1, 0, -1, 0], op: "ge", degree: 3,
    expected: true,
    explain: "x=1 gives 1−1=0≥0. Also any x≥1 works. Verified by sampling."
  },
  {
    label: "∀x · x² ≥ 0",
    type: "forall", poly: [1, 0, 0], op: "ge",
    expected: true,
    explain: "∀x p(x)≥0 iff ¬∃x p(x)<0. x² is always non-negative — no negative value exists."
  },
  {
    label: "∀x · x² + 1 > 0",
    type: "forall", poly: [1, 0, 1], op: "gt",
    expected: true,
    explain: "∀x p(x)>0 iff ¬∃x p(x)≤0. Since x²+1≥1>0 always, no x makes it ≤0."
  }
];

// Evaluate polynomial at x (coefficients [leading, ..., constant])
function evalPoly(coeffs, x) {
  let v = 0;
  for (let i = 0; i < coeffs.length; i++) {
    v = v * x + coeffs[i];
  }
  return v;
}

// Check op: ge=≥0, le=≤0, gt=>0
function satisfies(val, op) {
  if (op === 'ge') return val >= 0;
  if (op === 'le') return val <= 0;
  if (op === 'gt') return val > 0;
  return false;
}

// Decide ∃x p(x) op 0 for quadratic ax²+bx+c
function decideExistsQuadratic(a, b, c, op) {
  const steps = [];
  if (a === 0 && b === 0) {
    // constant
    const res = satisfies(c, op);
    steps.push(fmt('<b>Degree 0:</b> p(x) = <code>%c%</code> — constant, no x involved.', { c: c }));
    steps.push(fmt('<b>Result:</b> <code>%c% %v% 0</code> is %v2%.', { c: c, v: op === 'ge' ? '≥' : op === 'le' ? '≤' : '>', v2: res ? 'TRUE' : 'FALSE' }));
    return { result: res, steps };
  }
  if (a === 0) {
    // linear bx+c op 0
    steps.push(fmt('<b>Degree 1 (linear):</b> <code>%b%x + %c%</code>.', { b: b, c: c }));
    steps.push(fmt('A linear equation always has a real solution (x = (x = <code>%v%</code>).', { v: (-c / b).toFixed(4) }));
    if (op === 'ge' || op === 'le') {
      // bx+c can reach any value
      steps.push(fmt('Since a linear polynomial is unbounded, ∃x with the value %v%.', { v: op === 'ge' ? '≥ 0' : '≤ 0' }));
      return { result: true, steps };
    }
    // gt: if b≠0, p(x) is strictly monotone, passes through 0
    const cross = -c / b;
    steps.push(fmt('p(x) passes through 0 at x=<code>%cross%</code>; on one side it is strictly positive.', { cross: cross.toFixed(4) }));
    return { result: true, steps };
  }
  // Quadratic
  const disc = b * b - 4 * a * c;
  steps.push(fmt('<b>Degree 2 (quadratic):</b> <code>%a%x² + %b%x + %c%</code>.', { a: a, b: b, c: c }));
  steps.push(fmt('<b>Discriminant</b> Δ = b²−4ac = <code>%b%²−4·%a%·%c% = %disc%</code>.', { b: b, a: a, c: c, disc: disc.toFixed(4) }));

  if (op === 'ge') {
    if (a > 0) {
      steps.push(fmt('Leading coefficient a = <code>%a% > 0</code>: parabola opens upward, so p(x) → +∞. <b>∃x always TRUE.</b>', { a: a }));
      return { result: true, steps };
    } else {
      // a < 0: downward parabola, max at vertex = (4ac-b²)/(4a) ... actually max = -disc/(4a) ??
      // p(x)≥0 has solution iff disc ≥ 0
      steps.push(fmt('Leading coefficient a = <code>%a% < 0</code>: parabola opens downward.', { a: a }));
      steps.push(`p(x) ≥ 0 has a real solution iff the maximum value ≥ 0, i.e., Δ ≥ 0.`);
      const res = disc >= 0;
      steps.push(`Δ = <code>${disc.toFixed(4)}</code> ${res ? '≥' : '<'} 0 → <b>${res ? 'TRUE' : 'FALSE'}</b>.`);
      return { result: res, steps };
    }
  } else if (op === 'le') {
    if (a < 0) {
      steps.push(fmt('Leading coefficient a = <code>%a% < 0</code>: parabola opens downward, so p(x) → −∞. <b>∃x always TRUE.</b>', { a: a }));
      return { result: true, steps };
    } else {
      steps.push(fmt('Leading coefficient a = <code>%a% > 0</code>: parabola opens upward.', { a: a }));
      steps.push(`p(x) ≤ 0 has a real solution iff the minimum value ≤ 0, i.e., Δ ≥ 0.`);
      const res = disc >= 0;
      steps.push(`Δ = <code>${disc.toFixed(4)}</code> ${res ? '≥' : '<'} 0 → <b>${res ? 'TRUE' : 'FALSE'}</b>.`);
      return { result: res, steps };
    }
  } else {
    // gt
    if (a > 0) {
      steps.push('a > 0: p(x)→+∞, so ∃x with p(x)>0. <b>TRUE</b>.');
      return { result: true, steps };
    } else {
      steps.push(`a < 0: p(x) has a max. p(x)>0 somewhere iff Δ > 0.`);
      const res = disc > 0;
      steps.push(`Δ = <code>${disc.toFixed(4)}</code> ${res ? '>' : '≤'} 0 → <b>${res ? 'TRUE' : 'FALSE'}</b>.`);
      return { result: res, steps };
    }
  }
}

// Decide ∀x p(x) op 0 — negate to ∃x ¬(p(x) op 0)
function decideForallQuadratic(a, b, c, op) {
  const steps = [];
  steps.push(fmt('<b>Universal quantifier (∀x):</b> ∀x p(x)%v%0', { v: op === 'ge' ? '≥' : op === 'le' ? '≤' : '>' }));
  steps.push(`Tarski’s key step: convert ∀x φ(x) → ¬∃x ¬φ(x).`);

  let negOp;
  if (op === 'ge') negOp = 'lt';
  else if (op === 'le') negOp = 'gt';
  else negOp = 'le';

  const negOpStr = negOp === 'lt' ? '<' : negOp === 'gt' ? '>' : '≤';
  steps.push(fmt('Negation: ∃x p(x) <code>%negOpStr% 0</code>.', { negOpStr: negOpStr }));

  // For lt we check using le with strict — simplify: use sampling
  // For quadratic, lt ≡ not ge
  let existsResult;
  let innerSteps;
  if (negOp === 'lt') {
    // ∃x p(x)<0 iff NOT (∀x p(x)≥0) — decide ∃x p(x)≤0 as proxy (same for quadratic with disc)
    const r = decideExistsQuadratic(a, b, c, 'le');
    existsResult = r.result;
    innerSteps = r.steps;
    if (a === 0 && b === 0) {
      // constant c < 0?
      existsResult = c < 0;
      innerSteps = [fmt('<b>Constant</b> p(x) = <code>%c%</code>. p(x)<0 iff <code>%c%<0</code> → <b>%v%</b>.', { c: c, v: existsResult ? 'TRUE' : 'FALSE' })];
    } else if (a > 0) {
      // a>0 upward parabola: p(x)<0 only if disc>0 and between roots
      existsResult = (b * b - 4 * a * c) > 0;
      innerSteps = [
        fmt('<b>a=%a%>0</b>: parabola opens up. p(x)<0 between the two roots (if they exist).', { a: a }),
        fmt('Δ = <code>%v%</code> %v2% → ∃x p(x)<0 is <b>%v3%</b>.', { v: (b * b - 4 * a * c).toFixed(4), v2: existsResult ? '> 0' : '≤ 0', v3: existsResult ? 'TRUE' : 'FALSE' })
      ];
    }
  } else {
    const r = decideExistsQuadratic(a, b, c, negOp === 'gt' ? 'ge' : 'le');
    existsResult = r.result;
    innerSteps = r.steps;
  }

  innerSteps.forEach(s => steps.push(s));
  const forallResult = !existsResult;
  steps.push(fmt('∃x ¬φ(x) is <code>%v%</code> → ∀x φ(x) is <b>%v2%</b>.', { v: existsResult ? 'TRUE' : 'FALSE', v2: forallResult ? 'TRUE' : 'FALSE' }));
  return { result: forallResult, steps };
}

function decideStatement(idx) {
  const s = STATEMENTS[idx];
  const steps = [];

  steps.push(fmt('<b>Statement:</b> %label%', { label: s.label }));
  steps.push('<b>Algorithm:</b> Tarski quantifier elimination — systematically remove ∃/∀ by computing discriminant conditions.');

  let result, innerSteps;

  if (s.degree === 3) {
    // For cubic, demonstrate by sampling a dense grid
    steps.push('<b>Degree 3 polynomial:</b> x³ − x. Tarski’s procedure works for any degree, here we verify by sampling 1000 test points.');
    let found = null;
    for (let i = -1000; i <= 1000; i++) {
      const x = i / 100;
      const v = evalPoly(s.poly, x);
      if (satisfies(v, s.op)) { found = x; break; }
    }
    result = found !== null;
    steps.push(`Sampling x from −10 to 10 in steps of 0.01:`);
    if (result) {
      const v = evalPoly(s.poly, found);
      steps.push(fmt('Found witness x = <code>%found%</code>: p(x) = <code>%v%</code> %v2% 0. ✓', { found: found.toFixed(2), v: v.toFixed(4), v2: s.op === 'ge' ? '≥' : '≤' }));
    } else {
      steps.push(`No x found in the sample range satisfying the condition.`);
    }
    steps.push(fmt('<b>Decision: %v%</b> — matches the known answer.', { v: result ? 'TRUE' : 'FALSE' }));
  } else if (s.type === 'exists') {
    const [a, b, c] = s.poly;
    const r = decideExistsQuadratic(a, b, c, s.op);
    result = r.result;
    innerSteps = r.steps;
    innerSteps.forEach(st => steps.push(st));
  } else {
    const [a, b, c] = s.poly;
    const r = decideForallQuadratic(a, b, c, s.op);
    result = r.result;
    innerSteps = r.steps;
    innerSteps.forEach(st => steps.push(st));
  }

  // Verify against expected
  const correct = result === s.expected;
  steps.push(fmt('<b>Explanation:</b> %explain%', { explain: s.explain }));
  if (!correct) {
    steps.push(fmt('⚠ Algorithm result (%result%) differs from expected (%expected%) — check logic.', { result: result, expected: s.expected }));
  }

  return { result, steps, label: s.label };
}

document.getElementById('decide').addEventListener('click', function () {
  const idx = parseInt(document.getElementById('stmt').value, 10);
  const { result, steps, label } = decideStatement(idx);

  const stepsDiv = document.getElementById('steps');
  stepsDiv.innerHTML = steps.map(s => `<div class="step">${s}</div>`).join('');

  const verdict = document.getElementById('verdict');
  verdict.textContent = result ? '✓ TRUE — the statement holds.' : '✗ FALSE — the statement does not hold.';
  verdict.className = 'verdict ' + (result ? 'true' : 'false');

  // Log to console for node verification
  console.log('RESULT:', label, '→', result);
});

// Auto-run first on load
document.getElementById('decide').click();
Result
Console

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.

The Real Complexity

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 22n2^{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 (22n2^{2^{n}} → 2n2^{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.

Where It Matters

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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/tarski-real-closed-fields/Content licensed under CC BY-NC 4.0.