Differences

This shows you the differences between two versions of the page.

--- sav08:qe_from_conjunction_of_literals_suffices [2008/04/09 21:08]
vkuncak created
+++ sav08:qe_from_conjunction_of_literals_suffices [2009/04/21 19:02]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Quantifier Elimination from Conjunction of Literals is Sufficient ======
+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 [[wp>literal (mathematical logic)|literal]]s, that is, show that each formula of the form:
+\[
+   \exists x. \bigwedge_{i=1}^n L_i
+\]
+where each $L_i$ is a literal, is equivalent to a quantifier-free formula. Indeed, suppose we know how to eliminate quantifiers from conjunctions of formulae, then if $F$ is a quantifier-free formula, we can write it in [[wp>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 $F$ is quantifier-free, we transform $\lnot F$ into disjunctive normal form, and use the fact that $\forall x. F$ is equivalent to $\lnot \exists x. \lnot F.$
+(taken fro [[wp>Quantifier Elimination]] to which it was contributed, thus the visibility rules apply)