Is it right to change variables at this situation during skolemization?

Question

I am to solve this problem:

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

I'm getting rid of implication:

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

Am I right that we have to resolve varialbe conflict this way: x->t and y->k

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

Then I'm moving all quantifiers to the front

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

Now getting rid of exists-quantifiers x=f1(y) and k=f2(y,t). I'm a bit confused to change new variable k to the function.

$ \forall y \forall t (P(f1(y),y) \lor Q(t,f2(y,t))) $

Am I right at my solution?

Answer 1

If your question is whether it's legitimate to change a recently renamed variable for an existential quantifier into a function symbol - sure, there's nothing wrong about that; there is no difference in whether the variable name has been changed at some point or not; the elimination of $\exists$ is independent of that step.