I am trying to derive the Skolem normal form of
$∀x[P(x) \land ∀y ∃x( \neg (Q(x,y)) → ∀zR(a,x,y))]$
$\rightsquigarrow ∀x[P(x) \land ∀y ∃x( Q(x,y) \lor ∀zR(a,x,y) )]$
And when it was solved in the class, they changed x to t, so it became
$∀x[P(x) \land ∀y ∃t( Q(t,y) \lor R(a,t,y) )]$
I understand that the variable $z$ does not matter to the predicate $R$. But I do not know the reason of changing the variable $x$ to $t$. Could somebody tell why it should happen?
In order not to accidentally identify two variables which are supposed to be different.
As long as variables are bound by quantifiers, their meaning is clear: In $∀x(P(x) \land ∀y ∃x(\neg(Q(x,y)) → ∀zR(a,x,y)))$, the inner quantifier $\exists x$ will "overwrite" the binding of the outer quantifier $\forall x$, and it is clear that the occurence of $x$ in $P(x)$ belongs to $\forall x$ while the two occurrences of $x$ in the second part of the formula belong to $\exists x$. Hence, the $x$ in $P(x)$ and the two in the second part of the formula are effectively two different variables that will be evaluated under different assignment functions.
But the goal of Skolemization is to eliminate quantifiers, so if we leave the two variables as they are and move the quantifiers away, then it is no longer visible that the $x$ in $P(x)$ and the ones in $Q(x,y) ... R(a,x,y)$ once were bound by different quantifiers, and it will look as if they were the same variable and supposed to be interpreted by the same assignment, which does not capture the original meaning of the formula correctly.
Therefore, we have to rename one of the variables to a different variable name. In the case of bound variables, this is an unproblematic procedure: The name of bound variables doesn't matter as long all variables which are supposed to be the same carry the same name, so we choose to rename the $x$'s that are bound by $\exists x$ to (for example) $t$. That way, we made sure that we can tell the the variables belonging to $\forall x$ and those belong to $\exists x$ (now $\exists t$) apart apart even after the quantifiers have been eliminated.