= Solution
A <partial type> $p(\mathbf x)$ is a set of $L$-<first-order formulas> in a fixed tuple $\mathbf x=(x_1,\ldots,x_n)$ jointly consistent with $T$. A <complete type>, the usual meaning of an $n$-type here, is maximal among such consistent sets: for each <first-order formula> $\varphi(\mathbf x)$ it contains exactly one of $\varphi,\neg\varphi$.
Add new constants $\mathbf c$ and consider
$$
T\cup\{\varphi(\mathbf c):\varphi\in p\}.
$$
Every finite subset is satisfiable by consistency of the type. The <compactness theorem> gives a <first-order model> of the full set. Its $L$-reduct is a <first-order model> of $T$, and the interpretations of $\mathbf c$ realize $p$. This proof applies to partial as well as complete types.
For a <complete theory> in a countable language, \b[the types realized in every <first-order model> are exactly the isolated types]. An <isolated type> has a consistent <first-order formula> $\theta\in p$ such that $T\models\forall\mathbf x(\theta\to\varphi)$ for every $\varphi\in p$. Completeness forces $T\models\exists\mathbf x\theta$, so every <first-order model> realizes $p$; the converse is the <omitting types theorem>. Countability is a hypothesis of that converse, not of the preceding compactness realization argument. For a <partial type> the corresponding criterion is an isolating consistent <first-order formula>, together with its existence in every <first-order model>; it need not itself belong to the <partial type>.
If $T$ is not complete, no one complete $n$-type can be realized in every <first-order model> of $T$: a <complete type> decides sentences, and two completions of $T$ disagree on some sentence. Thus the completeness and countability hypotheses must be retained when using the isolated-type characterization.
Back to article page
