• English only

# Differences

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

 sav08:qe_from_conjunction_of_literals_suffices [2009/04/21 19:04]vkuncak sav08:qe_from_conjunction_of_literals_suffices [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2009/04/21 19:04 vkuncak 2009/04/21 19:04 vkuncak 2009/04/21 19:03 vkuncak 2009/04/21 19:03 vkuncak 2009/04/21 19:02 vkuncak 2009/04/21 19:02 vkuncak 2008/04/09 21:08 vkuncak created Next revision Previous revision 2009/04/21 19:04 vkuncak 2009/04/21 19:04 vkuncak 2009/04/21 19:03 vkuncak 2009/04/21 19:03 vkuncak 2009/04/21 19:02 vkuncak 2009/04/21 19:02 vkuncak 2008/04/09 21:08 vkuncak created Line 1: Line 1: ====== Quantifier Elimination from Conjunction of Literals is Sufficient ====== ====== 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: + ((taken from [[wp>​Quantifier Elimination]] to which it was originally contributed,​ so the Wikipedia sharing rights apply))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: - \[ + \begin{equation*} ​\exists x. \bigwedge_{i=1}^n L_i ​\exists x. \bigwedge_{i=1}^n L_i - \] + \end{equation*} 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]] ​ 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]] ​ - \[ + \begin{equation*} ​\bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij} ​\bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij} - \] + \end{equation*} and use the fact that and use the fact that - \[ + \begin{equation*} ​\exists x. \bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij} ​\exists x. \bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij} - \] + \end{equation*} is equivalent to is equivalent to - \[ + \begin{equation*} ​\bigvee_{j=1}^m \exists x. \bigwedge_{i=1}^n L_{ij} ​\bigvee_{j=1}^m \exists x. \bigwedge_{i=1}^n L_{ij} - \] + \end{equation*} Finally, to eliminate a universal quantifier ​ Finally, to eliminate a universal quantifier ​ - \[ + \begin{equation*} ​\forall x. F ​\forall x. F - \] + \end{equation*} 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.\$ 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 from [[wp>​Quantifier Elimination]] to which it was originally contributed,​ so the Wikipedia sharing rights apply))