Henkinization vs Skolemization

Question

I am a novice in logic, and as I learn the basics of both constructions to, roughly speaking, witness quantifiers, one by constants (Henkin) and the other by Skolem functions, a couple of questions come to mind:

What significant distinctions exist between the two constructions? For example, are there situations when one is preferrable over the other?

Would you recommend a book which treats both?

Answer 1

I have some evidence that Skolemization is instrumentally useful in proving the downward Löwenheim-Skolem theorem and Henkinization is instrumentally useful in proving compactness.

I strongly suspect, though, that if you really wanted to, you could use Skolemization nontrivially as a preprocessing step to construct a equisatisfiable $\exists$-free version of a theory $T$ as part of a compactness proof. (A Skolemized theory is also Henkinized, so the original proof would go through without changes.)

The usefulness of Henkinization in a proof of Löwenheim-Skolem seems limited, though.

---

I don't know whether the usage of these constructions differ significantly, but I can give you references that define both.

Marker's Model Theory: An Introduction covers Henkinization on page 34 Definition 2.1.5

We say that an $L$-theory $T$ has the witness property if whenever $\phi(v)$ is an $L$-formula with one free variable $v$, there is a constant symbol $c \in L$ such that $T \models (\exists v \mathop. \phi(v)) \to \phi(c)$.

It goes on to use this definition in a proof of the compactness theorem.

Skolem functions and Skolemization are defined on pages 45 and page 46.

The definition is quite similar, a theory has builtin Skolem functions if and only if for all wffs $\varphi$ with at least one free variable there exists a function $f$ such that $ T \models \forall \vec{x} \mathop. (\exists v \mathop. \varphi(v, \vec{x})) \to \varphi(f(\vec{x}), \vec{x})$.

Skolem functions are then used in a proof of the Löwenheim-Skolem theorem.

As for other books, Hodges' A Shorter Model Theory uses Hintikka sets to prove compactness on page 125. I don't really understand the proof, it appears to use existential witnesses in some manner though (and certainly contains the word witness).

Skolemization appears on page 71 in that book and appears immediately before a proof of the downward Löwenheim-Skolem theorem.