[proofplan] We prove both directions directly from the definition of elementary substructure. The forward implication says that if $\mathcal{N}$ and $\mathcal{M}$ agree on all formulas with parameters from $N$, then any existential statement true in $\mathcal{M}$ is already true in $\mathcal{N}$ and hence has a witness in $N$. For the reverse implication, we prove by induction on formulas that $\mathcal{N}$ and $\mathcal{M}$ have the same truth values on all formulas with parameters from $N$; the only non-formal step is the existential case, where the assumed witness condition supplies an element of $N$. [/proofplan] [step:Derive the witness condition from elementarity] Assume $\mathcal{N} \preccurlyeq \mathcal{M}$. Let $n \geq 0$ be an integer, let $\varphi(x,y_1,\dots,y_n)$ be an $L$-formula, and let $a = (a_1,\dots,a_n) \in N^n$. Suppose \begin{align*} \mathcal{M} \models \exists x\,\varphi(x,a_1,\dots,a_n). \end{align*} Since $\mathcal{N} \preccurlyeq \mathcal{M}$ and all parameters $a_1,\dots,a_n$ lie in $N$, we have \begin{align*} \mathcal{N} \models \exists x\,\varphi(x,a_1,\dots,a_n). \end{align*} By the semantics of the existential quantifier, there exists $b \in N$ such that \begin{align*} \mathcal{N} \models \varphi(b,a_1,\dots,a_n). \end{align*} Again using $\mathcal{N} \preccurlyeq \mathcal{M}$, now applied to the formula $\varphi(x,y_1,\dots,y_n)$ with parameters $(b,a_1,\dots,a_n) \in N^{n+1}$, we obtain \begin{align*} \mathcal{M} \models \varphi(b,a_1,\dots,a_n). \end{align*} Thus the Tarski-Vaught witness condition holds. [/step] [step:Prove agreement on terms and atomic formulas] Assume conversely that the stated witness condition holds. We first record the atomic base case needed for the induction on formulas. Let $m \geq 0$ be an integer, and let $c = (c_1,\dots,c_m) \in N^m$. For every $L$-term $t(z_1,\dots,z_m)$, the value of $t$ at $c$ computed in $\mathcal{N}$ equals the value of $t$ at $c$ computed in $\mathcal{M}$: \begin{align*} t^{\mathcal{N}}(c_1,\dots,c_m) = t^{\mathcal{M}}(c_1,\dots,c_m). \end{align*} This follows by structural induction on terms. Constants are interpreted in $\mathcal{N}$ as their interpretations in $\mathcal{M}$, because $\mathcal{N}$ is a substructure. Variables evaluate to the same assigned elements. If $t = f(t_1,\dots,t_k)$ for a $k$-ary function symbol $f \in L$, then the induction hypothesis gives agreement on the values of $t_1,\dots,t_k$, and the interpretation $f^{\mathcal{N}}$ is the restriction of $f^{\mathcal{M}}$ to $N^k$. It follows that $\mathcal{N}$ and $\mathcal{M}$ agree on atomic formulas with parameters from $N$. Indeed, if $\alpha(z_1,\dots,z_m)$ is an equality $s = t$, then the preceding term agreement gives \begin{align*} \mathcal{N} \models s(c) = t(c) \iff s^{\mathcal{N}}(c) = t^{\mathcal{N}}(c) \iff s^{\mathcal{M}}(c) = t^{\mathcal{M}}(c) \iff \mathcal{M} \models s(c) = t(c). \end{align*} If $\alpha(z_1,\dots,z_m)$ is $R(t_1,\dots,t_k)$ for a $k$-ary relation symbol $R \in L$, then term agreement and the fact that $R^{\mathcal{N}} = R^{\mathcal{M}} \cap N^k$ give \begin{align*} \mathcal{N} \models R(t_1(c),\dots,t_k(c)) \iff \mathcal{M} \models R(t_1(c),\dots,t_k(c)). \end{align*} [/step] [step:Induct on formulas to transfer truth between $\mathcal{N}$ and $\mathcal{M}$] We prove the following statement by induction on the construction of $L$-formulas: for every integer $m \geq 0$, every $L$-formula $\psi(z_1,\dots,z_m)$, and every tuple $c = (c_1,\dots,c_m) \in N^m$, \begin{align*} \mathcal{N} \models \psi(c_1,\dots,c_m) \iff \mathcal{M} \models \psi(c_1,\dots,c_m). \end{align*} The atomic case was proved in the previous step. For Boolean connectives, the conclusion follows directly from the induction hypothesis and the semantics of $\neg$, $\wedge$, $\vee$, and $\implies$. For example, if $\psi = \neg \theta$, then \begin{align*} \mathcal{N} \models \neg \theta(c) \iff \mathcal{N} \not\models \theta(c) \iff \mathcal{M} \not\models \theta(c) \iff \mathcal{M} \models \neg \theta(c). \end{align*} The other Boolean connectives are handled by the same truth-functional argument. It remains to handle existential quantification. Let \begin{align*} \psi(z_1,\dots,z_m) := \exists x\,\theta(x,z_1,\dots,z_m). \end{align*} First suppose \begin{align*} \mathcal{N} \models \exists x\,\theta(x,c_1,\dots,c_m). \end{align*} Then there exists $b \in N$ such that \begin{align*} \mathcal{N} \models \theta(b,c_1,\dots,c_m). \end{align*} By the induction hypothesis applied to $\theta$ and the tuple $(b,c_1,\dots,c_m) \in N^{m+1}$, \begin{align*} \mathcal{M} \models \theta(b,c_1,\dots,c_m). \end{align*} Therefore \begin{align*} \mathcal{M} \models \exists x\,\theta(x,c_1,\dots,c_m). \end{align*} Conversely suppose \begin{align*} \mathcal{M} \models \exists x\,\theta(x,c_1,\dots,c_m). \end{align*} By the assumed Tarski-Vaught witness condition applied to the formula $\theta(x,z_1,\dots,z_m)$ and the parameter tuple $c \in N^m$, there exists $b \in N$ such that \begin{align*} \mathcal{M} \models \theta(b,c_1,\dots,c_m). \end{align*} By the induction hypothesis applied to $\theta$ and $(b,c_1,\dots,c_m) \in N^{m+1}$, \begin{align*} \mathcal{N} \models \theta(b,c_1,\dots,c_m). \end{align*} Hence \begin{align*} \mathcal{N} \models \exists x\,\theta(x,c_1,\dots,c_m). \end{align*} This completes the induction. [/step] [step:Conclude that $\mathcal{N}$ is an elementary substructure of $\mathcal{M}$] The induction proves that every $L$-formula has the same truth value in $\mathcal{N}$ and $\mathcal{M}$ when all free variables are assigned elements of $N$. This is exactly the definition of \begin{align*} \mathcal{N} \preccurlyeq \mathcal{M}. \end{align*} Therefore the witness condition implies $\mathcal{N} \preccurlyeq \mathcal{M}$, and the first step proved the converse. The equivalence follows. [/step]