Quantifier Elimination

Origin. The method predates its name: Löwenheim (1915) and Skolem used elimination for the calculus of relatives, Langford (1927) for dense linear orders, Presburger (1929) for the additive integers. Tarski turned it into a general technique and applied it to real closed fields in work of the early 1930s, published as A Decision Method for Elementary Algebra and Geometry (1948, revised 1951). Remove quantifiers from formulas. Quantifier-free equivalents. Decidability. Foundation for effective model theory.

Models. Every formula equivalent to quantifier-free. Theory has QE. Algebraically closed fields. Real closed fields.

Formalism.

Definition: Theory T has QE iff for every φ(x̄): ∃ψ quantifier-free with T ⊨ φ ↔ ψ.

Equivalently: Eliminate one quantifier at a time. ∃x.φ → quantifier-free.

Test for QE: Model-theoretic criterion. Substructure completeness. Amalgamation property.

Algebraically closed fields: Every non-constant polynomial has a root. ACF has QE. ∃x. x² + 1 = 0 → ⊤ (in ACF).

Real closed fields: An ordered field in which every positive element has a square root and every odd-degree polynomial has a root. Both conditions are needed: the field of ruler-and-compass constructible reals satisfies the first, being closed under square roots, yet x³ − 2 has no root in it, so it is Euclidean but not real closed. RCF has QE (Tarski-Seidenberg). Decidable geometry.

Dense linear orders: DLO has QE. ∃x. a < x < b → a < b.

Presburger arithmetic: (ℤ, +, 0, 1, <) — QE only after expanding the language. Add a congruence predicate x ≡ₙ y for each n ≥ 2; Presburger arithmetic then has QE (Presburger 1929) and is decidable. In the bare language it does not. ∃y (x = y + y) defines the even numbers, and no quantifier-free formula can: over ℤ with only +, <, 0 and 1, an atomic formula in one free variable defines a point or a half-line, so every quantifier-free definable set is a finite union of points and intervals. The evens are not one. This is the standard illustration that QE is a property of a theory in a language, not of a theory — the contrast with DLO, which eliminates in its own signature with nothing added.

Consequences: Decidability: check QF sentences. Definable sets: Boolean combinations of basic. Completeness: often follows.

QE procedure: Fourier-Motzkin (linear). CAD (real closed fields). Gröbner (polynomial).

Symbols.

Metatheory. T has QE iff it is substructure complete: whenever A is a common substructure of models M and N of T, M and N satisfy the same formulas with parameters from A. The usable form is the one-quantifier test: it suffices to eliminate a single existential in front of a conjunction of literals. QE implies model completeness, but not conversely: real closed fields in the ring language are model complete, since the order is definable by ∃y (y² = x), yet lack QE there. QE is a property of a theory in a signature, not of a theory: Morleyization — adding a relation symbol for every formula — gives any theory QE, so the claim is informative only for a fixed natural language. Nor does QE by itself give decidability; one needs the elimination to be effective and the quantifier-free sentences decidable. Classical instances: Langford (1927) for dense linear orders, Presburger (1929) for (ℤ, +, <) with congruences, Tarski for ACF and RCF, Abraham Robinson for algebraically closed valued fields, Macintyre (1976) for the p-adics after adding n-th power predicates.

Applies to. Decision procedures. SMT solving. Algebraic geometry. Verification. Database optimization.

Limitations. Because QE is signature-relative, "T has QE" asserts nothing about T alone — Morleyization supplies it trivially, and Presburger arithmetic loses it the moment the congruence predicates are dropped. Th(ℕ, +, ·) admits no effective quantifier elimination in any recursive expansion with a decidable set of quantifier-free sentences, since that would decide arithmetic. Where elimination does hold it is expensive: Fischer and Rabin (1974) proved a 2^{2^{cn}} nondeterministic lower bound for the theory of (ℕ, +), Oppen (1978) a triply exponential upper bound for its elimination procedure, and Davenport and Heintz (1988) a doubly exponential lower bound for elimination in real closed fields — so the blow-up in cylindrical algebraic decomposition is intrinsic and not an artifact. Expansions break the property routinely: adding an integer-part predicate to RCF costs not only QE but decidability, since the result interprets arithmetic.

© 2026 Lingenic LLC