Skolemization in Marker’s Proof of Theorem 2.3.7 (Downward Löwenheim-Skolem)

model-theory

For convenience, I'll re-state Lemma 2.3.6 and Theorem 2.3.7 in Marker's Model Theory:

$\textbf{Lemma 2.3.6}$: Let $T$ be an $\mathcal{L}$-theory. There are $\mathcal{L}^\ast \supseteq \mathcal{L}$ and $T^\ast \supseteq T$ an $\mathcal{L}^\ast$ theory such that $T^\ast$ has built-in Skolem functions, and if $\mathcal{M} \models T$, then we can expand $\mathcal{M}$ to $\mathcal{M}^\ast \models T^\ast$. We can choose $\mathcal{L}^\ast$ such that $\vert \mathcal{L}^\ast \vert = \vert \mathcal{L} \vert + \aleph_0$. We call $T^\ast$ a skolemization of $T$.

$\textbf{Theorem 2.3.7 (L}\overset{..}{\textbf{o}}\textbf{wenheim-Skolem Theorem)}$: Suppose that $\mathcal{M}$ is an $\mathcal{L}$-structure and $X \subseteq M$, there is an elementary submodel $\mathcal{N}$ of $\mathcal{M}$ such that $X \subseteq N$ and $\vert \mathcal{N} \vert \le \vert X \vert + \vert \mathcal{L} \vert + \aleph_0$.

Now for the question:

The proof of Theorem 2.3.7 starts by stating that "by Lemma 2.3.6, we may assume that Th($\mathcal{M}$) has built-in Skolem functions." But can we guarantee this? Th($\mathcal{M}$) is an $\mathcal{L}$-theory (as $\mathcal{M}$ is an $\mathcal{L}$-structure), so we have no way of guaranteeing that it has built-in Skolem functions; it's entirely possible we have to include more function symbols in our language. Perhaps this is what Marker meant: we extend Th($\mathcal{M}$) to its skolemization via Lemma 2.3.6, obtaining a new theory with an expanded language of size $\vert \mathcal{L} \vert + \aleph_0$. This is consistent with the size claim at the end of Theorem 2.3.7.

Does this construction work, or does Th($\mathcal{M}$) already have built-in Skolem functions?

Best Answer

  1. Yes, the idea is that we Skolemize the theory, expand a model to a model of the Skolemized theory, produce an elementary submodel as a Skolem hull, and then show that the reduct to the original language is an elementary submodel of the original model satisfying the desired properties.
  2. I think it's better/more natural to include nullary functions (or equivalently constant symbols) as witnesses to formulas with no additional variables. But I don't know that it presents a real issue because you get them for free, essentially, when the dependence of a formula on the other variables is trivial. (Edit: I think this actually doesn't quite patch up the problem when we're taking the Skolem hull of the empty set, though to prove the theorem for $X=\emptyset$ we can just start with an arbitrary singleton rather than the empty set in that case and be fine.)
Related Question