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??

1$\begingroup$ Can you tell us where you've read or heard that keeping existential quantifiers is not good? $\endgroup$ – Tom Leinster Nov 21 '12 at 19:14

1$\begingroup$ I'm asking, because Skolemization basically means removing existential quantifiers, but why?? $\endgroup$ – Mohammad Noorani Bakerally Nov 21 '12 at 19:48

3$\begingroup$ Some discussion here might be useful: mathoverflow.net/questions/90324/… $\endgroup$ – Suvrit Nov 21 '12 at 20:12

$\begingroup$ Underlying the processes is a tension between truth preservation $A~\vdash~B$ and logical truth preservation $\models~A~\iff~\models~B$. I think the question is a good one and that we have not as yet plumbed the depths of what these mean. More work in this area is needed, even though the methodologies have a long track record of usefulness their meaning is yet to be examined. In my opinion, until this is examined thoroughly, the foundations of logic in the 192030 period is not well established even yet and all the applications of Cantor's ideas to these formulas are on shaky ground. $\endgroup$ – Michael McGrady Jun 6 '14 at 17:45

3$\begingroup$ @MichaelMcGrady I don't really understand what your comment has to do with Skolemization. Could you elaborate? $\endgroup$ – Noah Schweber Jun 6 '14 at 19:09
For example, Skolemizations (and the dual operation of Herbrandization) are used, prooftheoretically, 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 HilbertAckermann 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 HilbertAckermann theorem cannot hold. Notice that, the HilbertAckermann theorem itself is a reduction of firstorder to propositional logic that was first proved (finitarily) by use of epsilonoperator, which is almost the same thing as Skolemization.
Herbrand Theorem: a more complete reduction of firstorder 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 HilbertAckerman, 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.
Removing existential quantifiers is called Skolemization because it was used by Skolem, probably in proving the LöwenheimSkolem 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.

2$\begingroup$ The ization of names should be banned! $\endgroup$ – Mariano SuárezÁlvarez Nov 21 '12 at 20:59

29$\begingroup$ @Mariano: Can we call the practice of rebranding those processes SuárezAlvarezization? $\endgroup$ – Zack Wolske Nov 21 '12 at 21:33

$\begingroup$ Lets do it and call this process "SelfreferenceAlvarezWolskelization". $\endgroup$ – Pushpa Jun 7 '17 at 4:09
Skolemization, and its dual Herbrandization, can be useful in changing a statement with many quantifiers into a statement with one (nonbounded) 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.\ \leftx_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'].}\ \leftx_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)}].\ \leftx_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)].\ \leftx_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)].\ \leftx_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.

1$\begingroup$ I like this answer, but I'd point out that, by going to an object $M$ two types higher than the base domains, it's rather different from the usual Skolemizations (and Herbrandizations) that one uses in firstorder logic (where one goes up one type but then quickly removes the quantifiers over that higher type). In fact, this notion of metastability looks to me more like a Dialecticastyle interpretation (though I confess that no exact correspondence to Dialectica is clear to me at the moment). $\endgroup$ – Andreas Blass Nov 22 '12 at 3:43

$\begingroup$ Andreas, yes this is basically Gödel's Dialectica interpretation. (In my mind I think of it as Skolemization which made me think to put it here). Thanks for the clarification! $\endgroup$ – Jason Rute Nov 22 '12 at 17:18

$\begingroup$ I don't understand; you haven't gotten rid of all the inner existential quantifiers. Do you mean to just set $m = M(\varepsilon, F)$, rather than supposing that it is bounded by it? $\endgroup$ – Ryan Reich Nov 23 '12 at 6:20

$\begingroup$ Ryan, the main point is that the innermost existential and universal quantifiers are bounded. In theories powerful enough to encode arithmetic, bounded number quantifiers can be removed by encoding finite sets as numbers. This makes the statement an $\exists \forall$ statement. As for your second question, yes one can just get rid of the inner existential by taking $M(\varepsilon,F)$ to be the minimal $m$ that satisfies the property. But the value of just using a bound is that a bound can be much more uniform. Notice my example. This version is more useful in applications. $\endgroup$ – Jason Rute Nov 23 '12 at 14:06
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 secondorder 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 settheoretic complexity of the associated higherorder 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!

$\begingroup$ Admittedly, this may not be in the spirit of the OP: I'm addressing why Skolemization is useful from the point of view of creating new ideas, not solving existing problems, and that might not be as desired. $\endgroup$ – Noah Schweber Jun 6 '14 at 18:29