# Quantifier Elimination from Conjunction of Literals is Sufficient

^{1)}To show constructively that a theory has quantifier elimination, it suffices to show that we can eliminate an existential quantifier applied to a conjunction of literals, that is, show that each formula of the form:

where each is a literal, is equivalent to a quantifier-free formula. Indeed, suppose we know how to eliminate quantifiers from conjunctions of formulae, then if is a quantifier-free formula, we can write it in disjunctive normal form

and use the fact that

is equivalent to

Finally, to eliminate a universal quantifier

where is quantifier-free, we transform into disjunctive normal form, and use the fact that is equivalent to

^{1)}

taken from Quantifier Elimination to which it was originally contributed, so the Wikipedia sharing rights apply