[proofplan] We prove first that the atomic diagram is exactly the data needed to make the named-copy map $a \mapsto c_a^N$ into an $L$-embedding: equality facts give injectivity, function facts give preservation of function symbols, and relation facts give preservation and reflection of relation symbols. Then we prove the elementary version by translating every $L$-formula with parameters from $M$ into an $L(M)$-sentence by replacing each parameter $a$ with the constant symbol $c_a$. Satisfaction of all such translated sentences in $N$ is precisely preservation of truth of all formulas with parameters, which is the definition of elementary embedding. [/proofplan] [step:Show that the atomic diagram makes the named-copy map an embedding] Assume $N \models \operatorname{Diag}_{\mathrm{at}}(M)$. Define the map \begin{align*} i: M &\to N|_L \\ a &\mapsto c_a^N. \end{align*} We first prove that $i$ is injective. If $a,b \in M$ and $a \neq b$, then the negated atomic $L(M)$-sentence $c_a \neq c_b$ belongs to $\operatorname{Diag}_{\mathrm{at}}(M)$, since it is true in $M_M$. Hence $N \models c_a \neq c_b$, so $c_a^N \neq c_b^N$, and therefore $i(a) \neq i(b)$. Let $f$ be an $n$-ary function symbol of $L$, and let $a_1,\dots,a_n \in M$. Define $b \in M$ by \begin{align*} b = f^M(a_1,\dots,a_n). \end{align*} The atomic $L(M)$-sentence \begin{align*} f(c_{a_1},\dots,c_{a_n}) = c_b \end{align*} is true in $M_M$, so it belongs to $\operatorname{Diag}_{\mathrm{at}}(M)$. Since $N$ satisfies the atomic diagram, \begin{align*} f^N(c_{a_1}^N,\dots,c_{a_n}^N) = c_b^N. \end{align*} By the definition of $i$, this says \begin{align*} f^{N|_L}(i(a_1),\dots,i(a_n)) = i(f^M(a_1,\dots,a_n)). \end{align*} Thus $i$ preserves every function symbol of $L$. Let $R$ be an $n$-ary relation symbol of $L$, and let $a_1,\dots,a_n \in M$. If $M \models R(a_1,\dots,a_n)$, then the atomic sentence $R(c_{a_1},\dots,c_{a_n})$ belongs to $\operatorname{Diag}_{\mathrm{at}}(M)$, so \begin{align*} N \models R(c_{a_1},\dots,c_{a_n}). \end{align*} Equivalently, \begin{align*} N|_L \models R(i(a_1),\dots,i(a_n)). \end{align*} If $M \not\models R(a_1,\dots,a_n)$, then the negated atomic sentence $\neg R(c_{a_1},\dots,c_{a_n})$ belongs to $\operatorname{Diag}_{\mathrm{at}}(M)$, so \begin{align*} N|_L \not\models R(i(a_1),\dots,i(a_n)). \end{align*} Therefore, for every relation symbol $R$ of $L$ and every tuple $a_1,\dots,a_n \in M$, \begin{align*} M \models R(a_1,\dots,a_n) \quad\Longleftrightarrow\quad N|_L \models R(i(a_1),\dots,i(a_n)). \end{align*} The map $i$ is injective, preserves all function symbols, and preserves and reflects all relation symbols. Hence $i: M \to N|_L$ is an $L$-embedding. [guided] Assume $N \models \operatorname{Diag}_{\mathrm{at}}(M)$. We must prove that the named-copy map \begin{align*} i: M &\to N|_L \\ a &\mapsto c_a^N \end{align*} is an embedding of $L$-structures. An embedding must be injective, must respect every function symbol, and must preserve and reflect every relation symbol. First, take $a,b \in M$ with $a \neq b$. In the canonical expansion $M_M$, the sentence $c_a \neq c_b$ is true because $c_a^{M_M} = a$ and $c_b^{M_M} = b$. Hence $c_a \neq c_b$ is in the atomic diagram. Since $N$ satisfies the atomic diagram, $N \models c_a \neq c_b$, so $c_a^N \neq c_b^N$. Thus $i(a) \neq i(b)$, proving injectivity. Next, let $f$ be an $n$-ary function symbol of $L$, and choose $a_1,\dots,a_n \in M$. Define the element $b \in M$ by \begin{align*} b = f^M(a_1,\dots,a_n). \end{align*} In $M_M$, the atomic sentence \begin{align*} f(c_{a_1},\dots,c_{a_n}) = c_b \end{align*} is true, because the left-hand side is interpreted as $f^M(a_1,\dots,a_n)$ and the right-hand side is interpreted as $b$. Therefore this sentence lies in $\operatorname{Diag}_{\mathrm{at}}(M)$. Since $N$ satisfies the atomic diagram, \begin{align*} f^N(c_{a_1}^N,\dots,c_{a_n}^N) = c_b^N. \end{align*} Using the definition $i(a) = c_a^N$, this becomes \begin{align*} f^{N|_L}(i(a_1),\dots,i(a_n)) = i(f^M(a_1,\dots,a_n)). \end{align*} So $i$ respects the interpretation of $f$. Finally, let $R$ be an $n$-ary relation symbol of $L$, and let $a_1,\dots,a_n \in M$. If $M \models R(a_1,\dots,a_n)$, then $R(c_{a_1},\dots,c_{a_n})$ is an atomic sentence true in $M_M$, hence belongs to the atomic diagram. Since $N$ satisfies it, \begin{align*} N|_L \models R(i(a_1),\dots,i(a_n)). \end{align*} If instead $M \not\models R(a_1,\dots,a_n)$, then the negated atomic sentence $\neg R(c_{a_1},\dots,c_{a_n})$ is true in $M_M$ and hence belongs to the atomic diagram. Therefore $N$ satisfies that negated atomic sentence, which gives \begin{align*} N|_L \not\models R(i(a_1),\dots,i(a_n)). \end{align*} Thus, for every tuple from $M$, \begin{align*} M \models R(a_1,\dots,a_n) \quad\Longleftrightarrow\quad N|_L \models R(i(a_1),\dots,i(a_n)). \end{align*} We have verified exactly the defining conditions of an $L$-embedding. [/guided] [/step] [step:Recover the atomic diagram from an embedding] Assume that \begin{align*} i: M &\to N|_L \\ a &\mapsto c_a^N \end{align*} is an $L$-embedding. We prove that $N \models \operatorname{Diag}_{\mathrm{at}}(M)$. Let $\sigma$ be an atomic $L(M)$-sentence true in $M_M$. Every closed $L(M)$-term $t$ has a value $t^{M_M} \in M$ in $M_M$ and a value $t^N \in N$ in $N$. We first prove by induction on the construction of $t$ that \begin{align*} t^N = i(t^{M_M}). \end{align*} If $t$ is a constant symbol $c_a$ with $a \in M$, then \begin{align*} t^N = c_a^N = i(a) = i(t^{M_M}). \end{align*} If $t$ is a constant symbol $d$ of the original language $L$, then preservation of the $0$-ary function symbol $d$ gives \begin{align*} t^N = d^N = i(d^M) = i(t^{M_M}). \end{align*} If $t = f(t_1,\dots,t_n)$, where $f$ is an $n$-ary function symbol of $L$, then the induction hypothesis gives $t_k^N = i(t_k^{M_M})$ for $1 \leq k \leq n$. Since $i$ preserves $f$, \begin{align*} t^N &= f^N(t_1^N,\dots,t_n^N) \\ &= f^N(i(t_1^{M_M}),\dots,i(t_n^{M_M})) \\ &= i(f^M(t_1^{M_M},\dots,t_n^{M_M})) \\ &= i(t^{M_M}). \end{align*} Now suppose $\sigma$ has the form $t_1 = t_2$. Since $M_M \models t_1 = t_2$, we have $t_1^{M_M} = t_2^{M_M}$. The term computation gives \begin{align*} t_1^N = i(t_1^{M_M}) = i(t_2^{M_M}) = t_2^N, \end{align*} so $N \models t_1 = t_2$. Suppose instead $\sigma$ has the form $R(t_1,\dots,t_n)$, where $R$ is an $n$-ary relation symbol of $L$. Since $M_M \models R(t_1,\dots,t_n)$, we have \begin{align*} M \models R(t_1^{M_M},\dots,t_n^{M_M}). \end{align*} Because $i$ preserves relations, \begin{align*} N|_L \models R(i(t_1^{M_M}),\dots,i(t_n^{M_M})). \end{align*} Using $t_k^N = i(t_k^{M_M})$ for each $k$, this is exactly \begin{align*} N \models R(t_1,\dots,t_n). \end{align*} Thus every atomic sentence true in $M_M$ is true in $N$. If $\neg \sigma$ is a negated atomic sentence true in $M_M$, then $\sigma$ is atomic and false in $M_M$. If $N \models \sigma$, the preceding equality and relation arguments, using injectivity and reflection of relations, would imply $M_M \models \sigma$, a contradiction. Hence $N \models \neg \sigma$. Therefore $N \models \operatorname{Diag}_{\mathrm{at}}(M)$. [/step] [step:Translate formulas with parameters into sentences with named constants] For every $L$-formula $\varphi(x_1,\dots,x_n)$ and every tuple $(a_1,\dots,a_n) \in M^n$, define the associated $L(M)$-sentence $\varphi[c_{a_1},\dots,c_{a_n}]$ to be the sentence obtained by replacing each free occurrence of $x_k$ by the constant symbol $c_{a_k}$, for $1 \leq k \leq n$. By the semantics of constants in the canonical expansion $M_M$, \begin{align*} M \models \varphi(a_1,\dots,a_n) \quad\Longleftrightarrow\quad M_M \models \varphi[c_{a_1},\dots,c_{a_n}]. \end{align*} Similarly, because $c_a^N = i(a)$ for every $a \in M$, \begin{align*} N|_L \models \varphi(i(a_1),\dots,i(a_n)) \quad\Longleftrightarrow\quad N \models \varphi[c_{a_1},\dots,c_{a_n}]. \end{align*} [guided] Fix an $L$-formula $\varphi(x_1,\dots,x_n)$ and a tuple $(a_1,\dots,a_n) \in M^n$. The purpose of the language $L(M)$ is to turn formulas with parameters from $M$ into sentences. We define $\varphi[c_{a_1},\dots,c_{a_n}]$ to be the $L(M)$-sentence obtained by substituting the constant symbol $c_{a_k}$ for the free variable $x_k$ for every $1 \leq k \leq n$. In the canonical expansion $M_M$, the constant $c_{a_k}$ is interpreted as $a_k$. Therefore evaluating the sentence $\varphi[c_{a_1},\dots,c_{a_n}]$ in $M_M$ is exactly the same as evaluating the formula $\varphi(x_1,\dots,x_n)$ in $M$ under the assignment $x_k \mapsto a_k$. Hence \begin{align*} M \models \varphi(a_1,\dots,a_n) \quad\Longleftrightarrow\quad M_M \models \varphi[c_{a_1},\dots,c_{a_n}]. \end{align*} Likewise, in $N$, the constant $c_{a_k}$ is interpreted as $c_{a_k}^N = i(a_k)$. Thus evaluating the same $L(M)$-sentence in $N$ is exactly the same as evaluating the original $L$-formula in the reduct $N|_L$ at the tuple $(i(a_1),\dots,i(a_n))$. Therefore \begin{align*} N|_L \models \varphi(i(a_1),\dots,i(a_n)) \quad\Longleftrightarrow\quad N \models \varphi[c_{a_1},\dots,c_{a_n}]. \end{align*} These two equivalences are the bridge between elementary embeddings and elementary diagrams. [/guided] [/step] [step:Show that the elementary diagram is equivalent to elementary embedding] Assume first that $N \models \operatorname{Diag}_{\mathrm{el}}(M)$. Since every atomic or negated atomic sentence true in $M_M$ is an $L(M)$-sentence true in $M_M$, we have \begin{align*} \operatorname{Diag}_{\mathrm{at}}(M) \subseteq \operatorname{Diag}_{\mathrm{el}}(M). \end{align*} Thus $N \models \operatorname{Diag}_{\mathrm{at}}(M)$, and the first part of the proof shows that $i: M \to N|_L$ is an $L$-embedding. Let $\varphi(x_1,\dots,x_n)$ be an $L$-formula and let $(a_1,\dots,a_n) \in M^n$. If \begin{align*} M \models \varphi(a_1,\dots,a_n), \end{align*} then \begin{align*} M_M \models \varphi[c_{a_1},\dots,c_{a_n}]. \end{align*} So $\varphi[c_{a_1},\dots,c_{a_n}] \in \operatorname{Diag}_{\mathrm{el}}(M)$, and hence \begin{align*} N \models \varphi[c_{a_1},\dots,c_{a_n}]. \end{align*} By the translation equivalence, \begin{align*} N|_L \models \varphi(i(a_1),\dots,i(a_n)). \end{align*} Conversely, if $M \not\models \varphi(a_1,\dots,a_n)$, then \begin{align*} M_M \models \neg \varphi[c_{a_1},\dots,c_{a_n}]. \end{align*} Since $\neg \varphi[c_{a_1},\dots,c_{a_n}]$ belongs to $\operatorname{Diag}_{\mathrm{el}}(M)$, we get \begin{align*} N \models \neg \varphi[c_{a_1},\dots,c_{a_n}], \end{align*} and therefore \begin{align*} N|_L \not\models \varphi(i(a_1),\dots,i(a_n)). \end{align*} Hence, for every $L$-formula $\varphi(x_1,\dots,x_n)$ and every tuple $(a_1,\dots,a_n) \in M^n$, \begin{align*} M \models \varphi(a_1,\dots,a_n) \quad\Longleftrightarrow\quad N|_L \models \varphi(i(a_1),\dots,i(a_n)). \end{align*} Thus $i$ is an elementary $L$-embedding. Conversely, assume that $i: M \to N|_L$ is an elementary $L$-embedding. Let $\sigma$ be an $L(M)$-sentence true in $M_M$. Since $\sigma$ contains only finitely many added constant symbols, choose $a_1,\dots,a_n \in M$ such that every added constant symbol occurring in $\sigma$ is among $c_{a_1},\dots,c_{a_n}$. There is an $L$-formula $\varphi(x_1,\dots,x_n)$ such that \begin{align*} \sigma = \varphi[c_{a_1},\dots,c_{a_n}]. \end{align*} Since $M_M \models \sigma$, the translation equivalence gives \begin{align*} M \models \varphi(a_1,\dots,a_n). \end{align*} Because $i$ is elementary, \begin{align*} N|_L \models \varphi(i(a_1),\dots,i(a_n)). \end{align*} Applying the translation equivalence again, \begin{align*} N \models \varphi[c_{a_1},\dots,c_{a_n}]. \end{align*} Since this sentence is $\sigma$, we have $N \models \sigma$. Therefore every sentence in $\operatorname{Diag}_{\mathrm{el}}(M)$ is true in $N$, so \begin{align*} N \models \operatorname{Diag}_{\mathrm{el}}(M). \end{align*} This proves the equivalence between elementary embedding and satisfaction of the elementary diagram. [/step]