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 LeinsterCommented Nov 21, 2012 at 19:14
-
1$\begingroup$ I'm asking, because Skolemization basically means removing existential quantifiers, but why?? $\endgroup$– Mohammad Noorani BakerallyCommented Nov 21, 2012 at 19:48
-
3$\begingroup$ Some discussion here might be useful: mathoverflow.net/questions/90324/… $\endgroup$– SuvritCommented Nov 21, 2012 at 20:12
-
1$\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 1920-30 period is not well established even yet and all the applications of Cantor's ideas to these formulas are on shaky ground. $\endgroup$– Michael McGradyCommented Jun 6, 2014 at 17:45
-
3$\begingroup$ @MichaelMcGrady I don't really understand what your comment has to do with Skolemization. Could you elaborate? $\endgroup$– Noah SchweberCommented Jun 6, 2014 at 19:09
4 Answers
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.
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.
-
2$\begingroup$ The ization of names should be banned! $\endgroup$ Commented Nov 21, 2012 at 20:59
-
35$\begingroup$ @Mariano: Can we call the practice of rebranding those processes Suárez-Alvarezization? $\endgroup$ Commented Nov 21, 2012 at 21:33
-
1$\begingroup$ Lets do it and call this process "Self-reference-Alvarez-Wolskelization". $\endgroup$– PushpaCommented Jun 7, 2017 at 4:09
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.
-
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 first-order 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 Dialectica-style interpretation (though I confess that no exact correspondence to Dialectica is clear to me at the moment). $\endgroup$ Commented Nov 22, 2012 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$ Commented Nov 22, 2012 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$ Commented Nov 23, 2012 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$ Commented Nov 23, 2012 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 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!
-
$\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$ Commented Jun 6, 2014 at 18:29