11 Introduction to Quantifier Elimination

Definition (Definable set). Let T be an L-theory and M⊨T. Then X⊆Mn is definable is there is some L-formula φ(x1,…,xn) such that

X={a¯∈Mn:M⊨φ(a¯)}.

Definition 11.1 (Theory has quantifier elimination). An L-theory T has quantifier elimination (QE) if for any L-formula φ(x1,…,xn) ther eis a quantifier free formula ψ(x1,…,xn) such that

T⊨∀⁡x¯(φ(x¯)↔ψ(x¯)).

(i.e. they define the same set in all models).

Example 11.2.

Lemma 11.3. Assuming that:

  • T is an L-theory

  • for any quantifier-free formula φ(x1,…,xn,y) there is a quantifier-free formula ψ(x1,…,xn) such that

    T⊨∀⁡x¯(∃⁡yφ(x¯,y)↔ψ(x¯)).

Proof. Exercise: induction on the complexity of formulas. □

Theorem 11.4. Assuming that:

  • T an L-theory

Then the following are equivalent:
  • (i) T has quantifier elimination
  • (ii) Let M,N⊨T, A⊆M, A⊆N (substructures). For any quantifier-free formula φ(x1,…,xn,y) and tuple a¯∈A, if M⊨∃⁡y,φ(a¯,y) then N⊨∃⁡y,φ(a¯,y).
  • (iii) For any L-structure A, T∪D(A) is a complete LA-theory.

Proof.

Remark.