why Skolemization? Can someone explain what is the reason for using Skolemization, I clearly understand that its the removal of existencial quantifiers, but whats the use? why is keeping existencial quantifiers not good??
 A: Skolemization, and its dual Herbrandization, can be useful in changing a statement with many quantifiers into a statement with one (non-bounded) existential quantifier.  This provides a uniform witness for some property.
Metastability
Here is an important example, called metastability.  The following says that a sequence of reals $(x_n)$ is Cauchy.

$\forall \varepsilon>0.\ \exists m\in\mathbb{N}.\ \forall n\geq m.\ \left|x_n - x_m\right| < \varepsilon $

Now, first we do the following trivial looking manipulation. (Note, $[m,n']:=\{m,\ldots,n'\}$.)

$\forall \varepsilon>0.\ \exists m\in\mathbb{N}.\ \color{blue}{\forall n'\in\mathbb{N}.\ \forall n\in [m,n'].}\ \left|x_n - x_m\right| < \varepsilon $

Herbrandize the $n'$ into a function $F(m)$.

$\forall \varepsilon>0.\ \color{blue}{\forall F\colon \mathbb{N}\rightarrow\mathbb{N}.}\ \exists m\in\mathbb{N}.\ \forall n\in [m,\color{blue}{F(m)}].\ \left|x_n - x_m\right| < \varepsilon $

Do a similar trivial manipulation.

$\forall \varepsilon>0.\ \forall F\colon \mathbb{N}\rightarrow\mathbb{N}.\ \color{blue}{\exists m'\in\mathbb{N}.\ \exists m\leq m'.}\ \forall n\in [m,F(m)].\ \left|x_n - x_m\right| < \varepsilon $

Skolemize the $m'$ into a functional $M(\varepsilon,F)$.

$\color{blue}{\exists M\colon \mathbb{Q}\times\mathbb{N}^\mathbb{N}\rightarrow\mathbb{N}.}\ \forall \varepsilon>0.\ \forall F\colon \mathbb{N}\rightarrow\mathbb{N}.\ \exists m\leq \color{blue}{M(\varepsilon,F)}.\ \forall n\in [m,F(m)].\ \left|x_n - x_m\right| < \varepsilon $

This formulation is called metastability.  This witness $M$ looks quite complicated, and in some sense it is.  But $M$ has some advantages.  Unlike a rate of convergence, $M$ is quite uniform.  For example any increasing sequence $(x_n)$ in between 0 and 1 has a metastable bound of $M(\varepsilon,F) = F^{[1/\varepsilon]}(0)$, i.e. the function $F$ iterated the floor of $1/\varepsilon$ times starting at $0$.
For this reason, metastability is useful in proving convergence, for example in Tao's proof of the convergence of multiple ergodic averages.  For more on metastability see this blog post.
A: Somewhat related to Jason Rute's answer: suppose you give me a formula, say $\varphi\equiv\forall x\exists y\theta(x, y)$ where $\theta$ is quantifier free. Skolemization gives me a way to think about the complexity of $\varphi$ being true: how complicated must a Skolem function for $\varphi$ be?
For example, consider the formula "For every $x$ there is a $y$ such that EITHER $\Phi_x(x)$ halts in exactly $y$ many stages, OR $y=0$ and $\Phi_x(x)$ never halts." This is clearly a true sentence; however, any Skolem function for it must be equivalent to the Halting problem. So the formula is not "recursively true." 
(Note that in the above example, our underlying structure is the natural numbers with $+$ and $\times$. In general, we either need to look at copies of a given structure with domain $\omega$, or adopt some other notion of effectiveness which treats a broader class of structures.)
There are now a bunch of interesting directions one can go with this! We could try to formalize the notion of "recursively true"; depending what aesthetic we bring to the table, this could lead to an intuitionistic logic, or to something like Reverse Mathematics. We could look at set of true $\Pi^0_2$ (or beyond) sentences of arithmetic, partially preordered by "every Skolem function for $\varphi_1$ computes a Skolem function for $\varphi_2$" (or other partial preorders with the sameish motivation, for example the 'degrees of provability' http://projecteuclid.org/download/pdfview_1/euclid.ndjfl/1352383227). We could focus on some particular sentence of interest, and try to understand the family of Skolem functions associated to it. We could move one type higher - to second-order statements like "For every set $X\subseteq\mathbb{N}$, there is a set $Y\subseteq\mathbb{N}$ such that if $X$ codes an infinite linear order then $Y$ codes an infinite ascending sequence or an infinite descending sequence in $X$" and look at the descriptive set-theoretic complexity of the associated higher-order Skolem functions. Or any number of other approaches I haven't thought of!

The bottom line for me: Skolemization lets us turn a statement which may be false or true into a statement which may be false or may be true with a certain complexity; and this makes things infinitely more fascinating, at least for me!
A: For example, Skolemizations (and the dual operation of Herbrandization) are used, proof-theoretically, when one wants "reductions" of first order logic to propositional logic. 


*

*In order to prove the consistency of a first order theory finitarily, one can consider, by Skolemization, a conservative open extension of the theory. If this extension is simple enough, then one can use Hilbert-Ackermann consistency theorem, which says that an open theory $T$ is inconsistent iff there is a disjunction of negations of instances of the axioms of $T$ that is a tautological consequence of axioms of equality. For example, consider Robinson Arithmetic $Q$. One Standard formulation of $Q$ is not open: it has an axiom saying that if $n$ is not zero then there exists a predecessor of $n$. The Skolemization of this axiom introduces the symbol of the predecessor function, and now we can replace the original axiom by an open one. Now, it is easy to define a (propositional) valuation, based on the usual algorithms for the arithmetic functions, and this shows that the condition in the Hilbert-Ackermann theorem cannot hold. Notice that, the Hilbert-Ackermann theorem itself is a reduction of first-order to propositional logic that was first proved (finitarily) by use of epsilon-operator, which is almost the same thing as Skolemization. 

*Herbrand Theorem: a more complete reduction of first-order logic to propositional logic. It says that a sentence in prenex normal form is a logical theorem iff there is a disjunction of instances of the matrix of the Herbrand normal form of the sentence (the midsequent) that is tautological consequence of instances of equality axioms. The (finitary) proof of this theorem can be done in two steps: first, prove the theorem for existential sentences in prenex normal form, and, after that, show that an arbitrary sentence is equivalent for validity to its Herbrandization. The technique of Skolemization is used throughout in this proof: the existential case is essentially Hilbert-Ackerman, and the Herbrandization is dual to Skolemization. 

*Any proof of the completeness theorem for first order logic must, at some point, deal with the validation of existential sentences (in the canonical structure). This proof can be done by Skolemization, through a reduction of the general case to the case in which the theory is open. In the case the theory is open, the proof of the completeness can be done more simply, because now you don't have to worry about the validity of existentials in the canonical structure. There is an (easy) exercise in Shoenfield's book dedicated to this proof. The proof uses only propositional concepts, such as "tautologically complete set of quantifier free sentences", and the construction of the canonical structure. This is another reduction of first order to propositional logic.

*Also, the reduction of first order to propositional logic can be useful in decidability problems. For example, the set of valid existential sentences that contains no function symbols (but may contain constants) is decidable. This can be proved finitarily, by use of Herbrand's theorem: it is decidable whether a quantifier free formula is tautological consequence of instances of equality axioms in a language without function symbols. In fact, if the quantifier free, function symbol free formula $\varphi$ is a tautological consequence of equality axioms $A_1$,..., $A_n$ then, identifying all variables and constants of $\varphi$ and $A_1$,..., $A_n$ with $x$, it follows that $\varphi*$ is a tautological consequence of equality axioms $A^*_1$,..., $A^*_n$, where  $\varphi*$ and $A^*_1$,..., $A^*_n$ are the resulting formulas with all terms identified with $x$. It is easy to see that all new equality axioms (the $A^*_i$) can be dropped, possibly with the exception of the equality axiom $x=x$. Now, it is decidable if $\varphi*$ is a tautological consequence of $x=x$. Furthermore, $\varphi*$ is an instance of $\varphi$, and hence we're done. The infinitary proof of this fact is based on the remark that $\varphi$ is valid iff it is valid in all finite models of a specific (finite) cardinality.
In general, the infinitary proofs of the finitary results mentioned above are easy. 
A: Removing existential quantifiers is called Skolemization because it was used by Skolem, probably in proving the Löwenheim-Skolem theorem.  Similarly, the dual process of removing universal quantifiers is sometimes called Herbrandization, because it's an ingredient in Herbrand's theorem.  Removing all quantifiers (by introducing new predicate symbols for all formulas) is sometimes called Morleyization; I'm not actually sure why, but I'll guess Morley used it (before a lot of other people).  Whether these transformations of formulas are good depends on what you want to do.  Generally, Skolemization is useful in considerations of satisfiability and Herbrandization is useful in the dual considerations of validity.
