# Problem with transforming a formula to Prenex CNF

I've been trying to transform the following formula all day long with no avail:

$\lnot[\forall x \exists y F(u,x,y) \to \exists x (\lnot \forall y G(y,v) \to H(x))]$

the answer sheet gives us the solution but not the steps, here it is:

∀x∃y∃z[F(u, x, y) ∧ ¬G(z, v) ∧ ¬H(x))]

I can't seem to find a way to properly reach that conclusion. I'll transcribe one of my tries in painstaking detail and I'd be immensely grateful if someone could point out where I made a mistake:

1) $\lnot[\forall x \exists y F(u,x,y) \to \exists x (\lnot \forall y G(y,v) \to H(x))]$

2) $\lnot[\lnot \forall x \exists y F(u,x,y) \lor \exists x (\lnot \forall y G(y,v) \to H(x))]$

3) $\lnot[\exists x \forall y \lnot F(u,x,y) \lor \exists x (\lnot \forall y G(y,v) \to H(x))]$

4) $\lnot[\exists x \forall y \lnot F(u,x,y) \lor \exists x (\lnot \lnot \forall y G(y,v) \lor H(x))]$

5) $\lnot[\exists x \forall y \lnot F(u,x,y) \lor \exists x (\forall y G(y,v) \lor H(x))]$

6) $\lnot\exists x \forall y \lnot F(u,x,y) \land \lnot \exists x (\forall y G(y,v) \lor H(x))$

7) $\forall x \exists y F(u,x,y) \land \lnot \exists x (\forall y G(y,v) \lor H(x))$

8) $\forall x \exists y F(u,x,y) \land \forall x \lnot (\forall y G(y,v) \lor H(x))$

9) $\forall x \exists y F(u,x,y) \land \forall x \lnot \forall y G(y,v) \land H(x))$

10) $\forall x \exists y F(u,x,y) \land \forall x \exists y G(y,v) \land H(x))$

After this I simply gave up because I saw that no matter how I distributed the quantifier I wouldn't be able to reach the provided answer.

You should have the following.   Check for where you dropped negation (9-10).

1. $(\forall x~\exists y~F(u,x,y)) \land (\forall x~((\exists y~\lnot G(y,v)) \land \lnot H(x)))$

Now the universal distributes over conjunction: $(\forall a~\phi)\land(\forall a~\psi)\iff (\forall a~(\phi\land \psi))$

1. $\phantom{\forall x~(\exists y~F(u,x,y) \land ((\exists y~\lnot G(y,v)) \land \lnot H(x)))}$

However Existential does not; therefore we must use alpha substitution in one of the two existentials.   Substituting in the second will lead to the target.

1. $\phantom{\forall x~(\exists y~F(u,x,y) \land ((\exists z~\lnot G(z,v)) \land \lnot H(x)))}$

You can there by use that $\psi\land(\exists a~\phi)\equiv \exists a~(\psi\land\phi)$ if $a$ is not free in $\psi$ (and the universe is not-empty).

1. ${\forall x~\exists y~\exists z~(F(u,x,y) \land \lnot~G(z,v) \land \lnot H(x))}$
• Oh, thank you very much. The negation error from 8 onwards was actually a typo. I guess my real problem was that I couldn't see why I shouldn't rename the x in the second $\forall x$. May 24 '18 at 1:27
• You don't rename the $x$, you rename the $y$. May 24 '18 at 2:11