Distinction between Built-in and Definable Skolem Functions

Question

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)$

I have few questions about this distinction:
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?

Answer 1

$\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.