Lemma 11.3.
Assuming that:
T
is an
L
-theory
for any quantifier-free formula
φ
(
x
1
,
…
,
x
n
,
y
)
there is a quantifier-free formula
ψ
(
x
1
,
…
,
x
n
)
such that
T
⊨
∀
x
¯
(
∃
y
φ
(
x
¯
,
y
)
↔
ψ
(
x
¯
)
)
.
Then
T
has
quantifier elimination
.