Is it right to render the quantifier of existence through a disjunction during skolemization

Question

I am to solve a problem:

$\forall x \exists y \neg P(x,y) \rightarrow \exists x \forall y Q(x,y)$

I'm getting rid of implication:

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

And now I'm using this formula: $\exists x A(x) \lor \exists B(x)$ = $\exists x( A(x) \lor B(x))$

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

Then I resolve variable conflicts: y->t

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

And moving all quantifiers to the very begining

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

The existence quantifier should be changed to the constanta: x->c

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

And then eliminating the $\forall$ quantifiers

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

Am I right at my solution? Can anybody please check the answer?

Answer 1

Yes. Each step is well reasoned and checks out okay.