Wednesday, November 23, 2011 CC-BY-NC
Prenex normal form

Maintainer: admin

1Converting into prenex normal form

Prenex normal form: when all the quantifiers are at the very left side of the formula.

1.1Allowed moves

  • Change of bound variables
  • Replacing $\neg \forall x \phi$ with $\exists x \neg \phi$ and $\neg \exists x \phi$ with $\forall x \neg \phi$
  • Replacing $(\forall x \Phi) \land (\Psi)$ with $\forall x(\Phi \land \Psi)$ provided $x$ does not occur free in $\Psi$ (if it does, use a different variable for the quantifier). Same with $\exists$. This also works if the quantifier is in the second place.
  • Replacing $\Phi \to \Psi$ by $\neg \Phi \lor \Psi$ (they're equivalent). It's not that you can't use a $\to$ in prenex normal form, it's just that you sometimes have to change it to be able to move the quantifiers. See the first example below.
  • Replacing $\Phi \iff \Psi$ with, for example, $(\Phi \to \Psi) \land (\Psi \to \Phi)$ or $(\Phi \land \Psi) \lor (\neg \Phi \land \neg \Psi)$ or whatever.

Note: if $\Phi$ is equivalent to $\Phi'$ then $\forall a(\Phi)$ is equivalent to $\forall a (\Phi')$.

The wikipedia page on this is pretty good.

1.2In-class examples

$$\exists x Px \to Qy$$

Sequent Explanation
$\neg (\exists x Px) \lor Qy$ The equivalent replacement thing
$(\forall x \neg Px) \lor Qy$ The negation replacement thing
$\forall x (\neg Px \lor Qy)$ Moving the quantifier outside
$\forall x (Px \to Qy)$ Putting the $\to$ back in

More on the HTSEFP page.

$$\forall y (Py \to Qxy) \land \neg \forall x (Px \land \exists y Qxy)$$

See the Fall 2009 final page for the solution.

$$(\exists Pxy \to \forall Qxy) \land \neg \forall y \exists x ((Pxy \lor \neg Qyx) \land \neg Pxz)$$

See the Fall 2010 final page for the solution.

1.3Other examples

Not done in class - found here. Solutions created independently but compared to the provided solutions to ensure accuracy

$$\forall x((\exists y R(x, y) \land \forall y \neg S(x, y)) \to \neg (\exists y R(x, y) \land P))$$

Sequent Justification
$\forall x (\neg(\exists y R(x,y) \land \forall y(\neg S(x,y))) \lor \neg (\exists y R(x, y) \land P)$ Changed the implication into a disjunction
$\forall u (\neg(\exists y R(u,y) \land \forall y(\neg S(u,y))) \lor \neg (\exists y R(x, y) \land P)$ Change of bound variable (x to u)
$\forall u (\neg \exists y R(u, y) \lor \neg \forall y (\neg S(u, y))) \lor (\neg \exists y R(x, y) \lor \neg P)$ Distributed the negation, for both sides
$\forall u (\forall y (\neg R(u, y)) \lor \exists v S(u, v)) \lor \forall y(\neg R(x, y) \lor \neg P) $ Changed $\neg \exists$ to $\forall \neg$ for both sides
... Something, got a bit lost
$\forall y \forall u \exists v \forall w(\neg R(u, y) \lor S(u, v) \lor \neg R(x, w) \lor \neg P)$ Moving things outside