A topic in the Open Knowledge Graph — a free, open map of 15,290 topics and the order to learn them in.
A theory T admits quantifier elimination (QE) if every formula is logically equivalent to a quantifier-free formula within T. Theories with QE have drastically simplified model theory: complexity reduces to the quantifier-free fragment. If the quantifier-free theory is decidable, the full first-order theory is decidable.
From your study of complete first-order theories, you know that a theory is complete if it decides every sentence — either the sentence or its negation is a theorem. But completeness is not the same as computability: we need an algorithm to decide which sentences are theorems. Quantifier elimination is the main technique for turning completeness into a decision procedure, and it works by stripping quantifiers away until only quantifier-free formulas remain.
A theory T admits quantifier elimination (QE) if for every first-order formula φ(x̄) — which may contain existential and universal quantifiers — there is a quantifier-free formula ψ(x̄) that is logically equivalent to φ in every model of T. "Quantifier-free" means built from atomic formulas (equalities, inequalities, function applications) and Boolean connectives, with no ∃ or ∀. The claim is dramatic: all the complexity of nested quantifiers collapses to something elementary.
The canonical example is the theory of real closed fields (RCF) — the first-order theory of the real numbers with +, ·, < and 0, 1. Every formula in this language, no matter how deeply nested its quantifiers, is equivalent in RCF to a Boolean combination of polynomial equalities and inequalities like p(x₁, …, xₙ) ≥ 0. This is Tarski's theorem (1948), and it has a surprising consequence: the first-order theory of the reals is decidable. An algorithm exists that takes any first-order sentence about real-number arithmetic and outputs "true" or "false." Note the contrast with number theory over ℤ, where Gödel's incompleteness and undecidability results apply — the difference lies precisely in whether QE holds. The ordered field axioms with completeness over ℝ admit QE; Peano arithmetic does not.
The proof strategy for QE typically proceeds by induction on formula complexity. The key step is eliminating a single block of existential quantifiers: given ∃y φ(x̄, y) where φ is already quantifier-free, find an equivalent quantifier-free formula in x̄ alone. For real closed fields, this is done via cylindrical algebraic decomposition or older elimination-of-quantifiers algorithms. For simpler theories — like the theory of dense linear orders without endpoints (the rationals with <) — the elimination is almost immediate: ∃y (a < y ∧ y < b) is equivalent to a < b.
The decidability payoff generalizes: if T admits QE, then T is decidable if and only if its quantifier-free theory is decidable. Since quantifier-free formulas have a simple Boolean structure, decidability reduces to deciding atomic formulas — questions like "is this polynomial inequality always satisfiable?" which are often algorithmically tractable. QE thus converts a logic problem (can this sentence be proved or refuted in T?) into an algebraic problem, making the boundary between logic and computation visible.