[proofplan] We prove the equivalence by translating realization of a type into satisfiability of a theory with constants. If a tuple realizes $p(x)$ in an elementary extension of $M$, then the expansion naming $M$ and the tuple satisfies every finite fragment of the elementary diagram together with $p(c)$. Conversely, finite satisfiability of those fragments allows us to apply compactness to obtain a model of the whole expanded theory. The elementary diagram then identifies the named copy of $M$ as an elementary substructure, and the interpretations of the new constants realize $p(x)$. [/proofplan]

[step:Translate realization in an elementary extension into finite satisfiability] Assume first that $p(x)$ is a partial type over $A$ with respect to $M$. By definition, there exist an $L$-structure $N$, an elementary embedding $j: M \to N$, and a tuple $b = (b_1,\dots,b_n) \in N^n$ such that $N \models \varphi(b)$ for every $\varphi(x) \in p(x)$, where each parameter $a \in A$ is interpreted as $j(a)$ in $N$. Expand $N$ to an $L(M) \cup \{c_1,\dots,c_n\}$-structure $N^\ast$ by interpreting each constant $\bar{m}$ as $j(m)$ and each $c_i$ as $b_i$. Since $j: M \to N$ is elementary, every $L(M)$-sentence true in the natural $L(M)$-expansion of $M$ is true in $N^\ast$. Therefore \begin{align*} N^\ast \models \operatorname{ED}(M). \end{align*} Also, for every $\varphi(x) \in p(x)$, the interpretation of $\varphi(c)$ in $N^\ast$ is exactly the assertion $N \models \varphi(b)$, so \begin{align*} N^\ast \models p(c). \end{align*} Thus $N^\ast$ is a model of $\operatorname{ED}(M) \cup p(c)$, and consequently every finite subset of $\operatorname{ED}(M) \cup p(c)$ is satisfiable. [/step]

[step:Apply compactness to the expanded theory]Assume conversely that every finite subset of $\operatorname{ED}(M) \cup p(c)$ is satisfiable. Let $\Sigma$ be the $L(M) \cup \{c_1,\dots,c_n\}$-theory defined by \begin{align*} \Sigma := \operatorname{ED}(M) \cup p(c). \end{align*} By hypothesis, every finite subset of $\Sigma$ has a model. By the [Compactness Theorem for first-order logic](/theorems/4290) (citing a result not yet in the wiki: [Compactness Theorem](/theorems/2748)), there exists an $L(M) \cup \{c_1,\dots,c_n\}$-structure $N^\ast$ such that \begin{align*} N^\ast \models \Sigma. \end{align*}[/step]

[guided]We want to turn finite satisfiability into a single structure realizing all formulas in $p(x)$ at once. The natural object to which compactness applies is the expanded theory \begin{align*} \Sigma := \operatorname{ED}(M) \cup p(c), \end{align*} written in the language $L(M) \cup \{c_1,\dots,c_n\}$. Here $\operatorname{ED}(M)$ forces the named constants $\bar{m}$ to behave exactly as the elements of $M$ do, while $p(c)$ asks the new tuple of constants $c = (c_1,\dots,c_n)$ to satisfy every formula in the proposed type. The hypothesis says precisely that every finite subset of this theory $\Sigma$ is satisfiable. Therefore the Compactness Theorem for first-order logic applies: since all finite pieces of $\Sigma$ have models, the whole theory $\Sigma$ has a model. Hence there exists an $L(M) \cup \{c_1,\dots,c_n\}$-structure $N^\ast$ such that \begin{align*} N^\ast \models \operatorname{ED}(M) \cup p(c). \end{align*} This is the crucial compactness step: it replaces separate finite witnesses by one structure in which all formulas from $p(c)$ hold simultaneously.[/guided]

[step:Recover an elementary extension of $M$ from the elementary diagram] Let $N$ be the reduct of $N^\ast$ to the original language $L$. For each $m \in M$, define \begin{align*} j: M &\to N \\ m &\mapsto \bar{m}^{N^\ast}, \end{align*} where $\bar{m}^{N^\ast}$ denotes the interpretation of the constant symbol $\bar{m}$ in $N^\ast$. We show that $j$ is an elementary embedding. Let $\psi(y_1,\dots,y_k)$ be an $L$-formula, and let $m_1,\dots,m_k \in M$. If \begin{align*} M \models \psi(m_1,\dots,m_k), \end{align*} then the $L(M)$-sentence $\psi(\bar{m}_1,\dots,\bar{m}_k)$ belongs to $\operatorname{ED}(M)$, so \begin{align*} N^\ast \models \psi(\bar{m}_1,\dots,\bar{m}_k). \end{align*} Equivalently, \begin{align*} N \models \psi(j(m_1),\dots,j(m_k)). \end{align*} The same argument applied to $\neg \psi$ gives the converse implication. Hence, for every $L$-formula $\psi(y_1,\dots,y_k)$ and every $m_1,\dots,m_k \in M$, \begin{align*} M \models \psi(m_1,\dots,m_k) \quad \Longleftrightarrow \quad N \models \psi(j(m_1),\dots,j(m_k)). \end{align*} Thus $j: M \to N$ is elementary. Since elementary embeddings identify their domain with an elementary substructure of the codomain, replacing $N$ by the isomorphic copy over $j[M]$ lets us regard $M$ as an elementary substructure of $N$. In this notation, $N \succeq M$. [/step]

[step:Read the interpretations of the new constants as a realizing tuple] For each $1 \leq i \leq n$, let \begin{align*} b_i := c_i^{N^\ast} \in N, \end{align*} and define $b := (b_1,\dots,b_n) \in N^n$. Let $\varphi(x) \in p(x)$. Since $\varphi(c) \in p(c) \subset \Sigma$ and $N^\ast \models \Sigma$, we have \begin{align*} N^\ast \models \varphi(c). \end{align*} By the definition of the interpretation of the constants $c_i$ and of the parameter constants from $A \subset M$, this is exactly \begin{align*} N \models \varphi(b), \end{align*} where each parameter $a \in A$ is interpreted as the element $j(a)$, identified with $a$ after viewing $M \preceq N$. Therefore $b$ realizes every formula in $p(x)$ inside the elementary extension $N \succeq M$. Hence $p(x)$ is a partial type over $A$ with respect to $M$. [/step]