= Solution
A precise countable-language form of the <omitting types theorem> is the following. Let $T$ be a consistent <first-order theory> in a countable <first-order language>, and let $(p_j(\bar x_j))_{j\in\mathbb N}$ be a countable family of <nonprincipal partial types>, each in finitely many variables. Then \b[there is a finite or countably infinite model of $T$ omitting all the $p_j$.]
A <partial type> is a set of formulas jointly consistent with $T$. It is principal if there is a formula $\theta(\bar x)$ such that $T\cup\{\exists\bar x\,\theta\}$ is consistent and
$$
T\models\forall\bar x\,(\theta\to\psi)\qquad\text{for every }\psi\in p.
$$
For a <complete type>, this is exactly being an <isolated type>. Nonprincipal means that no such formula exists. A model omits $p$ if no tuple in that model satisfies every formula in $p$; different tuples may fail different members of the type. The model in the theorem need not omit each individual formula everywhere.
For parameter types, use the expanded language naming the parameters. Countability then applies to that expanded language, and hence requires a countable parameter set as well. There is no countability restriction in the finite-satisfiability argument of part (a).
Back to article page
