Local omission of a partial type
= Local omission of a partial type
A <first-order theory> locally omits a family $\Gamma(\mathbf x)$ if every formula $\theta(\mathbf x)$ consistent with it has a consistent refinement $\theta\land\neg\gamma$ for some $\gamma\in\Gamma$. Equivalently no consistent formula implies all of $\Gamma$. In a countable language the <omitting types theorem> converts this local condition into a countable model with no realization of the family.