Understanding types and the proof that every type is realized in an elementary extension.

Question

So I've been recently been studying types from David Marker's book and have some issues understanding them and in particular why did Marker choose to present certain proof of the following theorem

Theorem: Let $\mathcal{M}$ be an $\mathcal{L}$-structure, $A\subseteq M$, and $p$ an $n$-type over $A$. There is $\mathcal{N}$ an elementary extension of $\mathcal{M}$ such that $p$ is realized in $\mathcal{N}$.

I start by defining types. If $\mathcal{M}$ is an $\mathcal{L}$-structure and $A\subseteq M$ then $\text{Th}_A(\mathcal{M})$ is the theory of $\mathcal{M}$ in an extended language $\mathcal{L}_A$ adding a constant symbol for each $a\in A$ and interpreting $\mathcal{M}$ in the obvious manner. $p$ is an $n$-type if it is a set of $\mathcal{L}_A$ formulas in free variables $v_1, \ldots, v_n$ and $p \cup \text{Th}_A(\mathcal{M})$ is satisfiable. The type is complete if $\phi\in p$ or $\neg\phi\in p$ for all $\mathcal{L}_A$ formulas in free variables $v_1, \ldots, v_n$.

The way I undertand the definition is at follows. In a language $\mathcal{L}^*$ that extends $\mathcal{L}_A$ by adding a constant symbol for each variable $v_i$ in the formulas in $p$, $p$ is a type if $p \cup \text{Th}_A(\mathcal{M})$ is satisfiable. The type is complete if $p \cup \text{Th}_A(\mathcal{M})$ is complete in said language. $p \cup \text{Th}_A(\mathcal{M})$ is satisfiable (equiv. finitely satisfiable) is equivalent to, for any $q$ finite subset of $p$, and if $\psi$ is the conjuntion of all formulas in $q$, the sentence $\exists v_1,\ldots, v_n \;\psi$ belongs in $\text{Th}_A(\mathcal{M})$. I like to call this "$p$ is finitely realised by $\mathcal{M}$".

So let's get back to the theorem. Note firstly that $\text{Th}_M(\mathcal{M})=ED(\mathcal{M})$ is the elementary diagram of $\mathcal{M}$. We must proof that $p\cup ED(\mathcal{M})$ is consistent. The proof in Marker's book is at follows. Suppose not and let without loss of generality $\phi(\bar{v},\bar{a}) \wedge \psi(\bar{a},\bar{b})$ be the formula that is inconsistent (with $\phi$ conjunction of formulas in $p$ and $\psi$ conjunction of formulas in $ED(\mathcal{M})$, and with $\bar{a}$ being an array of elements in $A$, $\bar{b}$ an array in $M\setminus A$ and $\bar{v}$ the $n$-array of type variables).

Now clearly $\exists \bar{w} \psi(\bar{a},\bar{w})\in\text{Th}_A(\mathcal{M})$ and so given a model of $p \cup \text{Th}_A(\mathcal{M})$ we can interpret $\bar{b}$ to be the elements that witness $\exists \bar{w} \psi(\bar{a},\bar{w})$ proving that the above formula is in fact satisfiable.

I wonder however if the theorem was not trivial given the understading of a type as a set of formulas "finitely witnessed" by $\mathcal{M}$. Basically, $\mathcal{M}$ will satisfy any finite subset of $p\cup \text{Th}_A(\mathcal{M})$ as much as it will satisfy any finite subset of $p\cup ED(\mathcal{M})$.

Am I making sense? Or is my take on types entirely or partially mistaken? Am I missing something in this proof?

Answer 1

I agree with your assessment that Marker's proof is more complicated than necessary. Since you've already established that $p$ is finitely satisfiable in $\mathcal{M}$, $p\cup ED(\mathcal{M})$ is clearly finitely satisfiable (in $\mathcal{M}$), hence it's consistent by compactness.