In putting a formula into prenex form, it is the second move, so to speak, where the variable has to be free in the rest of the formula. For example $ (\forall x)[\phi(x)] \land (\exists x)[\psi(x)] $ is equivalent to $ (\forall x)[\phi(x) \land (\exists x)\psi(x)] $ because the $x$ in $\psi$ is still not affected by the universal quantifier. But that formula is not equivalent to $ (\forall x)(\exists x)[\phi(x) \land \psi(x)] $ nor to $ (\exists x)(\forall x)[\phi(x) \land \psi(x)] $ because in each of these both the $x$ in $\phi(x)$ and the $x$ in $\psi(x)$ are controlled by the same quantifier, even though they were not in the original.
The solution is easy: first rename all the quantified variables to they are all distinct, and then there will never be a conflict between different quantifiers when you pull them out front. There's nothing deep about it.
It is actually surprisingly tricky to give a correct definition of free and bound variables. The key is that it is not a variable itself that is "free" or "bound". The more fundamental thing is a specific instance of a variable (that is, a combination of a variable and its location within the formula) being a bound instance or a free instance. This is because, for example, $ [x = x] \land (\exists x)[x = x] $ has both free instances of $x$ and bound instances of $x$, as in the example above.
The definition of free and bound instances is inductive:
- If $\phi$ has no quantifiers, every instance of every variable in $\phi$ is free
- For a formula $\lnot \phi$, every instance of a variable corresponds to an instance of the same variable in $\phi$. The instance in $\lnot \phi$ is free if it was free in $\phi$ and bound if it was bound in $\phi$.
- For formula $\phi \lor \psi$, every instance of a variable corresponds either to an instance of the same variable in $\phi$ or an instance of the same variable in $\psi$. The instance in the compound formula is free if and only if the corresponding instance in the subformula is free, and bound if and only if the corresponding instance in the subformula is bound.
- The clauses for $\land$ and $\to$ are parallel to the clause for $\lor$.
- Every instance of $x$ in $(\forall x)\phi$ and $(\exists x)\phi$ is bound. Any other instance of a variable in $(\forall x)\phi$ or $(\exists x)\phi$ corresponds to an instance in $\phi$, and the instance in the quantified formula is free if and only if the instance in the subformula was free, and bound if and only if the instance in the subformula was bound.
Given that definition, we say that a variable is "occurs freely in the formula $\phi$" if there is at least one instance of $x$ in $\phi$ that is a free instance.