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.

  • (1) Let T=Th(F), F a field in Lrings. Let φ(w,x,y,z) be the formula saying
    “(wxyz) has an inverse”,

    i.e.

    ∃⁡s,t,u,v[(stuv)(wxyz)=(1001)].

    Then

    T⊨∀⁡x,w,y,z(φ(w,x,y,z)⟺wz−xy≠0).
  • (2) Let T=Th(ℝ,⋅,+,0,1). Consider φ(x)=∃⁡y(y2=x) (this defines ℝ≥0).

    Quantifier free formulas in one variable are boolean combinations of polynomial equations, i.e. define sets of size finite or cofinite. But ℝ≥0 is infinite-co-infinite, so cannot be defined by a quantifier free formula.

    Remark: Th(ℝ,⋅,+,0,1) does have quantifier elimination.

    We can show Th(ℝ,⋅,+,0,1) and Th(ℝ,⋅,+,0,1,<) have the same definable sets.

    This is because we can define < in Lrings in T by noting x<y if and only if

    ∃⁡z(z≠0∧y−z2=x).

    Note: you can always find a language in which the theory of a structure has quantifier elimination: just add a relation symbol for each non quantifier-free formula. This is called the “Morleyisation” of a structure, but isn’t particularly informative.

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.

  • (i) ⟹ (iii) Assume T has quantifier elimination, and let A be an L-structure. Suppose M,N⊨T∪D(A). We want to show M≡LAN.

    Let σ be an LA-sentence, and suppose that M⊨σ. Then σ can be written as φ(a¯) where φ(x¯) is an L-formula and a¯∈A.

    By quantifier elimination, we have ψ(x¯) such that

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

    Now M⊨T, so M⊨∀⁡x¯(φ(x¯)↔ψ(x¯)), and M⊨φ(a¯). So M⊨ψ(a¯). Now ψ(a¯)∈D(A) as M⊨D(A). So N⊨ψ(a¯), as N⊨D(A). Hence N⊨φ(a¯) as N⊨T (i.e. N⊨∀⁡x¯(φ(x¯)↔ψ(x¯))). So N⊨σ.

  • (iii) ⟹ (ii) Let M,N⊨T, A⊆M, A⊆N. Let φ(x¯,y) be a quantifier free formula and let a¯∈A such that M⊨∃⁡yφ(a¯,y).

    As A⊆M, A⊆N, we have M,N⊨T∪D(A), so by (iii) we have M≡LAN so N⊨∃⁡φ(a¯,y).

  • (ii) ⟹ (i) We want to show quantifier elimination.

    By Lemma 11.3, it is sufficient to show for φ(x¯,y) quantifier free, we can find ψ(x¯) quantifier free such that

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

    Let L∗=L∪{c1,…,cn} where each ci is a new constant (with n=|x¯|). Let

    Γ={ψ(c¯):ψ(x¯) quantifier free formula such that T⊨∀⁡x¯,(∃⁡y,φ(x¯,y)→ψ(x¯))}.

    In definable sets:

    PIC

    Claim: T∪Γ⊨∃⁡y,φ(c¯,y).

    Proof: Suppose not. Then there is an L∗-structure

    N⊨T∪Γ∪{¬⁡∃⁡y,φ(c¯,y)}.

    Let ai=ciN, and let A⊆N be the substructure generated by a1,…,an in N.

    Then N⊨T, A⊆N, N⊨¬⁡∃⁡y,φ(c¯,y). Any b∈A is of the form tN(a¯) for an L-term t (exercise).

    So D(A) can be viewed as an L∗-structure by replacing b̲ (b=tN(a¯)) with t(c¯) in L∗. Let

    Σ=T∪D(A)∪{∃⁡y,φ(x¯,y)}.

    IDEA: build M⊨Σ, M⊨T∪D(A) and M⊨∃⁡y,φ(a¯,Y), contradicting (ii).

    Suffices to prove Σ is consistent.

    Assume Σ is inconsistent. Then by compactness we have ψ1(x¯),…,ψn(x¯) quantifier free L-formulas with

    • ψ1(c¯),…,ψm(c¯)∈D(A).

    • T∪{∧⁡i=1mψi(c¯)}∪{∃⁡y,φ(c¯,y)} is unsatisfiable.

    In definable sets:

    PIC

    Let ψ(x¯) be ¬⁡∧⁡i=1mψi(x¯), then T⊨∃⁡y,φ(c¯,y)→ψ(c¯).

    So T⊨∀⁡x¯(∃⁡y,φ(x¯,y)→ψ(x¯)) so ψ(c¯)∈Γ. So N⊨ψ(c¯) but also N⊨D(A) (A⊆N). Then

    N⊨∧i=1mψi(c¯)⏟∈D(A)=¬⁡ψ(c¯)

    contradiction. So by compactness, Σ is consistent.

    This proves the claim.

    Reminder: the claim was that T∪Γ⊨∃⁡y,φ(x¯,y). So by compactness, there are ψ1(x¯),…,ψm(x¯) quantifier free such that

    T∪{ψ(c¯),…⁡,ψm(c¯)}⏟⊆Γ⊨∃⁡y,φ(x¯,y).

    Recall

    T⊨∀⁡x¯(∃⁡y,φ(x¯,y)→∧i=1mψi(x¯))

    by choice of n. Let

    ψ(x¯)=∧i=1mψi(x¯).

    Then

    T⊨ψ(c¯)→∃⁡y,φ(c¯,y)

    hence

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

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

Remark.

  • (1) In (iii) we may assume A⊆M⊨T, as otherwise T∪D(A) is inconsistent and hence trivially complete.
  • (2) In (ii) and (iii) we may assume A is finitely generated.