 A notion that is closely related to model-completeness, but should not be confused with it, is elimination of quantifiers.  Suppose L is a first-order language, T is a theory in L, and Φ is a set of formulas of L.  We say that T has elimination of quantifiers down to Φ if for every formula φ(x1,…,xn) of L there is a formula ψ(x1,…,xn) in Φ such that in every model of T, φ and ψ are satisfied by exactly the same n-tuples of elements (a1,…,an).  (The ‘method of elimination of quantifiers’ discussed in section 2.2 of Tarski’s truth definitions) was a syntactic and pre-model-theoretic method for proving elimination of quantifiers down to a particular set of formulas.)  A theory is said to have quantifier elimination if it has elimination of quantifiers down to quantifier-free formulas. 