Fix some countable theory . Let be the space of complete -types over the empty set. A type is said to be isolated if there is a formula (over the empty set) such that every element satisfying realizes , and vice versa. Equivalently, is an isolated point in the stone topology on .
The countable omitting types theorem says that if is a countable set of non-isolated types (perhaps with varying ), then there is a countable model of in which no type in is realized. One proof proceeds by model-theoretic forcing (as described in Hodges' book Building Models by Games). If is finite, more elementary proofs exist. For example, one can take a model of , and begin building up a subset in which no type in 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 is a countable theory in which there is a non-isolated -type , then by the omitting types theorem, there is some countable model of in which is not realized. On the other hand, by compactness and Löwenheim-Skolem, there is a countable model in which is realized. The two countable models just described cannot be isomorphic, so is not countably categorical. ::: ::: :::