THE ATOMIC MODEL THEOREM AND TYPE OMITTING

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 other are equivalent to ACA(0) One, that every atomic theory has an atomic model, is not provable in RCA(0) but is incomparable with WKL0, more than Pi(1)(1) conservative RCA(0) and strictly weaker than all the combinatorial principles of Huschfeldt and Shore (2007) that are not Pi(1)(1) conservative over RCA(0). A priority argument 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 0 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 sot. 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, kind is thus ill a sense the weakest possible natural principle not. true in the omega-niodel consisting of the recursive sets.