Definition 11.1 (Theory has quantifier elimination). An $L$-theory $T$ has quantifier elimination (QE) if for any $L$-formula $\phi (x_1,\dots ,x_n)$ ther eis a quantifier free formula $\psi (x_1,\dots ,x_n)$ such that

$$T\models \forall \overline{x}(\phi (\overline{x})\leftrightarrow \psi (\overline{x})).$$

(i.e. they define the same set in all models).