= Solution
The <local omission of a partial type> $\Gamma(\mathbf x)$ by a consistent <first-order theory> $T$ means that, for every formula $\theta(\mathbf x)$ consistent with $T$, there is some $\gamma\in\Gamma$ such that
$$
T\cup\{\exists\mathbf x\,(\theta(\mathbf x)\land\neg\gamma(\mathbf x))\}
$$
is consistent. Equivalently, no formula consistent with $T$ implies every member of $\Gamma$. Thus every possible local condition has a compatible refinement excluding at least one proposed type formula.
The <omitting types theorem> states: in a countable first-order language, if $T$ is consistent and locally omits each of countably many finite-arity families $\Gamma_j$, then it has a countable model omitting them all. Omission means that no tuple satisfies every formula in the family. In the case of a <complete type>, local omission is equivalent to the type being nonisolated. Countability of the language and of the list of omission requirements is essential to this formulation.
Back to article page
