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 polynomial equation solvable. ACF has QE. ∃x. x² + 1 = 0 → ⊤ (in ACF).

Real closed fields: Ordered, every positive has sqrt. RCF has QE (Tarski-Seidenberg). Decidable geometry.

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

Presburger arithmetic: (ℤ, +, 0, 1, <). Has QE. Decidable.

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

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.