The countable omitting types theorem says that for a consistent theory in a countable language and countably many nonprincipal types of finite arities, there is a countable model omitting all those types. In particular a nonisolated complete type of can be omitted in a countable model.
Interpret “definable” here as without parameters. If parameters were allowed freely, every infinite structure would have infinitely many definable singleton sets, and the claimed implication would be false even for a dense linear order without endpoints.
Infinitely many distinct parameter-free definable subsets of imply infinitely many complete -types: if there were only such types, each formula would select a subset of those types, giving at most distinct definable subsets. There must also be a nonisolated complete type. To see this, suppose each complete type had an isolator . The family of their basic open sets covers the type space. Its compactness theorem gives a finite subcover, which would account for only finitely many complete types, a contradiction. Equivalently apply logical compactness theorem to .
A prime model admits an elementary embedding into every model of its complete theory. In the countable setting a prime model is atomic. If a tuple in the prime model had a nonisolated complete type, the omitting types theorem would give a model omitting that type; an elementary embedding of the prime model into it would realize the omitted type, a contradiction.
Combining the four parts, all positive implications are exactly those generated byThe structure refutes (ii)(i). The structure is a countable atomic and hence prime model of its complete theory, while failing both (i) and (ii); it refutes every remaining reverse arrow, including (iv)(i) and (iv)(ii). The counterexamples therefore cover all ordered pairs of distinct properties not forced by the boxed chain.
A partial type is a set of -first-order formulas in a fixed tuple jointly consistent with . A complete type, the usual meaning of an -type here, is maximal among such consistent sets: for each first-order formula it contains exactly one of .
Add new constants and considerEvery finite subset is satisfiable by consistency of the type. The compactness theorem gives a first-order model of the full set. Its -reduct is a first-order model of , and the interpretations of realize . This proof applies to partial as well as complete types.
For a complete theory in a countable language, the types realized in every first-order model are exactly the isolated types. An isolated type has a consistent first-order formula such that for every . Completeness forces , so every first-order model realizes ; the converse is the omitting types theorem. Countability is a hypothesis of that converse, not of the preceding compactness realization argument. For a partial type the corresponding criterion is an isolating consistent first-order formula, together with its existence in every first-order model; it need not itself belong to the partial type.
If is not complete, no one complete -type can be realized in every first-order model of : a complete type decides sentences, and two completions of disagree on some sentence. Thus the completeness and countability hypotheses must be retained when using the isolated-type characterization.