How to find the Skolem form of the following formula?

270 Views Asked by At

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)$ ?

2

There are 2 best solutions below

2
On

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.

0
On

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))]$