= Solution
A <first-order theory> $T$ admits <quantifier elimination> when every <first-order formula> $\varphi(\bar x)$ has a <quantifier-free formula> $\psi(\bar x)$, in the same <first-order signature> and with no additional <free variables>, such that
$$
\boxed{T\models\forall\bar x\,[\varphi(\bar x)\leftrightarrow\psi(\bar x)].}
$$
Thus 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).
Back to article page
