This is an old revision of the document!
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: \[
\exists x. \bigwedge_{i=1}^n L_i
\] 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 \[
\bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij}
\] and use the fact that \[
\exists x. \bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij}
\] is equivalent to \[
\bigvee_{j=1}^m \exists x. \bigwedge_{i=1}^n L_{ij}
\]
Finally, to eliminate a universal quantifier \[
\forall x. F
\] where is quantifier-free, we transform into disjunctive normal form, and use the fact that is equivalent to