First Order Logic: Skolemization and Free Variables? Bound/Free Variable assignment. I have a couple of questions about the role of the free variables.
The first one is more specific:
1) So a formula to be in a Skolem Normal Form it has to be:
a) In Prenex Normal Form
b) Not to have any ∃ quantifiers.
c) Not to have any free variables
Okay, I know how to achieve a) and b), but I couldn't find information anywhere on how to achieve c)?
2) I am trying to grasp my mind around the idea of the difference between free variables and bound variables. I know the difference mechanically, I know the rules, I understand how to work with them, but I still cannot completely understand the difference in terms of intuition. I will share some questions that will help me understand:
a) If we have the formula: p(x)&∃q(x). The first occurrence of x is free, the second is bound.


*

*What is different between the two sub formulas in terms of x? My idea is that:


*

*In both sub formulas if there is no x in the Domain to satisfy the
formula it is false. 

*If there is at least one x to satisfy both sub formulas: then P(x) is feasible (I am not sure if that   is the correct term) and q(x) is true.

*If both subformulas are satisfied for all x then both are true.



Is that the difference? That if there is at least one x (but not all) that satisfies the formula if we have existence quantifier then the formula is true but if we don't have - it is feasible?
b) What happens when we make a Variable assignment? 


*

*Does the bounded x get an assignment?    

*Do both x's get assignment?


Thank you in advance!
 A: 
What is the difference between free variables and bound variables.

Consider : $p(x) \land ∃xq(x)$ [typo corrected]. 
The first thing to note is that the quantified variable can be renamed without changing the "meaning" : $p(x) \land ∃yq(y)$.
Now, the issue regarding the difference between the two sub formulas in terms of $x$ has been removed.
As you say, in order to evaluate the truth-value of the formula in a domain $\mathfrak A$ you have to consider an assignment function : $s : \text {Var} \to \mathfrak A$.
Assume that there is $a \in \mathfrak A$ such that $q(a)$ holds. What about the satisfiability of the formula ? It depends on $s$ : if $s(x)=b$ and $p(x)$ holds for $b$, than the complete formula is satisfied by $s$ in $\mathfrak A$ :

$\mathfrak A \vDash (p(x) \land ∃yq(y))[s]$.

Now, consider the part $∃yq(y)$: we have that it is satified in $\mathfrak A$ by $s$ if there is an object $c \in \mathfrak A$ and an assignment $s'=s(y|c)$ which is exactly like $s$ except for one thing: at the variable $y$ it assignes the value $c$, such that $q(y)$ holds for $d$.
In conclusion, for $b, c \in \mathfrak A$: if $s(x)=b$ and $s'=s(y|c)$ and $p(x)$ holds for $b$ and $q(y)$ holds for $c$, we have that :

$\mathfrak A \vDash (p(x) \land ∃yq(y))[s]$,

i.e. the formula $p(x) \land ∃yq(y)$ is satisfied by $s$ in $\mathfrak A$.

The formal specification seems convoluted, but it is very easy to manufacture an example.
Consider the domain $\mathbb N$ of natural numbers and consider $(x = 0)$ as $p(x)$ and $(y > 0)$ as $q(y)$.
Consider the function $s$ such that : $s(x)=0$ and check whether :

$\mathbb N \vDash ((x = 0) \land ∃y(y > 0))[s]$.

