Quantifier Elimination

Abstract

Let L be a language. It may happen that two different L-formulas $\phi (\vec v)$ and $\phi '(\vec v)$ admit the same meaning in a structure A of L, or in a class of L-structures, for instance among the models of a given L-theory T. For example, in the ordered field of reals (and even in every real closed field), the formula ϕ(v):v≥0 (being nonnegative) is the same thing as ϕ′(v):∃w(v=w²) (being a square). Similarly, in the ordered domain of integers, ϕ(v):v≥0 (being positive) has the same interpretation as ϕ′(v):∃w₁∃w₂∃w₃∃w₄(v=∑_1≤i≤4w ² _i ) (being the sum of four squares): this is a celebrated theorem of Lagrange, already mentioned in the last chapter.