The atomic model theorem and type omitting
Denis R. Hirschfeldt, Richard A. Shore, Theodore A. Slaman · Transactions of the American Mathematical Society · 2009
We investigate the complexity of several classical model theoretic theorems about prime and atomic models and omitting types. Some are provable in RCA$_{0}$, and others are equivalent to ACA$_{0}$. One, that every atomic theory has an atomic model, is not provable in RCA$_{0}$ but is incomparable with WKL$_{0}$, more than $\Pi _{1}^{1}$ conservative over RCA$_{0}$ and strictly weaker than all the combinatorial principles of Hirschfeldt and Shore (2007) that are not $\Pi _{1}^{1}$ conservative over RCA$_{0}$. A priority argument with Shore blocking shows that it is also $\Pi _{1}^{1}$-conservative over B$\Sigma _{2}$. We also provide a theorem provable by a finite injury priority argument that is conservative over I$\Sigma _{1}$ but implies I$\Sigma _{2}$ over B$\Sigma _{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.