[proofplan] We show that $H$ satisfies the existential witness condition for all $L$-formulas with parameters from $H$. The Skolem axiom supplies a witness in $M$ by applying the appropriate Skolem function to the parameter tuple, and closure of $H$ under that function keeps the witness inside $H$. We then prove the corresponding elementary-substructure criterion by induction on formulas, using the witness condition exactly at the existential step. [/proofplan] [step:Verify that $H$ carries the induced $L$-substructure] Because $H$ is closed under every function symbol of $L^{\mathrm{Sk}}$, it is in particular closed under every function symbol of the sublanguage $L$. Since $H$ is nonempty, the induced interpretations of the function symbols, relation symbols, and constant symbols of $L$ make $H$ into an $L$-substructure of $M$. This is precisely the structure denoted by $N$. [/step] [step:Produce witnesses in $H$ for existential $L$-formulas realized in $M$] Let $\varphi(x,\bar{y})$ be an $L$-formula, let $\bar{a}\in H^{|\bar{y}|}$ be a tuple of parameters, and suppose \begin{align*} M \models \exists x\,\varphi(x,\bar{a}). \end{align*} Because $\varphi$ is an $L$-formula, the same formula is also an $L^{\mathrm{Sk}}$-formula. Since $M^{\mathrm{Sk}}\models T^{\mathrm{Sk}}$, the Skolem axiom for $\varphi$ gives \begin{align*} M^{\mathrm{Sk}} \models \varphi(f_\varphi(\bar{a}),\bar{a}). \end{align*} The formula $\varphi$ contains only symbols from $L$, so this is equivalently \begin{align*} M \models \varphi(f_\varphi(\bar{a}),\bar{a}). \end{align*} Since $H$ is closed under the $L^{\mathrm{Sk}}$-function symbol $f_\varphi$ and $\bar{a}\in H^{|\bar{y}|}$, we have $f_\varphi(\bar{a})\in H$. Thus every existential $L$-formula with parameters from $H$ that is realized in $M$ has a witness in $H$. [guided] Fix an $L$-formula $\varphi(x,\bar{y})$ and a parameter tuple $\bar{a}\in H^{|\bar{y}|}$. We assume that $M$ realizes the existential formula: \begin{align*} M \models \exists x\,\varphi(x,\bar{a}). \end{align*} The point of the Skolem expansion is that it has added a function symbol $f_\varphi$ whose value is required to choose a witness whenever such a witness exists. More precisely, $T^{\mathrm{Sk}}$ contains the axiom \begin{align*} \forall \bar{y}\,\bigl(\exists x\,\varphi(x,\bar{y}) \implies \varphi(f_\varphi(\bar{y}),\bar{y})\bigr). \end{align*} Since $M^{\mathrm{Sk}}\models T^{\mathrm{Sk}}$ and $M\models \exists x\,\varphi(x,\bar{a})$, applying this axiom at the tuple $\bar{a}$ gives \begin{align*} M^{\mathrm{Sk}} \models \varphi(f_\varphi(\bar{a}),\bar{a}). \end{align*} Now $\varphi$ is an $L$-formula, not a formula involving the added Skolem symbols. Therefore its truth value is the same in the $L^{\mathrm{Sk}}$-structure $M^{\mathrm{Sk}}$ and in its $L$-reduct $M$. Hence \begin{align*} M \models \varphi(f_\varphi(\bar{a}),\bar{a}). \end{align*} Finally, $H$ is closed under every function symbol of $L^{\mathrm{Sk}}$. Since $\bar{a}$ is a tuple from $H$, this closure condition gives \begin{align*} f_\varphi(\bar{a})\in H. \end{align*} Thus the existential formula has a witness lying inside $H$ itself. [/guided] [/step] [step:Prove elementarity from the existential witness property] We prove by induction on $L$-formulas $\psi(\bar{z})$ that for every tuple $\bar{b}\in H^{|\bar{z}|}$, \begin{align*} N \models \psi(\bar{b}) \iff M \models \psi(\bar{b}). \end{align*} For atomic formulas, the equivalence holds because $N$ is an induced $L$-substructure of $M$: function terms with parameters from $H$ have the same values in $N$ and $M$, and relation symbols are interpreted in $N$ by restriction from $M$. The Boolean connectives are preserved by the induction hypothesis. For example, if $\psi=\neg\theta$, then \begin{align*} N\models \neg\theta(\bar{b}) \iff N\not\models \theta(\bar{b}) \iff M\not\models \theta(\bar{b}) \iff M\models \neg\theta(\bar{b}), \end{align*} and conjunctions, disjunctions, and implications are handled in the same truth-functional way. It remains to handle existential quantifiers. Let $\psi(\bar{z})$ be $\exists x\,\theta(x,\bar{z})$, and assume the induction hypothesis is already known for $\theta(x,\bar{z})$. If \begin{align*} N\models \exists x\,\theta(x,\bar{b}), \end{align*} then there is $c\in H$ such that $N\models \theta(c,\bar{b})$. By the induction hypothesis, \begin{align*} M\models \theta(c,\bar{b}), \end{align*} so $M\models \exists x\,\theta(x,\bar{b})$. Conversely, suppose \begin{align*} M\models \exists x\,\theta(x,\bar{b}). \end{align*} By the witness property proved above, there is $c\in H$ such that \begin{align*} M\models \theta(c,\bar{b}). \end{align*} Applying the induction hypothesis to $\theta$ gives \begin{align*} N\models \theta(c,\bar{b}), \end{align*} and hence \begin{align*} N\models \exists x\,\theta(x,\bar{b}). \end{align*} Thus the equivalence holds for existential formulas, completing the induction. [guided] We now turn the witness property into full elementarity. The goal is to prove that every $L$-formula has the same truth value in $N$ and in $M$ when its parameters come from $H$. Formally, we prove by induction on formulas $\psi(\bar{z})$ that for every tuple $\bar{b}\in H^{|\bar{z}|}$, \begin{align*} N \models \psi(\bar{b}) \iff M \models \psi(\bar{b}). \end{align*} For atomic formulas, there is no quantifier to worry about. Since $N$ is the induced $L$-substructure on $H$, every $L$-term evaluated at parameters from $H$ has the same value in $N$ as in $M$, and every $L$-relation on $N$ is the restriction of the corresponding relation on $M$. Therefore atomic truth agrees. The induction steps for Boolean connectives use only the meaning of the connectives. For instance, if $\psi=\neg\theta$, then the induction hypothesis for $\theta$ gives \begin{align*} N\models \neg\theta(\bar{b}) \iff N\not\models \theta(\bar{b}) \iff M\not\models \theta(\bar{b}) \iff M\models \neg\theta(\bar{b}). \end{align*} The same argument applies to conjunctions, disjunctions, and implications by their truth tables. The only substantial case is the existential quantifier. Let \begin{align*} \psi(\bar{z}) := \exists x\,\theta(x,\bar{z}), \end{align*} and assume the induction hypothesis has already been proved for $\theta(x,\bar{z})$. First suppose $N\models \exists x\,\theta(x,\bar{b})$. Then some element $c\in H$ satisfies $N\models \theta(c,\bar{b})$. By the induction hypothesis applied to the tuple $(c,\bar{b})$, we get \begin{align*} M\models \theta(c,\bar{b}), \end{align*} so $M\models \exists x\,\theta(x,\bar{b})$. Conversely, suppose $M\models \exists x\,\theta(x,\bar{b})$. This is exactly the situation handled by the Skolem-witness step: the formula is an $L$-formula and the parameter tuple $\bar{b}$ lies in $H$. Therefore there exists $c\in H$ such that \begin{align*} M\models \theta(c,\bar{b}). \end{align*} Applying the induction hypothesis again, now from $M$ back to $N$, yields \begin{align*} N\models \theta(c,\bar{b}). \end{align*} Since $c\in H$ is an element of the universe of $N$, this gives \begin{align*} N\models \exists x\,\theta(x,\bar{b}). \end{align*} Thus existential formulas are preserved in both directions. The induction proves truth agreement for every $L$-formula with parameters from $H$. [/guided] [/step] [step:Conclude that the reduct substructure is elementary] By the previous step, for every $L$-formula $\psi(\bar{z})$ and every tuple $\bar{b}\in H^{|\bar{z}|}$, \begin{align*} N \models \psi(\bar{b}) \iff M \models \psi(\bar{b}). \end{align*} This is precisely the definition of $N\preccurlyeq M$. The conclusion is stated in the reduct language $L$, because the witness argument was required only for existential $L$-formulas and the induced structure $N$ was defined as an $L$-substructure of the $L$-reduct $M$. [/step]