Fix some countable theory $ T $. Let $ S_n $ be the space of complete $ n $-types over the empty set. A type $ p(x) \in S_n $ is said to be isolated if there is a formula $ \phi(x) $ (over the empty set) such that every element satisfying $ \phi(x) $ realizes $ p(x) $, and vice versa. Equivalently, $ p(x) $ is an isolated point in the stone topology on $ S_n $.

The countable omitting types theorem says that if $ Z $ is a countable set of non-isolated types (perhaps with varying $ n $), then there is a countable model of $ T $ in which no type in $ Z $ is realized. One proof proceeds by model-theoretic forcing (as described in Hodges' book Building Models by Games). If $ Z $ is finite, more elementary proofs exist. For example, one can take a model of $ T $, and begin building up a subset in which no type in $ Z $ is realized, using the Tarski-Vaught criterion as a guide to determine what to add to this set, to make the set eventually be a model.

The omitting types theorem provides one direction in the Ryll-Nardzewski theorem on countably categorical theories. Specifically, if $ T $ is a countable theory in which there is a non-isolated $ n $-type $ p $, then by the omitting types theorem, there is some countable model of $ T $ in which $ p $ is not realized. On the other hand, by compactness and Löwenheim-Skolem, there is a countable model in which $ p $ is realized. The two countable models just described cannot be isomorphic, so $ T $ is not countably categorical.