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

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?

• @DerekElkins, you are right, they should be different – Elvin Aug 11 at 19:08
• Minor issue: $t$ and $k$ are unusual names to choose for variables - more conventional would be $x, y, z, u, v, w$ (in about that order of frequency). – lemontree Aug 12 at 13:40

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.