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

Question

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?

Answer 1

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

Answer 2

We can understand Marker's proof of the theorem through the spirit of lemma 2.3.6; namely, that we want to add witnesses to existential statements into the universe of $\mathcal{N}$. We do not need to expand the language and construct a Skolemization.

Formally, let $X_0 = X \cup \{c^{\mathcal{M}} \in M : c \in \mathcal{C}\}$. Given $X_i$, let $$X_{i+1} = X_i \cup \{m \in M : \text{if } \bar{x} \in X_i^n \text{ and } \mathcal{M} \models \exists v \, . \, \varphi(v, \bar{x}), \, m \text{ is a witness to } \exists v \, . \, \varphi(v, \bar{x})\}.$$ Note that we can use a choice function to pick only one $m$ per sentence, getting us the required cardinality. Let $N = \bigcup X_i$.

We want to ensure $\mathcal{N}$ is a substructure of $\mathcal{M}$.

1. Suppose $f$ is an n-ary function symbol of $\mathcal{L}$ and $\bar{x} \in N^n$. Then $\bar{x} \in X_i^n$ for some $i$, and so we have a witness $y \in X_{i+1}$ for the sentence $\exists v \, . \, v = f(\bar{x})$. Letting $f^{\mathcal{N}}(\bar{x}) = y$, we have $f^{\mathcal{N}} : N^n \to N$.

2. Suppose $R$ is an n-ary relation symbol of $\mathcal{L}$. Let $R^{\mathcal{N}} = R^{\mathcal{M}} \cap N^n$.

3. Suppose $c$ is a constant symbol of $\mathcal{L}$. By construction, $c^{\mathcal{M}} \in N$. So let $c^{\mathcal N} = c^{\mathcal M}$.

It is easy to verify that $\mathcal{N}$ is a substructure of $\mathcal{M}$. By Tarski-Vaught, $\mathcal{N} \prec \mathcal{M}$.

This proof is inspired by helpful conversations with @spaceisdarkgreen and by Corollary 2.1.3 in [1], which follows a similar approach.

[1] Tent, Katrin; Ziegler, Martin, A course in model theory, Lecture Notes in Logic 40. Cambridge: Cambridge University Press; Ithaca, NY: Association of Symbolic Logic (ASL) (ISBN 978-0-521-76324-0/hbk). x, 248 p. (2012). ZBL1245.03002.