Doubts finding a Prenex normal form $ \exists x\alpha\vee\exists y\beta=\exists x(\alpha\vee\beta) $

Question

I'm getting troubles when finding a Prenex Normal form of a formula at First-order logic exercises... and ask for help:

First, I know the equivalence:

$$ \forall x \alpha\wedge\forall y\beta=\forall x(\alpha\wedge\beta) $$

and

$$ \exists x\alpha\vee\exists y\beta=\exists x(\alpha\vee\beta) $$

So.. I need to find a Prenex Normal Form of:

$\alpha:=\forall[\exists y(P(y)\wedge Q(x,y))]\vee\forall y[\forall zQ(y,f(z))\rightarrow P(y)] $ with as few quantifiers as possible and I have:

$$ \alpha:=\forall[\exists y(P(y)\wedge Q(x,y))]\vee\forall y[\forall zQ(y,f(z))\rightarrow P(y)] $$

$$ \alpha\equiv\forall x\exists y(P(y)\wedge Q(x,y))\vee\forall y( \text ¬\forall zQ(y,f(z))\vee P(y)) $$

$$ \alpha\equiv\forall x\exists y(P(y)\wedge Q(x,y))\vee\forall y( \exists zQ(y,f(z))\vee P(y)) $$

$$ \alpha\equiv\forall x\exists y(P(y)\wedge Q(x,y))\vee\forall y\exists z( Q(y,f(z))\vee P(y)) $$

but I'm not sure if I can say that:

$$ \alpha\equiv\forall x\forall y\exists z[(P(z)\wedge Q(x,z))\vee( Q(y,f(z))\vee P(y))] $$

or something like that in order to remove a quantifier...

Any idea (?) thank you so much!

Answer 1

You already have this much

$$\forall \langle x,~ \exists \langle y,~ Py \land Qxy\rangle \rangle \lor \forall \langle y,~ \forall \langle z,~ Qy(fz)\rangle \implies Py\rangle $$

$$\forall \langle x,~ \exists \langle y,~ Py \land Qxy\rangle \rangle \lor \forall \langle y,~ \lnot \forall \langle z,~ Qy(fz)\rangle \lor Py\rangle $$

$$\forall \langle x,~ \exists \langle y,~ Py \land Qxy\rangle \rangle \lor \forall \langle y,~ \exists \langle z,~ \lnot Qy(fz)\rangle \lor Py\rangle $$

$$\forall \langle x,~ \exists \langle y,~ Py \land Qxy\rangle \rangle \lor \forall \langle y,~ \exists \langle z,~ \lnot Qy(fz) \lor Py\rangle \rangle $$

Recommanded next step is

$$\forall \langle x,~ \exists \langle y,~ Py \land Qxy\rangle \lor \forall \langle y,~ \exists \langle z,~ \lnot Qy(fz) \lor Py\rangle \rangle \rangle $$

$$\forall \langle x,~ \exists \langle y,~ Py \land Qxy\rangle \lor \forall \langle w,~ \exists \langle z,~ \lnot Qw(fz) \lor Pw\rangle \rangle \rangle $$

$$\forall \langle x,~ \forall \langle w,~ \exists \langle y,~ Py \land Qxy\rangle \lor \exists \langle z,~ \lnot Qw(fz) \lor Pw\rangle \rangle \rangle $$

Now the $y$ and $z$ can be combined into something like $s$:

$$\forall \langle x,~ \forall \langle w,~ \exists \langle s,~ (Ps \land Qxs) \lor (\lnot Qw(fs) \lor Pw)\rangle \rangle \rangle $$