Quantifier Elimination

Origin. Tarski (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.

Symbol	Unicode	Name	Meaning
QE	—	Quantifier elimination	Remove ∃∀
∃	U+2203	Existential	To eliminate
QF	—	Quantifier-free	Target
≡ₙ	U+2261	Congruence mod n	The expansion Presburger QE requires

Metatheory. Implies decidability. Model completeness related. Effective if procedure exists. Complexity varies.

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

Limitations. Not all theories have QE. Complexity can be high. Extensions lose QE.