Wednesday, November 23, 2011

Prenex normal form

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$$

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))$$