 Solution

A partial type $p(\mathbf{x})$ is a set of $L$-first-order formulas in a fixed tuple $\mathbf{x}=(x_1,\dots ,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 $\phi (\mathbf{x})$ it contains exactly one of $\phi ,\neg \phi$.

Add new constants $\mathbf{c}$ and considerEvery 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, 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 \phi )$ for every $\phi \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.