Type is Realized in some Elementary Extension

== Theorem ==
Let $\MM$ be an $\LL$-structure.
Let $A$ be a subset of the universe of $\MM$.
Let $p$ be an $n$-type over $A$.
There exists an elementary extension of $\MM$ which realizes $p$.
== Proof ==
The idea is to work in a language with constant symbols for all elements of $\MM$ and show that the union of $p$ and the elementary diagram of $\MM$ is satisfiable.
Since $\MM$ naturally embeds into any model of such a theory, this will prove the theorem.
Let $\LL_\MM$ be the language obtained by adding to $\LL$ constant symbols for each element of $\MM$.
Denote by $\map {\operatorname {Diag}_{\mathrm {el} } } \MM$ the elementary diagram of $\MM$.
Let $T$ be $p \cup \map {\operatorname {Diag}_{\mathrm{el} } } \MM$.
We will show that $T$ is finitely satisfiable.
It will follow by the Compactness Theorem that $T$ is satisfiable.
To this end, let $\Delta$ be a finite subset of $T$.
We have that $\Delta$ is finite.
Thus it consists of:
:finitely many $\LL_A$-sentences $\phi_0, \dotsc, \phi_n$ from $p$ (which are $\LL_\MM$ sentences since $A \subseteq \MM$)
along with:
:finitely many $\LL_\MM$-sentences $\psi_0,\dots,\psi_k$ from $\map {\operatorname{Diag}_{\mathrm{el} } } \MM$.
By definition, $p$ is satisfiable by some $\LL_A$-structure $\NN$ such that:
:$\NN \models p \cup \map {\operatorname{Th}_A} \MM$
Thus, since $\phi_0, \dotsc, \phi_n \in p$:
:$\NN$ satisfies $\phi_0, \dotsc, \phi_n$.
We will show that the same $\NN$ also satisfies $\psi_0, \dotsc, \psi_k$.
The obstacle to overcome is that the $\psi_i$ are $\LL_\MM$-formulas, and we only know $\NN$ as an $\LL_A$-structure which satisfies sentences with parameters from $A$.
The $\psi_i$ may have parameters from $\MM$ outside of $A$.
The idea is to quantify away the excess parameters and appropriately select the interpretation of new symbols so that $\NN$ is a good $\LL_\MM$-structure.
Explicitly:
Let $\psi$ be the conjunction $\psi_0 \wedge \cdots \wedge \psi_k$.
Note that since $\psi$ is an $\LL_\MM$-sentence, it can be written as an $\LL_A$-formula $\map \psi {\bar b}$, where $\bar b$ is a tuple of parameters from $\MM$ not in $A$.
By existentially quantifying away the tuple $\bar b$, we obtain an $\LL_A$-sentence $\exists \bar x \map \psi {\bar x}$.
Now, since $\MM \models \map \psi {\bar b}$, we have:
:$\MM \models \exists \bar x: \map \psi {\bar x}$
Hence $\exists \bar x: \map \psi {\bar x}$ is in $\map {\operatorname{Th}_A} \MM$.
By choice of $\NN$, it follows that:
:$\NN \models \exists \bar x: \map \psi {\bar x}$
and thus there must be some tuple $\bar c$ of elements from $\NN$ such that:
:$\NN \models \map \psi {\bar c}$
Now, by interpreting the $\LL_\MM$-symbols $\bar b$ as the elements $\bar c$, we can view $\NN$ as an $\LL_\MM$-structure which satisfies:
:$\phi_0 \wedge \cdots \wedge \phi_n \wedge \psi_0 \wedge \cdots \wedge \psi_k$. 
Thus $\NN$ satisfies all of $\Delta$.
This demonstrates that $T$ is finitely satisfiable and hence satisfiable by the Compactness Theorem.
This means that there is an $\LL_\MM$-structure $\MM^*$ which satisfies:
:$p \cup \map {\operatorname{Diag}_{\mathrm {el} } } \MM$
Since $\MM^*$ interprets a symbol for each element of $\MM$, there is an obvious embedding of $\MM$ into $\MM^*$.
This embedding is elementary since $\MM^*$ satisfies the elementary diagram of $\MM$.
Thus $\MM^*$ is an elementary extension of $\MM$.
Finally, since $\MM^*$ satisfies $p$, there must be a tuple of elements $\bar d$ such that $\MM^* \models \map \phi d$ for each $\map \phi {\bar v} \in p$.
Thus $\MM^*$ realizes $p$.
Category:Model Theory for Predicate Logic