The Atomic Model Theorem and Type Omitting

• Published in: Transactions of the American Mathematical Society 2009-11, Vol.361 (11), p.5805-5837
• Main Authors: Hirschfeldt, Denis R., Shore, Richard A., Slaman, Theodore A.
• Format: Article
• Language: English
• Subjects: Arithmetic; Atomic theory; Atoms; Exact sciences and technology; Logic and foundations; Mathematical induction; Mathematical logic; Mathematical logic, foundations, set theory; Mathematical theorems; Mathematics; Model theory; Priority arguments; Recursion; Sciences and techniques of general use; Urelements
• ISSN: 0002-9947; 1088-6850
• DOI: 10.1090/S0002-9947-09-04847-8

We investigate the complexity of several classical model theoretic theorems about prime and atomic models and omitting types. Some are provable in RCA₀, and others are equivalent to ACA₀.One, that every atomic theory has an atomic model, is not provable in RCA₀ but is incomparable with WKL₀, more than $\pi _1^1 $ conservative over RCA₀ and strictly weaker than all the combinatorial principles of Hirschfeldt and Shore (2007) that are not $\pi _1^1 $ conservative over RCA₀.A priority argument with Shore blocking shows that it is also $\pi _1^1 $ -conservative over $B\sum _2 $ We also provide a theorem provable by a finite injury priority argument that is conservative over $I\sum _1 $ but implies $I\sum _2 $ over $B\sum _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 cj-model consisting of the recursive sets.