What does it mean when $x$ is 'free'? In the context of first-order logic and resolution (I'm trying to study Skolemization for a midterm tomorrow), I am seeing several references to $x$ being free or not free. What does this mean?

To pull all quantifiers in front of the formula and thus transform it into a prenex form, use the following equivalences, where $x$ is not free in Q:


Edit:
$$\forall xP(x) ∧ \exists xQ(x) \equiv \forall x(P(x) ∧ \exists xQ(x)) ≡ \forall x(P(x) ∧ \exists yQ(y)) \equiv \forall x\exists y(P(x) ∧ Q(y)).$$
If the second $x$ is bound by the existential quantifier - why can it be pulled into prenex form if the blurb above says that this can be done only if $x$ is not free? Or am I misunderstanding something?
Edit 2:
OK, i'm clearly not all here at the moment. Ignore that question
 A: A variable $x_1$ in a formula $\phi(x_1,x_2,\cdots, x_n)$ is called bound if $x_1$ is contained in some sub-formula of the form $\forall x_1 (\psi(x_1,\cdots))$. If ia variable is not bound, it is free. That is, a variable is free if it is not being quantified over, so that it is "free" to assume different values. On the other hand, if a variable is being quantified over, it is almost like a placeholder -- it doesn't make sense to try and input different values for that variable.

With regards to your second question, since $x$ is bound it is not free.
A: $x$ is free in $Q$ if it is not quantified over. 
So in the $L_{Ring}$ formula $x = 1$, $x$ is free. 
But in the $L_{Ring}$ formula $\forall x (x = 1)$, $x$ is not free (in which case we call $x$ bound)
A: 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.
