“Standardizing variables” in the procedure of converting First Order Logic to CNF?

Question

In below question of converting the given formula into clause normal form, I stuck in the step “Standardizing variables”.Can someone explain to me whether my steps are correct and how to do “Standardizing variables” part in below formula? Also the other steps until obtaining clause normal form?

Here, q, p are predicate symbols. The square brackets were used to improve readability.They have the same meaning as round brackets.

∀x:([¬∃y:q(x,y)]∧[∃x∀y:(p(x,y)→p(y,y))])

step 1: remove →

∀x:([¬∃y:q(x,y)]∧[¬∃x∀y:(p(x,y)∨p(y,y))])

step 2: move ¬ inwards

∀x:([¬∃y:q(x,y)]∧[∀x∃y:(¬p(x,y)∧¬p(y,y))])

step 3: Standardizing variables

I stuck in here. Can someone explain me from this step? It would be really helpful.

Answer 1

It is simply replacing variables with other variables so that you never have two quantifiers in the same sentence quantifying the same variable.

IN your sentence you have two quantifiers that quantify a $x$ and two quantifiers that quantify a $y$, so you want to replace one of the $x$ variables with a different variable, for example a $v$, and one of the $y$ variables with a different variable yet, say a $w$.

Notice that you can do this as your very first step, and personally that is what I typically do, since having unique variables play unique roles in the sentences prevents getting confused about which variable is quantifed by which quantifier.