Converting to Prenex Normal Form

I have to convert the following to Prenex Normal Form. I'm not sure what's the best way.

$$\left( \forall x \exists y P(x,y) \leftrightarrow \exists x \forall y \exists z R \left(x,y,z\right)\right)$$

Any ideas/hints on the best way to work?

Thanks!

Solution 1:

Let's do this!

$$\forall x \exists y P(x,y) \leftrightarrow \exists x \forall y \exists z R \left(x,y,z\right)$$

You can't pull quantifiers out of a biconditional, so we have to rewrite it as two conditionals first:

$( \forall x \exists y P(x,y) \rightarrow \exists x \forall y \exists z R (x,y,z)) \land ( \exists x \forall y \exists z R (x,y,z) \rightarrow \forall x \exists y P(x,y) )$

Now let's rename the variables so they all have a unique name:

$\left( \forall x_1 \exists y_1 P(x_1,y_1) \rightarrow \exists x_2 \forall y_2 \exists z_1 R \left(x_2,y_2,z_1 \right)\right) \land \left( \exists x_3 \forall y_3 \exists z_2 R \left(x_3,y_3,z_2 \right) \rightarrow \forall x_4 \exists y_4 P(x_4,y_4) \right)$

Now we can pull out the quantifiers using the following two equivalences (which you can find on the wikipedia page as referenced by Hans):

Where $\varphi$ is a formula that does not contain $x$ as a free variable:

$$\varphi \rightarrow \forall x \ \psi(x) \Leftrightarrow \forall x (\varphi \rightarrow \psi(x))$$

$$\varphi \rightarrow \exists x \ \psi(x) \Leftrightarrow \exists x (\varphi \rightarrow \psi(x))$$

$$\forall x \ \psi(x) \rightarrow \varphi \Leftrightarrow \exists x (\psi(x) \rightarrow \psi)$$

$$\exists x \ \psi(x) \rightarrow \varphi \Leftrightarrow \forall x (\psi(x) \rightarrow \psi)$$

(Note the change in quantifier for the last two!)

OK, applied to what we had:

$\exists x_1 \forall y_1 \exists x_2 \forall y_2 \exists z_1 \left( P(x_1,y_1) \rightarrow R \left(x_2,y_2,z_1 \right)\right) \land \forall x_3 \exists y_3 \forall z_2 \forall x_4 \exists y_4 \left( R \left(x_3,y_3,z_2 \right) \rightarrow P(x_4,y_4) \right)$

And finally we can pull the quantifiers outside the $\land$ using two more Prenex equivalences (also listed on that page):

Where $\varphi$ is a formula that does not contain $x$ as a free variable:

$$\varphi \land \forall x \ \psi(x) \Leftrightarrow \forall x (\varphi \land \psi(x))$$

$$\varphi \land \exists x \ \psi(x) \Leftrightarrow \exists x (\varphi \land \psi(x))$$

Applied to what we had:

$\exists x_1 \forall y_1 \exists x_2 \forall y_2 \exists z_1 \forall x_3 \exists y_3 \forall z_2 \forall x_4 \exists y_4 (( P(x_1,y_1) \rightarrow R \left(x_2,y_2,z_1 \right) \land \left( R \left(x_3,y_3,z_2 \right) \rightarrow P(x_4,y_4) \right))$

And now it is in Prenex Normal Form!

Two final notes:

1. Note how due to the change in quantifier we cannot pull a quantifier outside a biconditional, and have to rewrite as two conditionals.

2. If you are putting the statement in PNF as a precursor to skolemization, you can make your life a bit easier to pull out the existentials before the universals, so you don't have to introduce functions symbols when skolemizing. So, if we had done that on your statement, we could have gotten:

$\exists x_1 \exists x_2 \forall y_2 \exists z_1 \forall x_3 \exists y_3 \forall x_4 \exists y_4 \forall y_1 \forall z_2 (( P(x_1,y_1) \rightarrow R \left(x_2,y_2,z_1 \right) \land \left( R \left(x_3,y_3,z_2 \right) \rightarrow P(x_4,y_4) \right))$

Solution 2:

Hint: Rename the bound variables such that they are all distinct, then move the quantifiers outside using the rules for connectives. See https://en.wikipedia.org/wiki/Prenex_normal_form#Conversion_to_prenex_form for details.