Let be a complete-theory. Let
. Then is an elimination set for iff for every
there is some
so that
.
In particular, has quantifier elimination iff the set of quantifier free formulas is an elimination set for . In other words has quantifier elimination iff for every
there is some quantifier free
so that
.