Finding prenex normal form and skolemization of a formula

Question

Transform the following predicate logic formula into prenex normal form and Skolem form: $F = \neg(\exists y.\forall x.P(x,y)\rightarrow \forall x. \exists y.P(x,y))$

My attempt for the transformation into prenex normal form:

• $(\exists y.\forall x.P(x,y) \wedge \neg( \forall x. \exists y.P(x,y)))$
• $(\exists u.\forall z.P(z,u) \wedge \exists x. \exists y.\neg P(x,y))$
• $\exists u.\forall z.\exists x. \exists y.(P(z,u) \wedge \neg P(x,y))$

and the skolemization:

• $\forall z.(P(z,a) \wedge \neg P(b,c))$

Is this right?

Answer 1

Close! Just a few small mistakes:

First, $\neg( \forall x. \exists y.P(x,y)))$ is equivalent to $\exists x. \neg \exists y.( P(x,y)))$, and thus to $\exists x. \forall y.\neg( P(x,y)))$

So, you end up with:

$(\exists u.\forall z.P(z,u) \wedge \exists x. \forall y.\neg P(x,y))$

and thus:

$\exists u.\forall z.\exists x. \forall y.(P(z,u) \wedge \neg P(x,y))$

Second, whenever you are Skolemizing, you should pay attention to any existentials that come after any universals. Consider the following:

$\forall x.\exists y.S(y,x)$

where $S(y,x)$ means '$y$ is the successor of $x$'. Now, if this is about whole numbers, then it is clear that this is a true statement: For every number there is a successor. But also note that there is not one number that is the successor to all numbers. So, there is no constant $a$ such that

$\forall x.S(a,x)$

is true. So that is not what you want as the Skolemization of the statement. Instead, notice that the successor of a number $x$ depends on what the number $x$ is. Indeed, we can think of this as a function from $x$ to $y$. So, what we can say, is that there is some function $f$ such that

$\forall x.S(f(x),x)$

is true. And that is exactly what the correct Skolemization is (make sure that $f$ is a 'new' function, i.e. not a function symbol that is used anywhere else in your statement(s) under consideration)

So, the Skolemization of your original statement:

$\exists u.\forall z.\exists x. \exists y.(P(z,u) \wedge \neg P(x,y))$

should have been:

$\forall z.(P(z,a) \wedge \neg P(f(z),g(z)))$

And applied to the corrected:

$\exists u.\forall z.\exists x. \forall y.(P(z,u) \wedge \neg P(x,y))$

you get:

$\forall z. \forall y.(P(z,a) \wedge \neg P(f(u),y))$

One last thing. In this particular case, you can actually avoid the use of such a function. Let's go back to:

$(\exists u.\forall z.P(z,u) \wedge \exists x. \forall y.\neg P(x,y))$

Here, we can first take out the $\exists u$, then the $\exists x$, then the $\forall z$, and finally the $\forall y$, resulting in:

$\exists u.\exists x.\forall z. \forall y.(P(z,u) \wedge \neg P(x,y))$

And now, when you Skolemize, you simply get:

$\forall z. \forall y.(P(z,a) \wedge \neg P(b,y))$