Am I right at my skolemization?

Question

I am to skolemize the problem below: $$\forall x \exists y \neg(P(x,y))\rightarrow \exists z \forall x Q(x,z)$$ $$\exists x \forall y P(x,y) \lor \exists z \forall x Q(x,z)$$ Then I am resolving variable conflict: x->t $$\exists x \forall y P(x,y) \lor \exists z \forall t Q(t,z)$$ $$\exists x \forall y \exists z \forall t(P(x,y)\lor Q(t,z))$$ Then I'm changing the $\exists x$ to a constant c $$\forall y \exists z \forall t(P(c,y)\lor Q(t,z))$$ Then I am to create a function: z=f(y) $$\forall y \forall t(P(c,y)\lor Q(t,f(y)))$$ Then eliminating quantifiers: $$P(c,y)\lor Q(t,f(y))$$ Am I right?

Answer 1

Correct, though you can avoid creating that function by first pulling out the existentials, and then the universals.

That is, from

$$\exists x \forall y P(x,y) \lor \exists z \forall t Q(t,z)$$

you can first pull out the $\exists x$:

$$\exists x (\forall y P(x,y) \lor \exists z \forall t Q(t,z))$$

then the $\exists z$:

$$\exists x \exists z (\forall y P(x,y) \lor \forall t Q(t,z))$$

and then the $\forall y$ and $\forall t$:

$$\exists x \exists z \forall y \forall t ( P(x,y) \lor Q(t,z))$$

now you just introduce a constant for each of the existentials:

$$\forall y \forall t (P(c,y) \lor Q(t,d))$$

and drop the universals:

$$P(c,y) \lor Q(t,d)$$