Omitting Types Theorem

The Omitting Types Theorem is a foundational result of model theory stating that, for a countable first-order language, if a complete type over a theory is not isolated by any single formula, then there is a countable model of the theory that omits that type entirely, meaning no element of the model realizes it. The theorem gives a precise condition for when a description of possible elements can be avoided altogether in some model, complementing the compactness theorem's guarantee that types can generally be realized, and it underlies later model-theoretic constructions such as atomic and prime models.