 Solution

A first-order theory $T$ admits quantifier elimination when every first-order formula $\phi (\bar{x})$ has a quantifier-free formula $\psi (\bar{x})$, in the same first-order signature and with no additional free variables, such thatThus all first-order models of $T$ agree that the two first-order formulas define the same tuples. This definition concerns first-order formulas with free variables, as well as first-order sentences; merely deciding closed assertions would be weaker. The existence of an effective procedure is an additional issue, supplied by the explicit construction in part (d).