# How to generate Skolem function in practice

Context: Skolemization is the process of removing the existential quantifiers in a first-order formula. The existential bounded variables are replaced with existential quantified function.

Questions: How, in practice, are these functions generated by an algorithm? Do we have another choice than a brute force strategy over all the possible functions? Is it of any practical use?

Example: Assume the formula $\forall{x}.\exists{y}.x \neq y$, then the Skolem form is $\exists{f}.\forall{x}.x \neq f(x)$ where $f$ is the function that explicits the dependency between $x$ and $y$. With resolution or any other method, how to, algorithmically, decide what is the result of $f(x)$? Is it all the values of the domain of discourse of $y$? If yes, does it mean that the role of the function is actually to "forbid" the value of $f(x)$ to change when a variable other than $x$ (if there was any) is instantiated?

Partial answer: As given below, we do not need to interpret the function $f$ to prove the validity. However, what about finding a model that satisfies the formula?

As I understood it...: Replying to myself to close this question. I guess there is no magic and we need to consider every function $f$ until we find a model. So if $f$ takes 2 arguments, it can maps to $|U| * |U|$ values ($|U|$ being the cardinality of the universe of discourse) and hence, the Skolem function is equivalent to the initial $\exists$ quantifier.

First of all there are two Skolem transformations, one replaces universal quantifiers and preserves validity, the other one replaces existential quantifiers and preserves satisfiability of the formula. Your question is about the second kind, so I will present it this way, but the other version is dual (and at least for me easier to understand).

Lemma: let $F$ be a formula and $sk(F)$ a Skolem transformation of $F$. Then if there exists a model $\mathcal{M}$ s.t. $\mathcal{M} \models F$ there exists a model $\mathcal{N}$ s.t. $\mathcal{N} \models sk(F)$.

If we can show that $sk(F)$ is unsatisfiable, it has no model. But then also $F$ can not have a model.

Now, Resolution is a quite efficient method to show that a formula (in conjunctive normal form) is unsatisfiable. This leads to the following approach to proving the validity of some formula $F$:

• Negate $F$
• Skolemize, transform the formula into conjunctive normal form
• Find a refutation for the CNF formula (a so called clause set)
• Because $\neg F$ does not have a model, all interpretations of $F$ must be a model - in other words: $F$ is valid.

Nowhere in this procedure do you need the actual interpretation of a Skolem function, you just rely on the fact that one must exist as part of the model $\mathcal{N}$.

• I understand your argument but I think my question was imprecise so I added an example and additional questions. Thanks. – Pierre T. Jun 27 '17 at 13:21
• Actually, I know understand we do not need the interpretation of the Skolem function to prove the validity of the formula. I realized my question is: how to generate Skolem function when looking for a model that satisfies the formula. – Pierre T. Jun 28 '17 at 5:40
• Sorry, it takes me a little time to get everything together. It's clear that Skolemization can be seen as some instance of the axiom of functional choice, so I expect it to be non-constructive. I have some remark in mind that for first order logic, something weaker suffices, but I believe this is non-constructive too. There are also approaches to algorithm extraction from (intuitionistic) proofs (via A-Translation or Gödel's Dialectica interpretation), where i will double check if you get an implementation for the skolem function (actually it's eigenvariables) or just don't need them at all. – lambda.xy.x Jun 28 '17 at 8:21
• Thank you for your answer! However, I think I do not have the background to fully understand your comment. Nevertheless, if we want to find a model that satisfies the formula, we are somehow forced to interpret the function $f$, right? So we can attribute a value to $y$. – Pierre T. Jun 29 '17 at 2:37