[proofplan] We prove the stronger statement that every $L$-formula has the same truth value in $N$ and in $M$ when all free variables are assigned values in $H$. The induced-substructure hypothesis first gives agreement for terms and atomic formulas. Boolean connectives then follow by induction on formula complexity. The only substantive point is the existential case: a witness in $M$ can be replaced by the chosen Skolem witness, and closure of $H$ puts that witness inside $N$. [/proofplan] [step:Show that terms with parameters from $H$ have the same value in $N$ and in $M$] Let $t(z_1,\dots,z_m)$ be an $L$-term and let $a=(a_1,\dots,a_m)\in H^m$. We prove by induction on the construction of $t$ that \begin{align*} t^N(a)=t^M(a)\in H. \end{align*} If $t$ is a variable $z_i$, then $t^N(a)=a_i=t^M(a)$, and $a_i\in H$ by assumption on $a$. If $t$ is a constant symbol $c$, then $t^N(a)=c^N=c^M=t^M(a)$, and $c^M\in H$ by closure under constants. Now suppose \begin{align*} t = g(t_1,\dots,t_k), \end{align*} where $g$ is a $k$-ary function symbol of $L$ and $t_1,\dots,t_k$ are $L$-terms. By the induction hypothesis, for each $i\in\{1,\dots,k\}$, \begin{align*} t_i^N(a)=t_i^M(a)\in H. \end{align*} Since $N$ interprets $g$ by restricting $g^M$ to $H^k$, \begin{align*} t^N(a) &= g^N(t_1^N(a),\dots,t_k^N(a)) \\ &= g^M(t_1^M(a),\dots,t_k^M(a)) \\ &= t^M(a). \end{align*} The tuple $(t_1^M(a),\dots,t_k^M(a))$ lies in $H^k$, so closure of $H$ under $g^M$ gives $t^M(a)\in H$. [guided] Before comparing formulas, we need to know that every term denotes the same element in the small structure and in the large structure. Let $t(z_1,\dots,z_m)$ be an $L$-term and let $a=(a_1,\dots,a_m)\in H^m$. We prove, by induction on how the term $t$ is built, that \begin{align*} t^N(a)=t^M(a)\in H. \end{align*} There are two base cases. If $t$ is a variable $z_i$, then both structures evaluate $t$ at the assigned element $a_i$, so \begin{align*} t^N(a)=a_i=t^M(a). \end{align*} Because $a\in H^m$, we have $a_i\in H$. If $t$ is a constant symbol $c$, then the induced substructure uses the same interpretation of $c$ as $M$: \begin{align*} t^N(a)=c^N=c^M=t^M(a). \end{align*} The hypothesis that $H$ contains all constant interpretations gives $c^M\in H$. For the inductive step, suppose \begin{align*} t = g(t_1,\dots,t_k), \end{align*} where $g$ is a $k$-ary function symbol and $t_1,\dots,t_k$ are simpler terms. The induction hypothesis says that each inner term has the same value in $N$ and $M$, and that this value belongs to $H$: \begin{align*} t_i^N(a)=t_i^M(a)\in H \end{align*} for every $i\in\{1,\dots,k\}$. Since $N$ is induced from $M$, the interpretation $g^N$ is exactly the restriction of $g^M$ to $H^k$. Therefore \begin{align*} t^N(a) &= g^N(t_1^N(a),\dots,t_k^N(a)) \\ &= g^M(t_1^M(a),\dots,t_k^M(a)) \\ &= t^M(a). \end{align*} Finally, the tuple of inputs to $g^M$ lies in $H^k$, and $H$ is closed under the interpretation of every function symbol. Hence $t^M(a)\in H$. [/guided] [/step] [step:Establish agreement for atomic formulas] Let $\theta(z_1,\dots,z_m)$ be an atomic $L$-formula and let $a\in H^m$. We show \begin{align*} N \models \theta(a) \quad \iff \quad M \models \theta(a). \end{align*} If $\theta$ is an equality $t_1=t_2$, then the preceding step gives \begin{align*} t_1^N(a)=t_1^M(a), \qquad t_2^N(a)=t_2^M(a), \end{align*} so equality holds in $N$ exactly when it holds in $M$. If $\theta$ is of the form $R(t_1,\dots,t_k)$, where $R$ is a $k$-ary relation symbol, then the preceding step gives $t_i^N(a)=t_i^M(a)\in H$ for each $i$. Since $R^N$ is the restriction of $R^M$ to $H^k$, \begin{align*} N \models R(t_1(a),\dots,t_k(a)) \quad \iff \quad M \models R(t_1(a),\dots,t_k(a)). \end{align*} Thus atomic formulas agree. [/step] [step:Propagate agreement through Boolean connectives] We prove by induction on formula complexity that for every $L$-formula $\psi(z_1,\dots,z_m)$ and every $a\in H^m$, \begin{align*} N \models \psi(a) \quad \iff \quad M \models \psi(a). \end{align*} The atomic case was proved in the preceding step. Suppose the equivalence holds for $\psi$. Then \begin{align*} N \models \neg \psi(a) &\iff \text{not } N \models \psi(a) \\ &\iff \text{not } M \models \psi(a) \\ &\iff M \models \neg \psi(a). \end{align*} Suppose the equivalence holds for $\psi_1$ and $\psi_2$. Then \begin{align*} N \models (\psi_1\wedge \psi_2)(a) &\iff N \models \psi_1(a)\text{ and }N \models \psi_2(a) \\ &\iff M \models \psi_1(a)\text{ and }M \models \psi_2(a) \\ &\iff M \models (\psi_1\wedge \psi_2)(a). \end{align*} The same argument applies to any Boolean connective definable from $\neg$ and $\wedge$. [/step] [step:Use the Skolem witness to handle existential quantifiers] Let $\psi(z_1,\dots,z_m)$ be the formula $\exists x\,\varphi(x,z_1,\dots,z_m)$, and assume the induction hypothesis holds for $\varphi(x,z_1,\dots,z_m)$. Fix $a=(a_1,\dots,a_m)\in H^m$. First suppose \begin{align*} M \models \exists x\,\varphi(x,a). \end{align*} By the defining property of the chosen Skolem function \begin{align*} s_\varphi: |M|^m &\to |M|, \end{align*} we have \begin{align*} M \models \varphi(s_\varphi(a),a). \end{align*} Since $a\in H^m$ and $H$ is closed under $s_\varphi$, the element $s_\varphi(a)$ belongs to $H$. Applying the induction hypothesis to the tuple $(s_\varphi(a),a)\in H^{m+1}$ gives \begin{align*} N \models \varphi(s_\varphi(a),a), \end{align*} and therefore \begin{align*} N \models \exists x\,\varphi(x,a). \end{align*} Conversely, suppose \begin{align*} N \models \exists x\,\varphi(x,a). \end{align*} Then there exists $b\in H$ such that \begin{align*} N \models \varphi(b,a). \end{align*} Because $(b,a)\in H^{m+1}$, the induction hypothesis gives \begin{align*} M \models \varphi(b,a). \end{align*} Since $b\in H\subseteq |M|$, this implies \begin{align*} M \models \exists x\,\varphi(x,a). \end{align*} Thus existential formulas agree. [guided] This is the only place where the Skolem functions are used. Let \begin{align*} \psi(z_1,\dots,z_m) \end{align*} be the formula \begin{align*} \exists x\,\varphi(x,z_1,\dots,z_m), \end{align*} and assume, as the induction hypothesis, that $\varphi$ already has the same truth value in $N$ and in $M$ for all parameter tuples from $H$. Fix a tuple $a=(a_1,\dots,a_m)\in H^m$. We first prove the direction from $M$ to $N$. Suppose \begin{align*} M \models \exists x\,\varphi(x,a). \end{align*} The problem is that an arbitrary witness in $M$ need not lie in $H$, so it need not be available as an element of $N$. The chosen Skolem function supplies a controlled witness. By hypothesis, the function \begin{align*} s_\varphi: |M|^m &\to |M| \end{align*} satisfies \begin{align*} M \models \varphi(s_\varphi(a),a) \end{align*} whenever $M \models \exists x\,\varphi(x,a)$. Because $a\in H^m$ and $H$ is closed under this Skolem function, we also have \begin{align*} s_\varphi(a)\in H. \end{align*} Now the induction hypothesis applies to the tuple $(s_\varphi(a),a)\in H^{m+1}$ and gives \begin{align*} N \models \varphi(s_\varphi(a),a). \end{align*} Therefore $N$ has a witness to the existential formula, namely $s_\varphi(a)$, and hence \begin{align*} N \models \exists x\,\varphi(x,a). \end{align*} For the reverse direction, suppose \begin{align*} N \models \exists x\,\varphi(x,a). \end{align*} Then there exists an element $b\in H$ such that \begin{align*} N \models \varphi(b,a). \end{align*} Here no Skolem function is needed: every element of $N$ is already an element of $M$, because the universe of $N$ is $H\subseteq |M|$. Since $(b,a)\in H^{m+1}$, the induction hypothesis gives \begin{align*} M \models \varphi(b,a). \end{align*} Thus $b$ is also a witness in $M$, so \begin{align*} M \models \exists x\,\varphi(x,a). \end{align*} Both directions are proved, so existential formulas agree. [/guided] [/step] [step:Conclude that the induced substructure is elementary] By the preceding induction, for every $L$-formula $\psi(z_1,\dots,z_m)$ and every $a\in H^m$, \begin{align*} N \models \psi(a) \quad \iff \quad M \models \psi(a). \end{align*} This is precisely the definition of $N$ being an elementary substructure of $M$. Therefore \begin{align*} N \preccurlyeq M. \end{align*} [/step]