= Solution
A <first-order theory> has <quantifier elimination> if every <first-order formula> is equivalent over the <first-order theory> to a <quantifier-free formula> with the same free variables:
$$
\boxed{\text{for each }\varphi(\mathbf x)\text{ there is quantifier-free }\theta(\mathbf x)\text{ with }T\models\forall\mathbf x(\varphi\leftrightarrow\theta).}
$$
Logical truth and falsity may be treated as the empty Boolean combinations when considering sentences in a language without closed terms. The assertion concerns <first-order formulas> with free variables, not merely sentences.
Back to article page
