[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*}
[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]
[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]
