Real Closed Fields (RCF)

Origin. Artin and Schreier (1927) gave the algebraic theory of real closed fields and used it to solve Hilbert's seventeenth problem. Tarski proved quantifier elimination, completeness, and decidability for the ordered field of reals — work of the early 1930s, delayed by the war, published as A Decision Method for Elementary Algebra and Geometry (1948, revised 1951). Collins (1975) gave cylindrical algebraic decomposition, the first implementable procedure. Van den Dries, Pillay, and Steinhorn founded o-minimality (1980s) with RCF as the motivating case.

Models. Ordered fields in which every positive element is a square and every odd-degree polynomial has a root. The reals are one, the real algebraic numbers are another, and the theory cannot tell them apart — Tarski's theorem says all real closed fields satisfy the same first-order sentences, so elementary real geometry is the same over ℝ and over ℝ_alg. That is the decidability result: the first-order theory of the real numbers, with addition, multiplication, and order, is decidable, and the fact sits directly against arithmetic's undecidability.

Formalism.

Language: +, ×, −, 0, 1, < (ordered rings).

Axioms of RCF: the ordered field axioms, plus R1. ∀x (x > 0 → ∃y (y² = x)) (positives are squares) R2. for each n ≥ 1, one axiom: ∀a₀…∀a_{2n} ∃x (x^{2n+1} + Σ_{i≤2n} aᵢxⁱ = 0) (odd-degree polynomials have roots)

Equivalently: an ordered field is real closed iff it is definably complete; iff its algebraic closure is a degree-2 extension (F[i] is algebraically closed); iff it satisfies the intermediate value theorem for polynomials.

Quantifier elimination (Tarski): every formula in the ordered-ring language is equivalent, modulo RCF, to a Boolean combination of polynomial inequalities f(x̄) ≥ 0. Consequences:

• RCF is complete: all real closed fields are elementarily equivalent, including ℝ, ℝ_alg, the real Puiseux series, and the computable reals.
• RCF is decidable — Tarski's theorem.
• Definable sets are exactly the semialgebraic sets — finite Boolean combinations of {f > 0}. The Tarski–Seidenberg theorem (projections of semialgebraic sets are semialgebraic) is QE restated.
• Model complete.

O-minimality: every definable subset of a model in one variable is a finite union of points and intervals. RCF is the motivating o-minimal theory. Cell decomposition, definable choice, the monotonicity theorem, and finiteness of the number of connected components all follow, and they transfer to the o-minimal expansions ℝ_an, ℝ_exp (Wilkie 1996), and ℝ_an,exp.

Complexity: Tarski's original procedure is non-elementary. Collins (CAD, 1975): doubly exponential in the number of variables. Ben-Or, Kozen, Reif; Renegar (1992): the existential fragment is in PSPACE, decidable in (sd)^O(n) arithmetic operations for n variables, s polynomials, degree d — singly exponential. Davenport and Heintz (1988): a doubly exponential lower bound for QE with alternating quantifiers. So CAD's blow-up is not an artifact of the algorithm.

Hilbert's seventeenth problem (Artin 1927): every positive semidefinite rational function over ℝ is a sum of squares of rational functions. The model-theoretic proof is a page from model completeness of RCF.

Bi-interpretability with geometry: Tarski's elementary geometry and RCF are bi-interpretable — the models of the geometry are exactly the planes F² for F real closed. That is why the geometry is complete and decidable, and it is where the two entries meet.

Symbols.

Metatheory. Tarski's theorem is the sharpest statement in the collection of what makes arithmetic undecidable: RCF has addition, multiplication, order, and a domain containing ℕ as a subset — and is decidable, because ℕ is not definable in it. Definability, not presence, is what codes sequences and what Gödel's argument needs. The o-minimality of RCF is the modern explanation of the same fact: definable sets in one variable are finite unions of intervals, so no definable set is an infinite discrete one, so no ℕ. Everything else follows from QE — completeness across all real closed fields, Tarski–Seidenberg, semialgebraic geometry, Artin's solution to Hilbert 17. The doubly exponential lower bound is unconditional and makes RCF, like Presburger arithmetic, a theory that is decidable and infeasible at once.

Applies to. Real algebraic geometry — semialgebraic sets are RCF's definable sets, by definition and by theorem. Robotics motion planning, where the configuration space is semialgebraic and CAD is the exact algorithm. Program verification and SMT solving over nonlinear real arithmetic. Control theory and hybrid systems. Optimization, through positivstellensätze and sums-of-squares relaxations. Geometry, via the bi-interpretation with Tarski's axioms.

Limitations. Doubly exponential in the number of variables, with a matching lower bound — CAD is unusable past a handful of variables, and the singly-exponential existential procedures are still not practical at scale. The theory cannot express completeness of the order, integrality, or anything about ℕ; adding the predicate "x ∈ ℤ" makes it undecidable immediately, since it then interprets PA. Adding exp preserves o-minimality (Wilkie) but decidability of ℝ_exp is open and known to follow from Schanuel's conjecture (Macintyre–Wilkie). The completeness result is about elementary geometry and analysis only: every interesting statement of real analysis quantifies over sets and is therefore outside the language.

© 2026 Lingenic LLC