**Maintainer:**admin

*1*Converting into prenex normal form¶

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

*1.1*Allowed 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.2*In-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.3*Other 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 |