How to find the Skolem form of the following formula? I'm confused about finding a Skolem form of the following formula:
F = $(\forall x)(P(x)\rightarrow(\forall y)((\forall z)Q(z,y)\rightarrow\neg(\forall z)R(y,z)))$
So following the algorithm I've done these transformations:
F = $(\forall x)(\neg P(x)\vee(\forall y)((\exists z)\neg Q(z,y)\vee(\exists z)\neg R(y,z)))$
= $(\forall x)(\neg P(x)\vee(\forall y)((\exists z)\neg Q(z,y)\vee(\exists m)\neg R(y,m)))$
= $(\forall x)(\forall y)(\neg P(x)\vee(\neg Q(f(x,y),y)\vee\neg R(y,g(x,y))))$
= $\neg P(x)\vee(\neg Q(f(x,y),y)\vee\neg R(y,g(x,y)))$
But the solution on the textbook gives a different answer which is:
F = $(\forall x)(\forall y)(\forall z)(\forall v)(\neg P(x)\vee\neg Q(z,y)\vee\neg R(y,v)))$
= $\neg P(x)\vee\neg Q(z,y) \vee \neg R(y,v)$
I can't quite understand. What's wrong with my own solution? And why here the $z$ is replaced with a constant instead of a function like $g(x,y)$ or $f(x,y)$ ?
 A: Your solution is correct, the book's solution got wrong at the first step:
\begin{align}
F=&\forall x\forall y\exists z\exists v(\lnot P(x)\lor(\lnot Q(z,y)\lor\lnot R(y,v)))\\
\neq&\forall x\forall y\forall z\forall v(\lnot P(x)\lor(\lnot Q(z,y)\lor\lnot R(y,v)))
\end{align}
Clearly, these two prenex normal forms are not equivalent.
A: I verified Manx's previous result and it's correct. According to the implication rule during prenex normal form conversion here, from your first sentence F:
F = $\forall x \forall y [P(x) \rightarrow (\forall z Q(z,y) \rightarrow \neg \forall v R(y,v))]$
F = $\forall x \forall y [P(x) \rightarrow (\neg \forall z Q(z,y) \lor \neg \forall v R(y,v))]$
F = $\forall x \forall y [P(x) \rightarrow (\neg (\forall z Q(z,y) \land \forall v R(y,v)))]$
F = $\forall x \forall y [P(x) \rightarrow (\neg \forall z \forall v (Q(z,y) \land R(y,v)))]$
F = $\forall x \forall y [\neg P(x) \lor (\neg \forall z \forall v (Q(z,y) \land R(y,v)))]$
F = $\forall x \forall y [\neg P(x) \lor \exists z \exists v \neg (Q(z,y) \land R(y,v))]$
F = $\forall x \forall y \exists z \exists v [\neg P(x) \lor \neg (Q(z,y) \land R(y,v))]$
F = $\forall x \forall y \exists z \exists v [\neg P(x) \lor (\neg Q(z,y) \lor \neg R(y,v))]$
