# Distinction between Built-in and Definable Skolem Functions

In A Course on Basic Model Theory ( Haimanti Sarbadhikari, Shashi Mohan Srivastava, pp. 27-28) and other textbooks, I have found the following distinction:

• A theory T has Built-in Skolem Functions iff $$T\models \forall x \exists y \varphi(x,y) \rightarrow \varphi (x,f(x))$$
• A theory T has Definable Skolem Functions iff
$$T \models ∀w∀u∀v ((ψ(w, u) ∧ ψ(w, v)) → u = v),$$
$$T \models ∀w (∃vφ(w, v) → ∃u (ψ(w, u) ∧ φ(w, u)).$$
Moreover, in this latter case we can introduce an anxiom such as: $$x=f_{\varphi }(w) \iff \psi (w,u)$$

1) Why we have this distinction?
2) It can be proved that every model has built-in Skolem functions, but not every model has definable Skolem functions. Is that correct? Why so?
3) If point (2) is correct, then having Built-in Skolem functions is enough to prove the equisatisfiability of a first-order formula and its Skolem Normal Form (SNF). Then I would say that, due to the fact that not every model has definable Skolem functions, we cannot prove the logical equivalence between a first-order formula and its SNF. Is this argument sound? Is so, why we need definable Skolem functions to prove the logical equivalence of a first-order formula and its SNF?

• In the first case $f$ is part of the language of $T$ : we have formula $\varphi (x,f(x))$. Commented Nov 21, 2019 at 16:15
• In the second case, having proved the two "functionality" theorems, we may enlarge the language of the adding the finction symbol $f_{\varphi}$ with the corresponding axiom. Commented Nov 21, 2019 at 16:16
• Thanks, I get it. Can you please say something more about question n.3? Namely: given that every model has built-in Skolem function, so we can prove the equisatisfiability of a first-order formula and it's Skolem Normal Form (SNF). Yet, given that not every model has a definable Skolem function, we cannot prove the logical equivalence of a first-order formula and it's SNF. Is this argument sound? Commented Nov 21, 2019 at 18:06
• I don’t know what you’re getting at with (2)... surely you don’t mean literally that every model has built-in Skolem functions? Can you say what you mean precisely and why you think it? Commented Nov 21, 2019 at 20:34

$$\newcommand{\L}{\mathcal{L}}$$First let me define better those 2 terms:

$$T_\L$$ is a Skolem theory(or, has built in Skolem functions, same thing) if:

For every $$n+1$$-ary formula $$φ$$, there exists in $$\L$$ an $$n$$-ary function symbol $$f$$ such that $$T\models \forall \overline x (\exists y \varphi(\overline x,y) \rightarrow \varphi (\overline x,f(\overline x)))$$

That is, the Skolem function is a symbol in the language.

$$T_\L$$ has definable Skolem functions if:

For every $$n+1$$-ary formula $$φ$$, there exists $$n+1$$-ary functional relation $$ψ$$ such that $$T\models \forall \overline x (\exists y \varphi(\overline x,y) \rightarrow ∀ z(\psi(\overline x,z)→\phi(\overline x,z)))$$.

Now for the questions:

1. We distinguish between the 2 because the fact that there exists a functional relation that behave like the above, does not implies that there exists such symbol $$f$$. Given that $$T_\L$$ is Skolem theory, we can simply define $$ψ(\overline x, z)=φ(\overline x,z)∧z=f(\overline x)$$, I believe you can check that this is indeed a functional relation that satisfy the definition of definable Skolem function. On the other hand, given $$ψ$$, we can't say anything about the existence of $$f$$

2. No, take any theory without any function symbols, and you get a theory that is not Skolem theory.

Now, that being said, it is correct that we can just add function symbol for each formula $$φ$$ and add the axioms $$x=f_{\varphi }(w) \iff \psi (w,u)$$. The new theory conservative extension to the old theory. If the new theory definable Skolem functions again, we can repeat this processes, doing this recursively and we get that the union of all of those is a conservative extension of the original theory and is a Skolem theory.