The Atomic Model Theorem and Type Omitting
Status: published in the Transactions
of the American Mathematical
Society 361 (2009) 5805 - 5837.
version and preprint
Abstract. We investigate the complexity of several classical model
theoretic theorems about prime and atomic models and omitting types. Some
are provable in RCA0, others are equivalent to ACA0.
One, that every atomic theory has an atomic model, is not provable in
RCA0 but is incomparable with WKL0, more than
Π11 conservative over RCA0 and
strictly weaker than all the combinatorial principles of Hirschfeldt and
Shore  that are not Π11 conservative over
RCA0. A priority argument with Shore blocking shows that it is
also Π11-conservative over BΣ2.
We also provide a theorem provable by a finite injury priority argument
that is conservative over IΣ1 but implies
IΣ2 over BΣ2, and a type omitting
theorem that is equivalent to the principle that for every X there
is a set that is hyperimmune relative to X. Finally, we give a
version of the atomic model theorem that is equivalent to the principle
that for every X there is a set that is not recursive in X,
and is thus in a sense the weakest possible natural principle not true in
the omega-model consisting of the recursive sets.