The Atomic Model Theorem and Type Omitting

Denis R. Hirschfeldt Department of Mathematics

University of Chicago Chicago IL 60637

Richard A. Shore Department of Mathematics Cornell University Ithaca NY 14853

Theodore A. Slaman Department of Mathematics University of California, Berkeley Berkeley CA 94720

June 11, 2008

Abstract

We investigate the complexity of several classical model theoretic theorems about prime and atomic models and omitting types. Some are provable in RCA_{0}, 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 Π_{1}^{1} conservative over RCA_{0} and strictly weaker than all the combinatorial principles of Hirschfeldt and Shore [2007] that are not Π_{1}^{1} conservative over RCA_{0}. A priority argument with Shore blocking shows that it is also Π_{1}^{1}-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 ω-model consisting of the recursive sets.

Hirschfeldt’s research was partially supported by NSF Grants DMS-0200465 and DMS-0500590.

Shore’s research was partially supported by NSF Grants DMS-0100035 and DMS-0554855.

Slaman’s research was partially supported by NSF Grants DMS-9988644 and DMS-0501167.

All the authors thank the Institute for Mathematical Sciences of the National University of Singapore for its generous support during the period July 18 – August 15, 2005, when part of this research was done.

1 Introduction

In this paper we investigate the complexity of a few classical model theoretic theorems about prime and atomic models and about omitting types in terms of both computational (recursion theoretic) and proof theoretic (reverse mathematical) calibrations and of the interplay between these approaches. The theorems of interest in such investigations are typically of the form ∀A (Θ(A) → ∃B Φ(A, B)) where Θ and Φ are arithmetic and A, B ∈ 2^{ℕ}. Thus, from the recursion theoretic point of view, we want to bound or characterize the computational complexity of B given an A satisfying Θ (typically in terms of Turing degree or place in one of the standard arithmetic/analytic definability or jump hierarchies). From the reverse mathematics point of view we want to determine the axiom systems in which the theorem is provable (typically subsystems of second order arithmetic determined by the amount of comprehension assumed). Here, characterizations correspond to reversals in the sense that one proves (over some weak system) the axioms of one of the subsystems of second order arithmetic from the statements of the mathematical theorems being investigated.

We briefly review the five standard systems of reverse mathematics. For completeness, we include systems stronger than arithmetical comprehension, but these will play no part in this paper. Details, general background, and results, as well as many examples of reversals, can be found in Simpson [1999], the standard text on reverse mathematics. Each of the systems is given in the language of second order arithmetic, that is, the usual first order language of arithmetic augmented by set variables and the membership relation ∈. Each contains the standard basic axioms for +, ·, and < (which say that ℕ is an ordered semiring). In addition, they all include a form of induction that applies only to sets (that happen to exist):

(I_{0}) (0 ∈ X ∧ ∀n (n ∈ X → n + 1 ∈ X)) → ∀n (n ∈ X).

We call the system consisting of I_{0} and the basic axioms of ordered semirings P_{0}. All the five standard systems are defined by adding various types of set existence axioms to P_{0}. They also correspond to classical construction principles in recursion theory.

(RCA_{0}) Recursive Comprehension Axioms: This is a system just strong enough to prove the existence of the recursive sets but not of 0′ nor indeed of any nonrecursive set. In addition to P_{0} its axioms include the schemes of Δ_{1}^{0} comprehension and Σ_{1}^{0} induction:

(Δ_{1}^{0}-CA_{0}) ∀n (φ(n) ↔ ψ(n)) → ∃X ∀n (n ∈ X ↔ φ(n)) for all Σ_{1}^{0} formulas φ and Π_{1}^{0} formulas ψ in which X is not free.

(IΣ_{1}) (φ(0) ∧ ∀n (φ(n) → φ(n + 1))) → ∀n φ(n) for all Σ_{1}^{0} formulas φ.

The next system says that every infinite binary tree has an infinite path. It is connected to the Low Basis Theorem (Jockusch and Soare [1972]) of recursion theory, which says that every such tree has an infinite path whose jump is recursive in that of the tree itself.

(WKL_{0}) Weak König’s Lemma: This system consists of RCA_{0} plus the statement that every infinite subtree of 2^{<ℕ} has an infinite path.

We next move up to arithmetic comprehension.

(ACA_{0}) Arithmetic Comprehension Axioms: This system consists of RCA_{0} plus the axioms ∃X ∀n (n ∈ X ↔ φ(n)) for every arithmetic formula φ in which X is not free.

In recursion theoretic terms, ACA_{0} proves the existence of 0′ and, by relativization, it proves, and in fact is equivalent to, the existence of X′ for every set X.

The next system corresponds to the existence of all (relativized) H-sets, i.e. the existence, for every set X, of the H_{e}^{X} (and so the hyperarithmetic hierarchy up to e) for each e ∈ O^{X}, the hyperjump of X. It says that arithmetic comprehension can be iterated along any countable well order.

(ATR_{0}) Arithmetical Transfinite Recursion: This system consists of RCA_{0} plus the following axiom. If X is a set coding a well order <_{X} with domain D and Y is a code for a set of arithmetic formulas φ_{x}(z, Z) (indexed by x ∈ D) each with one free set variable and one free number variable, then there is a sequence ⟨K_{x} | x ∈ D⟩ of sets such that if y is the immediate successor of x in <_{X}, then ∀n (n ∈ K_{y} ↔ φ_{x}(n, K_{x})), and if x is a limit point in <_{X}, then K_{x} is ⨁{K_{y} | y <_{X} x}.

The systems climbing up to full second order arithmetic (i.e. comprehension for all formulas) are classified by the syntactic level of the second order formulas for which we assume a comprehension axiom.

(Π_{n}^{1}-CA_{0}) Π_{n}^{1} Comprehension Axioms: ∃X ∀k (k ∈ X ↔ φ(k)) for every Π_{n}^{1} formula φ in which X is not free.

The recursion theoretic equivalent of the simplest of these systems, Π_{1}^{1}-CA_{0}, is the existence of O^{X} for every set X. Together with the four systems listed above, this system makes up the standard list of the axiomatic systems of reverse mathematics. Almost all theorems of classical mathematics whose proof theoretic complexities have been determined have turned out to be equivalent to one of them.

Below, we will also consider induction and bounding principles. In the definition of IΣ_{1} above, if we replace Σ_{1}^{0} formulas by Σ_{k}^{0} or Π_{k}^{0} formulas, we obtain the principles IΣ_{k} and IΠ_{k}, respectively. The principles IΣ_{k} and IΠ_{k} are equivalent over RCA_{0} (see Exercise II.3.12 in Simpson [1999]). The Σ_{k} bounding principle is defined as follows.

(BΣ_{k}) (∀i < n)(∃x)φ(x) → (∃u)(∀i < n)(∃x < u)φ(x) for all Σ_{k}^{0} formulas φ.

Over RCA_{0}, the principle BΣ_{k} is strictly between IΣ_{k−1} and IΣ_{k} (Paris and Kirby [1978]; see also Hájek and Pudlák [1998]).

The early connections between recursion theoretic ideas and methods on the one hand and reverse mathematics in the other typically involved recursive mathematics, diagonalization or finite injury arguments, and coding. Consider, for example, a theorem of the form ∀A (Θ(A) → ∃B Φ(A, B)) where Θ and Φ are arithmetic. We call B a solution for the instance of the theorem specified by A if Θ(A) → Φ(A, B).

A construction of recursive mathematics that shows that there is a solution B recursive in any given A generally shows that the theorem is provable in RCA_{0}. One that shows that B can be obtained arithmetically in A usually shows that the theorem is provable in ACA_{0}. Standard forms of applications of recursion theoretic diagonalization or finite injury results to reverse mathematical calibrations are as follows:

1. If there is no solution B recursive in some given A then the theorem is not provable in RCA_{0}.

2. If there is no solution B that is low over A, i.e. (B ⊕ A)′ ≡_{T} A′, then the theorem is not provable in WKL_{0}.

3. If there is no solution B arithmetic in A then the theorem is not provable in ACA_{0}.

Coding methods tend to give reversals.

1. If, for any recursive tree T, there is a recursive instance of the theorem such that any solution codes a path through T then the theorem usually implies WKL_{0}.

2. If there is a recursive instance of the theorem such that any solution computes 0′ then the theorem usually implies ACA_{0}.

3. If there is a recursive instance of the theorem such that any solution computes O then the theorem usually implies Π_{1}^{1}-CA_{0}.

In this paper we will analyze several theorems that fall into this standard classification scheme and some that fall well outside it. We are also particularly interested in reverse mathematical relationships derived from more complex recursion theoretic results and constructions.

In this paper all theories T in a language L are deductively closed (T ⊢ φ ⇒ φ ∈ T), complete (T ⊢ φ or T ⊢ ¬φ for every sentence φ of L) and consistent (there is no formula φ such that T ⊢ φ and T ⊢ ¬φ). All languages and models are countable. For the purposes of reverse mathematics, we include with a model A of T the function interpreting terms and the full satisfaction predicate for formulas with constants from the model. Formal definitions suitable for work in RCA_{0} can be found in Simpson [1999, Section II.8] along with, for example, a proof in RCA_{0} that any complete consistent theory has a model in this sense.

Definition 1.1. A partial type of a theory T is a set of formulas in a fixed number of free variables that is consistent with T. We will reserve the unmodified term type for complete types, i.e., maximal partial types. A partial type Γ is realized in a model A of T if there is an a⃗ such that A ⊨ φ(a⃗) for every φ ∈ Γ. Otherwise, Γ is omitted in A.

A formula φ(x_{1}, …, x_{n}) of T is an atom of T if for each formula ψ(x_{1}, …, x_{n}) we have T ⊢ φ → ψ or T ⊢ φ → ¬ψ but not both. A partial type Γ is principal if there is a formula φ consistent with T such that T ⊢ φ → ψ for all ψ ∈ Γ. Thus a complete type is principal if and only if it contains an atom of T.

The theory T is atomic if, for every formula ψ(x_{1}, …, x_{n}) consistent with T, there is an atom φ(x_{1}, …, x_{n}) of T extending it, i.e. one such that T ⊢ φ → ψ. A model A of T is atomic if every n-tuple from A satisfies an atom of T, that is, every type realized in A is principal. The model A is prime if it can be elementarily embedded in every model of T.

The standard classical theorems about these notions (as in e.g. Chang and Keisler [1977, 2.3]) are as follows:

1. AMT (Existence): T has an atomic model iff T is atomic.

2. AUniqueness: If A and B are atomic models of T then A ≅ B.

3. PMT (Existence): T has a prime model iff T is atomic.

4. PUniqueness: If A and B are prime models of T then A ≅ B.

5. Equivalence: A model of T is atomic iff it is prime.

Counting each biconditional as two implications, this list provides eight implications to analyze in terms of reverse mathematics. Three are easily seen in §2 to be provable in RCA_{0} (the “only if” directions of AMT (1) and PMT (3) and the “if” direction of Equivalence (5)). We prove in §2 as well that three others are equivalent to ACA_{0} (AUniqueness (2); the “only if” direction of PMT (3) and the “only if” direction of Equivalence (5)). Of the remaining two, the implication PUniqueness (4) is easily provable in ACA_{0} but its status in terms of reversals or connections to other systems remains completely open. Thus, when we refer below to principles considered in this paper, we always exclude PUniqueness. It is the “if” direction of AMT (1), which we call simply AMT, that turns out to be quite interesting.

(AMT) Atomic Model Theorem: Every complete atomic theory has an atomic model.

AMT is an exceptionally weak principle but nonetheless not provable in RCA_{0} or even WKL_{0}, as we will show below in Corollary 3.4. It turns out to be strictly weaker than most of the combinatorial principles studied in Hirschfeldt and Shore [2007] (hereafter [HS]), which were themselves shown to be weaker than the classical Ramsey’s Theorem for pairs that has long been of interest both recursion theoretically and in reverse mathematics. We refer to Cholak, Jockusch and Slaman [2001] (hereafter [CJS]) for the best analysis of Ramsey’s Theorem itself.

Our general analysis and, in particular, our proof that AMT is implied by the weakest of these combinatorial principles (SADS, as defined below) are related to various forcing constructions and priority arguments. Some of them supply more general conservation results; others touch on the issue of the role of BΣ_{2} and IΣ_{2} in (reverse) recursion theory. In particular, AMT is shown to be conservative over not only RCA_{0} (IΣ_{1}) and IΣ_{2} but over BΣ_{2} as well. This last argument uses a finite injury argument with Shore blocking to carry out the relevant construction in BΣ_{2}. (We know of only two other examples of principles that are known to be conservative over BΣ_{2}: WKL_{0} by Hájek [1993] and COH by Chong, Slaman and Yang [ta].) On the other hand, we are lead in §4 to a single statement about the existence of certain types of generics (a bit less than weakly 2generics) that can be proven by a finite injury priority argument and that is conservative over both IΣ_{1} and IΣ_{2} but not over BΣ_{2}, as it implies IΣ_{2} over BΣ_{2}. This seems to be the first example of such a theorem.

The existence of atomic models can be seen not only as a forcing/genericity construction but also (as is traditional in model theory) as a type omitting argument. In §5, we investigate the strength of another type omitting argument and show that it is equivalent (both recursion theoretically and in the sense of reverse mathematics) to the existence of hyperimmune sets. In §6, we give a weaker version of AMT that is equivalent to the existence of nonrecursive sets, and is thus in a sense the weakest possible natural principle not true in the ω-model consisting of the recursive sets. (An ω-model of a fragment of second order arithmetic is one whose first order part is standard, and hence is determined entirely by which subsets of ω it contains.)

To set the stage for our eventual analysis of AMT we define here many of the principles studied in [CJS] and [HS] and summarize the relationships among them in Diagram 1 below. (Single arrows are implications; double arrows are strict implications and negated arrows represent known nonimplications. See [HS] for attributions and references.) Each principle is to be understood as an addition to RCA_{0}.

Definition 1.2. An n-coloring (partition) of [ℕ]^{k}, the unordered k-tuples (n_{1}, …, n_{k}) of natural numbers (listed by convention in increasing order), is a map f : [ℕ]^{k} → n. A subset H of ℕ is homogeneous for the coloring f if H is infinite and |f“[H]^{k}| = 1 (i.e. all tuples from H have the same color). Unless otherwise stated all colorings will be 2-colorings of [ℕ]^{2}.

(RT_{2}^{2}) Ramsey’s Theorem for pairs: Every 2-coloring of [ℕ]^{2} has a homogeneous set.

Definition 1.3. A coloring f of [ℕ]^{2} is stable if (∀x)(∃y)(∀z > y)[f(x, y) = f(x, z)].

(SRT_{2}^{2}) Stable Ramsey’s Theorem for pairs: Every stable 2-coloring of [ℕ]^{2} has a homogeneous set.

Definition 1.4. If R⃗ = ⟨R_{i} | i ∈ ℕ⟩ is a sequence of sets, an infinite set S is R⃗-cohesive if (∀i)(∃s)[(∀j > s)(j ∈ S → j ∈ R_{i}) ∨ (∀j > s)(j ∈ S → j ∉ R_{i})].

(COH) Cohesive Principle: For every sequence R⃗ = ⟨R_{i} | i ∈ ℕ⟩ there is an R⃗- cohesive set.

We will denote the nth partial recursive in A function (in some standard effective listing) by Φ_{n}^{A}.

(DNR) Diagonally Nonrecursive Principle: For every set A there is a function f that is diagonally nonrecursive relative to A, i.e. ∀n¬(f(n) = Φ_{n}^{A}(n)).

(CAC) Chain-AntiChain Principle: Every infinite partial order (P, ⩽_{P}) has an infinite subset S that is either a chain, i.e. (∀x, y ∈ S)(x ⩽_{P} y ∨ y ⩽_{P} x), or an antichain, i.e. (∀x, y ∈ S)(x ⩽̸_{P} y ∧ y ⩽̸_{P} x).

Definition 1.5 (RCA_{0}). An infinite linear order (L, ⩽_{L}) in which all nonfirst elements have immediate predecessors and all nonlast ones have immediate successors has type

• ω if every element has finitely many predecessors;

• ω^{∗} if every element has finitely many successors;

• ω + ω^{∗} if it does not have type ω or ω^{∗} and every element has either finitely many predecessors or finitely many successors.

(ADS) Ascending or Descending Sequence: Every infinite linear order (L, ⩽_{L}) has an infinite subset S that is either an ascending sequence, i.e. (∀s < t)(s, t ∈ S → s <_{L} t), and so of order type ω, or a descending sequence, i.e. (∀s < t)(s, t ∈ S → t <_{L} s), and so of order type ω^{∗}.

(SADS) Stable ADS: Every linear order of type ω + ω^{∗} has a subset of order type ω or ω^{∗}.

(CADS) Cohesive ADS: Every linear order has a subset S of order type ω, ω^{∗}, or ω + ω^{∗}.

Definition 1.6. A partial order P is stable if either

(∀i ∈ P)(∃s)[(∀j > s)(j ∈ P → i <_{P} j) ∨ (∀j > s)(j ∈ P → i |_{P} j)]

or

(∀i ∈ P)(∃s)[(∀j > s)(j ∈ P → i >_{P} j) ∨ (∀j > s)(j ∈ P → i |_{P} j)].

(SCAC) Stable CAC: Every infinite stable partial order has an infinite chain or antichain.

[figure: RT_{2}^{2}; _{SRT2 2}; DNR; CAC; |; _{WKL_{0}}; |; COH; SCAC; |; ADS; COH; COH + WKL_{0}; |; SADS; CADS; _{RCA_{0}}]

Diagram 1

2 Within RCA_{0}, ACA_{0} and Reversals

We begin with the two facts provable in RCA_{0}. The first is the “only if” direction of AMT (1) and requires simply the classical proof.

Proposition 2.1 (RCA_{0}). If T has an atomic model, T is atomic.

Proof. Let A be an atomic model of T. Consider any formula ψ(x_{1}, …, x_{n}) consistent with T. As T is complete, T ⊢ ∃x_{1}, …, x_{n}ψ(x_{1}, …, x_{n}) and so there are c_{1}, …, c_{n} in A such that A ⊨ ψ(c_{1}, …, c_{n}). As A is atomic there is an atom φ(x_{1}, …, x_{n}) of T such that A ⊨ φ(c_{1}, …, c_{n}). Thus φ(x_{1}, …, x_{n}) is the required atom of T extending ψ.

The second is the “if” direction of Equivalence (5) and uses the effective version of the omitting types theorem in the classical proof.

Proposition 2.2 (RCA_{0}). Every prime model A of T is atomic.

Proof. Consider any n-tuple c_{1}, …, c_{n} of A and the set S of formulas it satisfies, S = {ψ(x_{1}, …, x_{n}) | A ⊨ ψ(c_{1}, …, c_{n})}. We wish to show that S contains an atom of T. If not, the classical omitting types theorem says that there is a model B of T that fails to realize S, i.e. there are no elements d_{1}, …, d_{n} of B such that S = {ψ(x_{1}, …, x_{n}) | B ⊨ ψ(d_{1}, …, d_{n})}. In this situation there could not be an elementary embedding of A into B, for the desired contradiction. Thus we need only verify in RCA_{0} that there is such a model B. The usual effective version of the Henkin construction for the omitting types theorem, as for example in Harizanov [1998, 6.1], provides in RCA_{0} a complete consistent set of sentences in the language with Henkin constants in which every n-tuple d_{1}, …, d_{n} satisfies ¬ψ(d_{1}, …, d_{n}) for some ψ(d_{1}, …, d_{n}) ∈ S. Simpson [1999, II.8.6] then constructs the required model in RCA_{0}.

These two Propositions together obviously supply the proof in RCA_{0} of the “only if” direction of PMT (3). We now prove that three other of the eight basic implications are equivalent to ACA_{0}.

Theorem 2.3. The following assertions are equivalent (over RCA_{0}):

1. ACA_{0}.

2. Every atomic model of T is prime.

3. AUniqueness.

4. Every atomic theory T has a prime model.

Proof. The classical proofs of assertions (2)–(4) can be easily carried out in ACA_{0}. We construct a theory T that will establish all the implications in the other direction. The language of T has unary predicates R_{i} and R_{i,j} for i, j ∈ ℕ. The theory T is the deductive closure of the following set S of axioms.

Axioms for T:

1. Axioms asserting that the R_{i} define infinite, pairwise disjoint sets.

2. R_{i,s}(x) → R_{i}(x) for every i, s ∈ ℕ.

3. R_{i,s}(x) → R_{i,s+1}(x).

4. If Φ_{i}(i) does not converge in fewer than s many steps then the axiom ¬R_{i,s}(x) is included.

5. If Φ_{i}(i) converges in exactly s many steps then there are axioms asserting that there are infinitely many x such that R_{i,s}(x) and infinitely many x such that ¬R_{i,s}(x).

6. If Φ(i) converges in exactly s many steps then the axioms ¬R_{i,s}(x) → ¬R_{i,t}(x) are included for every t > s.

This set S of axioms is clearly recursive and so provably exists in RCA_{0}. We claim that S admits quantifier elimination, i.e. for every formula ψ(x̄) there is a quantifier free φ(x̄) (possibly just the formal propositional symbols T, for true, or F, for false) with the same free variables such that S ⊢ φ(x̄) ↔ ψ(x̄). This claim implies that S is complete, as any sentence is equivalent to T or F modulo S, and so its deductive closure is Δ_{1} definable and provably exists in RCA_{0}. This closure is our desired theory T.

To see that S admits quantifier elimination it suffices to present a recursive procedure that finds a quantifier free equivalent φ(x̄) for a given existential formula ∃ȳφ(x̄, ȳ) as one can then carry out the usual induction (for the provable, in S, equivalence of the resulting formulas) in RCA_{0} by IΣ_{1}. By the usual applications of DeMorgan’s laws and the distribution of ∃ over ∨, we may assume φ is a conjunction of atomic formulas and negations of atomic formulas. As the language has only unary predicates the only atomic formulas are of the form R_{i}(z) or R_{i,s}(z) for z ∈ x̄ȳ.

We begin with the following simple consistency checks. If any of them fail, the formula is inconsistent with S and its equivalent is F.

Consistency Checks:

1. Is φ propositionally consistent, i.e. is there no occurrence of both R(z) and ¬R(z) for any relation R and variable z?

2. Is φ consistent with Axiom 1, i.e. does it not contain, for any z and i ≠ j, both R_{i}(z) and R_{j}(z)?

3. Is φ consistent with Axiom 2, i.e. if it contains some R_{i,s}(z) then does it not contain ¬R_{i}(z)?

4. Is φ consistent with Axiom 3, i.e. if it contains some R_{i,s}(z) then does it not contain ¬R_{i,t}(z) for any t > s?

5. Is φ consistent with Axiom 4, i.e. if Φ_{i}(i) does not converge in fewer than s many steps, then does R_{i,s}(z) not occur in φ?

6. Is φ consistent with Axiom 6, i.e. if ¬R_{i,s}(z) and R_{i,t}(z) occur in φ with s < t then does Φ_{i}(i) converge in exactly n steps with s < n ⩽ t?

If φ passes all these tests then the required equivalent to ∃ȳφ(x̄, ȳ) is gotten by replacing all the atomic and negated atomic conjuncts about any z ∈ ȳ with T. It is straightforward to see that the result is equivalent to ∃ȳφ(x̄, ȳ) modulo S. Thus S is complete as any sentence is equivalent to T or F modulo S.

We now determine the atoms of T. As the language has only unary predicates, the formulas satisfied by an n-tuple are determined by the ones satisfied by the individual elements of the tuple. Thus it suffices to determine the quantifier free formulas with one free variable x that decide all atomic formulas about x. If Φ_{i}(i) is divergent then R_{i}(x) is such a formula since it implies ¬R_{i,s}(x) for every s and also ¬R_{j}(x) and ¬R_{j,t}(x) for every j ≠ i and every t. If Φ_{i}(i) is convergent and converges in exactly s many steps then R_{i,s}(x) and ¬R_{i,s}(x) ∧ R_{i}(x) are such formulas. The first implies R_{i}(x), implies R_{i,t}(x) for every t > s and ¬R_{i,t}(x) for every t < s and implies ¬R_{j}(x) and ¬R_{j,t}(x) for every j ≠ i and every t. The second one implies ¬R_{i,t}(x) for every t and also ¬R_{j}(x) and ¬R_{j,t}(x) for every j ≠ i and every t. In any model A of T any element that satisfies some R_{i} satisfies one of these atoms. Thus any model in which every element is in some R_{i} is atomic.

Finally, we claim that T is atomic. Again we need to consider only quantifier free formulas φ(x) with one free variable, which we can take to be a conjunct of atomic formulas about x and negations of such formulas. (If we can extend all such consistent formulas to atoms, we can extend any consistent disjunction of them to an atom and so any formula to an atom as required.) If φ fails one of the above consistency checks it is inconsistent with T and so of no concern. Otherwise, if it contains some R_{i}(x) or R_{i,s}(x) as a conjunct then we can obviously extend it to one of the atoms described above. Otherwise, it contains only negated atomic formulas. In this case the atom R_{i}(x) extends φ for any i larger than all j such that R_{j} or any R_{j,t} appears in φ and Φ_{j}(j) is divergent.

To deduce ACA_{0} from each of assertions (2)–(4) of the theorem, we build two atomic models A, B of T such that if there is a model C with embeddings into both A and B then 0′ is recursive in C and the embeddings.

The domains of both A and B are ℕ and in each the interpretation of R_{i} is {⟨i, n⟩ | n ∈ ℕ}. To define R_{i,s} first see whether Φ_{i}(i) is convergent in at most s steps. If not, then R_{i,s} is empty. If so, say it converges at step t ⩽ s. In A we put {i} × [0, t] ⊆ R_{i,t}, split the rest of i × ℕ into two recursive infinite pieces, and put one into R_{i,t} and the other into ¬R_{i,t}. In B we put {i} × [0, t] ⊆ ¬R_{i,t} and then also split the rest of i × ℕ into two recursive infinite pieces and put one into R_{i,t} and the other into ¬R_{i,t}. Clearly A and B are recursive models of T and so provably exist in RCA_{0}.

Suppose now that C is also a model of T and there are embeddings f : C → A and g : C → B. We claim that we can compute 0′ from these models and embeddings, i.e. that it is Δ_{1} in them and so provably exists in RCA_{0}. Given i we find a c ∈ C such that C ⊨ R_{i}(c). (One exists by our first axioms for T.) We then get f(c). If Φ_{i}(i) converges in at most f(c) many steps then, of course, i ∈ 0′. If not, we get g(c). Again if Φ_{i}(i) converges in at most g(c) many steps then, of course, i ∈ 0′. If not, then we claim that Φ_{i}(i) diverges and so i ∉ 0′. Otherwise, by our assumptions, Φ_{i}(i) converges in exactly t many steps for some t > f(c). Thus by our construction of A, we have {i} × [0, t] ⊆ R_{i,t}^{A} and so, in particular, A ⊨ R_{i,t}(⟨i, f(c)⟩). As f and g are embeddings, B ⊨ R_{i,t}(⟨i, g(c)⟩) and so by the construction of B, we have g(c) > t for the desired contradiction.

Finally, we argue that each assertion (2)–(4) of the theorem provides a model C of T and embeddings into both A and B. For (2), note that A is atomic and so prime by (2). Thus there is an embedding of A into B, and A itself fulfills the requirements on C. Similarly, assuming (3) there is an isomorphism between A and B, and so either will fulfill the requirements on C. As for (4), we have shown that T is atomic and so (4) implies that it has a prime model C which by definition is embeddable into both A and B as required.

Of course, by Theorems 2.2 and 2.3(3), ACA_{0} ⊢ PUniqueness, but the reversal is open. We now turn to the remaining implication AMT and its relation to other principles.

3 AMT: Nonimplications

The reverse mathematically most interesting theorem of our group on prime and atomic models is (the existence part of) AMT, that every atomic theory has an atomic model. Along with those studied in [HS], it is another example of a mathematical existence theorem weaker than ACA_{0} and incomparable with WKL_{0}. We begin our analysis by using some of the recursion theoretic results of Csima, Hirschfeldt, Knight and Soare [2004] (hereafter [CHKS]), Csima [2004], [HS] and others to draw reverse mathematical conclusions of the form that AMT does not imply various other principles.

Theorem 3.1 (Csima [2004]). Every atomic decidable T (i.e. the set of sentences in T is recursive) has an atomic prime model A with a low complete diagram, i.e. if D is the set of sentences in the language of T with constants added for each element of A true in A, then D′ ≡_{T} 0′.

Definition 3.2 ([CHKS]). A degree a is prime bounding if every decidable atomic T has an atomic model recursive in a, i.e. its atomic diagram is recursive in a.

Theorem 3.3 ([CHKS]). A degree a ⩽ 0′ is prime bounding iff a ∈ L̄_{2}, i.e. a′′ > 0′′.

Corollary 3.4. WKL_{0} ⊬ AMT.

Proof. Essentially by the low basis theorem (Jockusch and Soare [1972]) as shown in Simpson [1999, proof of Theorem VIII.2.17], there is a low degree d, i.e. d′ = 0′, bounding a standard model M of WKL_{0}, i.e. every set in M is recursive in d. On the other hand, Theorem 3.3 says that no low degree can bound a standard model of AMT.

We now want to combine and slightly improve the two previous theorems to get the reverse nonimplication. As we will need the notion of the tree of Henkin constructions of models of a theory for this and later proofs, we first make it precise with the following definition.

Definition 3.5 (RCA_{0}). Let T be a (complete, consistent, deductively closed) theory in a language L. Let L′ be the extension of L gotten by adding on countably many new (Henkin) constants c_{i} and φ_{i} be an enumeration of all the sentences of L′. The tree F of all possible standard Henkin constructions of models of T is defined by recursion. Each node σ ∈ 2^{ℕ} in F will also be labeled by a set S_{σ} of sentences of L′ consistent with T associated with it. We begin by putting ∅ into F and setting S_{∅} = ∅. If σ ∈ F and |σ| = n, we ask whether S_{σ} ∪ {φ_{n}} is consistent with T. If so, we put σˆ 1 into F. If φ_{n} is of the form ∃xψ(x) we choose the least i such that c_{i} does not appear in S_{σ} and let S_{σˆ 1} = S_{σ} ∪ {φ_{n}, ψ(c_{i})}; otherwise S_{σˆ 1} = S_{σ} ∪ {φ_{n}}. If ¬φ_{n} is consistent with T, we put σˆ 0 into F and let S_{σˆ 0} = S_{σ} ∪ {¬φ_{n}}.

Remark 3.6. Even in RCA_{0}, the usual arguments show that at least one of φ and ¬φ must be consistent with T ∪ S_{σ} and if σˆ i ∈ F, then S_{σˆ i} is consistent with T. If P is any (infinite) path through F, then S_{P} = T ∪ {S_{σ} | σ ∈ P } is consistent and recursively defines a model M_{P} of T (in RCA_{0}) by the usual Henkin argument. (The elements are the c_{i} for i least such that there is some c_{j} with c_{i} = c_{j} ∈ S_{P}. The functions and relations are defined in the standard fashion.) The recursion theoretic version of this fact is that the tree F is recursive in T and each M_{P} is recursive in T ⊕ P. This consideration gives rise to a tree S (with the same nodes as F) labeled with D_{σ}, subsets of the complete diagrams of Henkin models of T. Of course, F and S trivially have infinitely many splits along every path (determined by various constants being equal or not if by nothing else). Thus if T is decidable (recursive), F and S are recursively isomorphic to the full binary tree 2^{<ℕ}.

Proposition 3.7. If T is atomic and decidable and a ∉ GL_{2}, i.e. (a ∨ 0′)′ < a′′, then T has an atomic model B with complete diagram of degree b ⩽ a with b ∈ GL_{1}, i.e. b ∨ 0′ = b′.

Proof. As T is decidable, the tree F of all possible standard Henkin constructions of models of T and the associated tree S of Henkin models of T are recursive and recursively isomorphic to 2^{<ℕ}. As always, the sets of nodes that decide each membership question of the jump of the model (given that it lies on S) are dense. Any path through S that meets each of these dense sets is in GL_{1}. (To decide whether e is in the jump just find a node σ such that either Φ_{e}^{D_{σ}}(e) is convergent or σ has no extension τ (on F) with Φ_{e}^{D_{τ}} (e) convergent.) As T is atomic, the set of nodes that make a given n-tuple c_{1}, …, c_{n} of Henkin constants satisfy an atom is also dense. (At any node there is some formula ψ(x_{1}, …, x_{n}) that contains all the facts determined so far about c_{1}, …, c_{n}. By atomicity of T, that formula ψ(x_{1}, …, x_{n}) can be extended to an atom φ(x_{1}, …, x_{n}). One then simply finds an extension of the given node on S whose label includes the formula φ(c_{1}, …, c_{n}).) Thus all we need to do is to produce a path through S that is recursive in a and meets all these dense sets of conditions. The corresponding Henkin model of T is then atomic and its complete theory is recursive in a and in GL_{1} as required.

The crucial point is that the function going from one of these dense sets and a node σ to an extension τ in the dense set is uniformly recursive in 0′. (For deciding the jump this is standard. For atomicity, just note that being an atom is a Π_{1} property of a formula.) We combine these operations into a single function f recursive in 0′ for which we can use the hypothesis that a ∉ GL_{2}. We define a function f recursive in 0′ by recursion. Given f(n), we let f(n + 1) be the least m > f(n) such that

1. every σ of length at most f(n) that has any extension τ on S such that Φ_{e}^{D_{τ}} (e) ↓ for any e ⩽ n has one at level m and

2. for every tuple ā of Henkin constants with code below f(n) and every σ on S of length at most f(n),

(a) σ has an extension τ on F of length less than m whose label has a formula isolating the type of ā and

(b) letting τ be such an extension of shortest length, for every ρ ⊇ σ such that |ρ| ⩽ |τ|, if ρ does not have a formula isolating the type of ā then ρ has a split in the type of ā (as given by D_{ρ}) appearing on (the labels of) S below level m.

Now as a ∉ GL_{2}, there is a g recursive in a that is strictly increasing and not dominated by f (see Lerman [1983, Corollary IV.3.4]).

We now construct a path through S recursive in g that meets all the specified dense sets. Inductively assume that at stage n we have σ on S of length at most min{f(n), g(n)}. We find the least e or ā below n (in a priority ordering where we order e before the tuple ā with code e) such that

1. Φ_{e}^{D_{σ}}(e) diverges but Φ_{e}^{D_{τ}} (e) converges for some τ ⊇ σ of length at most g(n + 1) or

2. there is a split in the type of ā above σ below level g(n + 1) in S, but for some τ ⊇ σ of length less than g(n + 1) there is no split of the type of ā in S above τ below level g(n + 1).

Choose a τ of minimal length satisfying the required condition for this least requirement. Let the (n + 1)^{st} step in constructing our desired path be τ. Note that we maintain our inductive hypothesis in that |τ| ⩽ f(n + 1), g(n + 1). The point here is that τ is by construction of length less than g(n + 1) and if f(n + 1) ⩽ g(n + 1) then it is of length less than f(n + 1) by the definition of f and our inductive hypothesis that |σ| < f(n).

Now we argue that every requirement is satisfied. Say deciding Φ_{e}^{M}(e) is the least one not satisfied and all higher priority ones have been satisfied by node ρ constructed at stage k. At some n > k we are at a node σ of length at most min{f(n), g(n)} and g(n + 1) > f(n + 1). If there is any extension τ of σ such that Φ_{e}^{D_{τ}} (e) ↓ then there is one of length at most f(n + 1) < g(n + 1) and so we find it at stage n and take the first one as the next element of our path and satisfy this requirement. Otherwise, there is no such extension and we also decide the jump at e as required.

If ā is the least tuple with a nonatomic type in the model we built again choose an n > ā such that g(n + 1) > f(n + 1) and all higher priority requirements have been satisfied by the node σ of length at most min{f(n), g(n)} produced at stage n (i.e. all Φ_{e}^{D_{σ}}(e) have been decided and all b̄ < ā have had their types isolated by σ). At stage n + 1 our computation sees that σ does not isolate the type of ā (by our assumption that it is not isolated in our model and the definition of f). If we search for a τ ⊇ σ that has no extensions splitting the type of ā in the labels below level g(n + 1), the one of shortest length that we find actually isolates the type of ā by the definition of f. We choose one such as the next node on our tree.

Corollary 3.8. Every degree a ∉ GL_{2} is prime bounding and, in fact, bounds a standard model of AMT all of whose sets are recursive in sets below a which are also in GL_{1}.

Proof. Given any a ∉ GL_{2} we can build a standard model of AMT bounded by a by iterating Proposition 3.7 to dovetail and produce a class of sets closed under AMT (i.e. for any atomic theory in the class there is an atomic model in the class) with each member of the class recursive in a and indeed recursive in some GL_{1} degree below a. To be more precise, we construct three sequences T_{i}, A_{i} and b_{i} such that for each i, we have T_{i} ⩽_{T} b_{i} ⩽ b_{i+1} ⩽ a and b_{i} ∈ GL_{1}, so that every complete atomic theory recursive in any b_{j} occurs as some T_{k} and A_{k} is an atomic model of T_{k} whose complete diagram is recursive in b_{k+1}. Say we have T_{i} ⩽_{T} b_{i} ∈ GL_{1} and b_{i} ⩽ a. Since b_{i} ∈ GL_{1}, we have (a ∨ b′_{i})′ = (a ∨ (b_{i}∨0′))′. As b_{i} ⩽ a, we have (a ∨ (b_{i}∨0′))′ = (a ∨ 0′)′. As a ∉ GL_{2}, we have (a ∨ 0′)′ < a′′. Thus (a ∨ b′_{i})′ < a′′, so a ∉ GL_{2}^{b_{i}}. By Proposition 3.7 (relativized to b_{i}) we can get an atomic model A_{i} of T_{i} with its complete diagram recursive in a and GL_{1}^{b_{i}}. We let b_{i+1} be the degree of A_{i} and note that it is in GL_{1} as b′_{i+1} = (b_{i+1} ∨ b′_{i}) = (b_{i+1} ∨ b_{i} ∨ 0′) = b_{i+1} ∨ 0′ as required.

Corollary 3.9. AMT does not imply WKL_{0}.

Proof. No incomplete r.e. degree can bound a model of WKL_{0} by Jockusch and Soare [1972]. On the other hand, by Corollary 3.8 every r.e. degree not in L_{2} bounds one.

We now turn to the relations between AMT and the combinatorial principles ranging in strength from RT_{2}^{2} to ADS and SADS studied in [CJS] and [HS] and defined in §1. We begin with the recursion theoretic arguments for nonimplications.

Corollary 3.10. AMT does not imply RT_{2}^{2}, SRT_{2}^{2}, CAC, COH or CADS.

Proof. RT_{2}^{2} and CAC have recursive instances with no Δ_{2} solution by Jockusch [1972] and Herrmann [2001]. COH has ones whose only Δ_{2} solutions are high (i.e. with jump 0′′) by Cooper [1972] and Jockusch and Stephan [1993], and so does CADS, since it has the same ω-models as COH ([HS]). SRT_{2}^{2} has ones with no low (i.e. with jump 0′) solution (Downey, Hirschfeldt, Lempp and Solomon [2001]). As above, however, every r.e. degree not in L_{2} bounds a model of AMT in which every degree is low.

A more subtle degree theoretic argument shows that AMT does not imply SADS.

Theorem 3.11 ([HS]). For any r.e. A, B there is a recursive order of type ω + ω^{∗} such that, if C is a suborder of type ω or ω^{∗}, then either B ⩽_{T} A ⊕ C or A ⩽_{T} B ⊕ C.

Corollary 3.12. AMT ⊬ SADS.

Proof. By standard results there are high r.e. h, a and b such that a ⩽̸ b ∨ h and b ⩽̸ a ∨ h. (For example, by Robinson [1971] as in Soare [1983, VIII.4.8], every finite usl can be embedded in every interval of r.e. degrees and we can take such an embedding with the bottom of the interval high.) By Corollary 3.8, there is a model of AMT with all sets recursive in h.

AMT also does not imply any of the other principles studied in [HS] that are below ACA_{0} and incomparable with WKL_{0}. In fact, we have a very strong conservation result similar to that for COH in [HS] that implies almost all of these independence results over AMT.

The basic situation here is that we start with a countable model M of RCA_{0} and a notion of forcing P defined over M. Moreover, if G is sufficiently generic over P (usually 1-generic plus satisfying a specific list of requirements that guarantee that if we force an instance of a Σ_{1}^{0} (or Π_{1}^{0}) formula then there is a least instance that can be forced and we do so), we can show that IΣ_{1} holds for formulas over M with G as an added set parameter. (This typically relies on a sufficiently simple definition of forcing for one quantifier sentences.) In this situation, M is an ω-submodel of the model M[G] gotten by adding on to the sets of M all sets definable over M by Δ_{1}^{0} formulas with G as an added set parameter, and M[G] is itself a model of RCA_{0} (Friedman [1976], or see Simpson [1999] or [CJS §6]), where a submodel A of B is an ω-submodel if A has the same first-order part as B. (Warning: in [CJS], M[G] is first officially defined as the model of IΣ_{1} gotten by adding on just G to the sets of M. What we generally want, however, is its extension to a model of RCA_{0}.)

Here we are interested in AMT and the relevant notion of forcing is standard Cohen forcing on the appropriate tree. Note that if G is Cohen 1-generic (i.e. every Π_{1}^{0} formula or its negation is forced and the conditions specific to forcing IΣ_{1} mentioned above are met) then adding G to M preserves IΣ_{1} and so M[G] ⊨ RCA_{0}.

Theorem 3.13. Let M be a countable model of RCA_{0} and let Φ(A, B) be a Σ_{3}^{0} predicate of two set variables such that for some fixed A ∈ M there is no B ∈ M with M ⊨ Φ(A, B). If G is Cohen 2-generic over M then there is no B ∈ M[G] with M[G] ⊨ Φ(A, B).

Proof. Suppose that Φ(A, B) = ∃x ∀y ∃z φ(A, B, x, y, z) where φ is Δ_{0}^{0} and, for the sake of a contradiction, that there is a B ∈ M[G] such that M[G] ⊨ Φ(A, B). Now M is an ω-submodel of M[G], and B is of the form Φ_{e}^{G⊕C} for some Turing functional Φ_{e} and set C in M, so for some x ∈ M,

M[G] ⊨ Φ_{e}^{G⊕C} is a total characteristic function and ∀y ∃z φ(A, Φ_{e}^{G⊕C}, x, y, z).

As this whole formula is equivalent (even in RCA_{0}) to a Π_{2}^{0}(G) (over M) formula ∀y ∃z Ψ(G, C, A, x, y, z) and G is 2-generic, there is a condition p ∈ M such that p ⊩ ∀y ∃z Ψ(G, C, A, x, y, z).

By the general definition of forcing this means that for every y in M and every condition p′ ⩽ p, there is a z ∈ M and a condition p′′ ⩽ p′ such that p′′ ⊩ Ψ(G, C, A, x, y, z). As forcing a Δ_{0}^{0} formula is itself a Δ_{0} relation, we can now define by recursion the function f such that f(0) = p and f(n + 1) ⊩ ∃zΨ(G, C, A, x, n, z). As M is a model of RCA_{0}, this function is an element of M and so gives the characteristic function of a set H ∈ M which by construction satisfies ∀y ∃z Ψ(H, C, A, x, y, z). Finally, if D = Φ_{e}^{H⊕C} then D ∈ M and M ⊨ ∀y ∃z φ(A, D, x, y, z) for the desired contradiction.

We now want to observe that adding a Cohen 2-generic adds an atomic model of each atomic theory T ∈ M. (In fact, even less than meeting all uniformly Π_{1}^{0} sequences of dense sets suffices for AMT as we will see in §4.) Iterating the forcing will then provide our conservation result.

Proposition 3.14. Let M be a countable model of RCA_{0} and let T be an atomic theory in M. If G is Cohen 2-generic over M then there is an A ∈ M[G] that is an atomic model of T in M[G].

Proof. Consider again the tree S in M of all standard Henkin constructions of models of T. For each initial segment of Henkin constants c̄ the set of nodes σ of S that include an atom φ about c̄ is dense by the assumption that T is atomic. Moreover, this set is Π_{1} as that is the complexity of the statement that φ is an atom of T. Thus the path through S determined by G meets every such set and so produces an atomic model of T as required.

We now have our conservation and nonimplication results. In the terminology of Simpson [1999, Definition VII.2.28], a model M is a restricted β-submodel of a model M′ if M is an ω-submodel of M′ and for every sentence of the form ∃X ψ where ψ is Π_{2}^{0} with parameters in M, we have M ⊨ ∃X ψ if and only if M′ ⊨ ∃X ψ. (This condition says that a subtree of ℕ^{<ℕ} in M has a path in M if and only if it has a path in M′, whence the terminology.)

Corollary 3.15. AMT is restricted (r-)Π_{2}^{1} conservative over RCA_{0}, i. e. conservative over RCA_{0} for sentences of the form ∀A (Θ(A) → ∃B Φ(A, B)) where Θ is arithmetic and Φ is Σ_{3}^{0}. Furthermore, every model of RCA_{0} is a restricted β-submodel of a model of AMT.

Proof. Consider any sentence of the specified form and any model M of RCA_{0} not satisfying the sentence. Then there is a set A of M such that M ⊨ Θ(A) for which there is no B in M such that M ⊨ Φ(A, B). Construct a sequence ⟨G_{i} | i ∈ ω⟩ of subsets of ℕ^{M} such that G_{i+1} is Cohen 2-generic over M[G_{1}] … [G_{i}]. Let M′ = ⋃{M[G_{0}] … [G_{i}] | i ∈ ω}. By the results mentioned above, M[G_{0}] … [G_{i}] ⊨ RCA_{0} for each i, and, by Proposition 3.14, every atomic theory T in M[G_{0}] … [G_{i}] has an atomic model in M[G_{0}] … [G_{i}][G_{i+1}]. Thus M′ ⊨ RCA_{0} + AMT as the first order part of every element of this ascending sequence of models is the same. By induction (on true ω) our theorem shows that there is no B ∈ M[G_{0}] … [G_{i}] such that M[G_{0}] … [G_{i}] ⊨ Φ(A, B). Again, as each successive model in this list is an ω-extension of the preceding one and M′ is just their union, we see that while M′ ⊨ Θ(A), there is no B ∈ M′ such that M′ ⊨ Φ(A, B). Thus our original sentence is not a theorem of RCA_{0} + AMT, as required.

The version of the corollary in terms of restricted β-extensions follows by taking Θ to be empty and Φ to be Π_{2}^{0}. Our argument shows that if M′ ⊨ ∃B Φ then M ⊨ ∃B Φ. The other direction follows from the fact that M is an ω-submodel of M′.

We note that this result also provides the usual Π_{1}^{1} conservativity result, since any Π_{1}^{1} sentence ∀AΨ(A) is equivalent to ∀A(¬Ψ(A) → ∃B(0 ≠ 0)). Moreover, the result is the best possible one of this form as AMT itself is a sentence of the form ∀A (Θ(A) → ∃B Φ(A, B)) with Θ arithmetic and Φ a Π_{3}^{0} formula. It is, however, strong enough to show that any principle that asserts, for example, the existence of an infinite set satisfying some recursive condition such as being homogeneous, a path through a tree, or a chain or antichain in a linear or partial order cannot be implied by AMT, as all of these statements are ones in which Φ is Π_{2}^{0}.

Corollary 3.16. None of the following principles are implied by AMT: RT_{2}^{2}, SRT_{2}^{2}, WKL_{0}, DNR, CAC, ADS, SADS.

By the argument of [HS] using Mathias forcing we can also add COH so that AMT + COH has the same properties specified in Corollaries 3.15 and 3.16 for AMT alone.

Note that by [HS] CAC, ADS and SADS are also incomparable with WKL_{0}.

4 AMT, SADS and IΣ_{2}

We now place AMT with respect to the combinatorial principles of [HS] by showing that it is implied by the weakest of them that is not conservative over RCA_{0}: SADS. (Note that by Corollary 3.16 this implication is strict.) We also place it more precisely in the purely proof theoretic hierarchy by showing that it is Π_{1}^{1}-conservative over BΣ_{2}. The proof of the implication uses a finite injury priority argument that must be carried out in RCA_{0} (and so only with IΣ_{1}) by using Shore blocking. The situation is more subtle than might first appear as similar constructions provide priority arguments for slightly stronger conclusions that, provably, cannot be carried out in RCA_{0}. The conservation proof also uses a priority argument. We will discuss these issues after proving our implication from SADS.

Theorem 4.1. RCA_{0} ⊢ SADS → AMT.

Proof. We work in RCA_{0} and begin with an atomic theory T. We again have the tree S of standard Henkin constructions of models of T (with Henkin constants c_{i}). We want to recursively define an ordering <_{L} on ℕ of type ω + ω^{∗} such that recursively in any subsequence R of type ω or ω^{∗} we can construct an infinite path P through S that corresponds to an atomic model A of T. Looking ahead to the construction of the path and model, we define a monotonic recursive operation Φ taking finite sequences of numbers to finite paths in S.

We define Φ(x_{1}, …, x_{n}) = ⟨σ_{1}, …, σ_{n}⟩ to be an increasing sequence of nodes in S by recursion on n. We let σ_{1} be the least node σ on S (in some standard ordering of nodes of type ω) that mentions c_{0} and such that in a (standardized) search of x_{1} many steps we have not found a witness to the assertion that σ is not an atom about c_{0}. (Remember that the nodes on S correspond to the conjunction of sets of formulas about the Henkin constants. This conjunction, viewed as a sentence about any particular set of constants (by existentially quantifying out the rest), may or may not be an atom of T. To see that it is not an atom, it suffices to find two incompatible extensions both of which are consistent with T. As T is complete, this is a recursive test of the candidate extensions.) We now proceed by induction. Given σ_{i} we let σ_{i+1} be the least σ (in the standard ordering) extending σ_{i} on S that mentions all of c_{0}, …, c_{x_{i}} such that in x_{i+1} many steps we have not found a witness to the assertion that σ is not an atom about c_{0}, …, c_{x_{i}}.

Our goal in defining our order L is to guarantee that any ω or ω^{∗} subsequence will infinitely often have successive elements far enough apart so that applying Φ will, for each i, produce at some point a correct witness that some σ_{n} is an atom for c_{0}, …, c_{i}. If so, Φ applied to any such sequence will produce our desired path through S generating an atomic model of T.

The construction of L will involve a movable marker procedure with two sets of markers d_{i,s} and u_{i,s} that remain in two disjoint parts D_{s} and U_{s} of L with every member of D_{s} being L-less than every member of U_{s}. The intuition is that the limit D of D_{s} is the ω part of L (the down side) and the limit U of U_{s} is the ω^{∗} part (the up side). The d_{i,s} and u_{i,s} will also stabilize to numbers d_{i} and u_{i} that will be in D and U and ordered by <_{L} in the end in ω and ω^{∗} orderings, respectively. We have requirements D_{i} and U_{i} with a standard priority ordering giving D_{i} priority over D_{j} for j > i and over U_{j} for j ⩾ i, and U_{i} priority over U_{j} for j > i.

We say that the requirement D_{i} needs attention at stage s if there exists a sequence x_{1}, …, x_{n}, d_{i,s} of elements of D_{s} increasing in both L and natural order such that Φ(x_{1}, …, x_{n}, d_{i,s}) = ⟨σ_{1}, …, σ_{n+1}⟩ and by stage s we have seen a witness that σ_{n+1} does not supply an atom about c_{0}, …, c_{x_{n}}. Similarly, we say that U_{i} needs attention at stage s if there is a sequence x_{1}, …, x_{n}, u_{i,s} of elements of U_{s} decreasing in L and increasing in the natural order such that Φ(x_{1}, …, x_{n}, u_{i,s}) = ⟨σ_{1}, …, σ_{n+1}⟩ and by stage s we have seen a witness that σ_{n+1} does not supply an atom about c_{0}, …, c_{x_{n}}.

At stage s let r be the smallest number not yet appearing in L_{s} = D_{s} ∪ U_{s}. Suppose the highest priority requirement needing attention at s is D_{i}. We move all numbers in D_{s} that are L greater than or equal to d_{i,s} to be the L smallest members of U_{s+1} (preserving the L order already defined on them). We let d_{i,s+1} = r and insert it as the L largest element of D_{s+1}. All d_{j,s+1} become undefined for j > i as do all u_{j,s+1} for j ⩾ i. Similarly, if the highest priority requirement needing attention at s is U_{i}, we move all numbers in U_{s} that are L smaller than or equal to u_{i,s} to be the L largest members of D_{s+1} (preserving the L order already defined on them). We let u_{i,s+1} = r and insert it as the L smallest element of U_{s+1}. All u_{j,s+1} become undefined for j > i as do all d_{j,s+1} for j > i. If no requirement needs attention, we add r as the L largest member of D_{s+1}, let it be d_{j,s+1} for the least j such that d_{j,s} is undefined, and add r + 1 as the L smallest member of U_{s+1} and let it be u_{j.s+1} for the least j such that u_{j,s} is undefined. We then go on to the next stage.

We first claim that every n is eventually in L_{s} and from some stage onward is always in D_{s} or always in U_{s}. As for entering L_{s}, as we always put in the least number not yet in L_{s} at every stage, n ∈ L_{n+1}. Once n is in D_{s} or U_{s}, it can change to the other at t > s only when we act for some requirement. By IΣ_{1} there is a requirement of highest priority for which we ever act that moves n. Say it is D_{i} and it acts to move n at stage t. This means that d_{i,t} ⩽_{L} n, we move n to U_{t+1} and all markers of lower priority become undefined. No action for U_{j} of higher priority ever moves n back to D_{s} by our choice of D_{i}. Any marker of lower priority is appointed after t and assigned to a number that, by construction, is L-less than n. Moving such a lower priority marker for its requirement, by construction, does not move any number L-above it. Thus n never leaves U_{s} after t. The argument if the highest priority requirement moving n is U_{i} is symmetric.

Once n has stopped moving at t, all numbers entering L after t are L-above n (if it is in D_{t}) or all are L-below n (if it is in U_{t}). Thus n has either finitely many L predecessors or finitely many L successors and is therefore of type ω + ω^{∗} as desired. We now apply SADS to get an infinite ascending or descending sequence R = ⟨x_{i}⟩ in L. Without loss of generality, assume it is ascending in L and in natural order. Let P = Φ(⟨x_{i}⟩) be the path in S determined by R. We claim that it includes an atom for each initial segment c_{0}, …, c_{n} of Henkin constants and so provides the required atomic model of T. We need an important fact about the construction.

Lemma 4.2. If we act for a requirement D_{i} at s and never act for any requirement of higher priority again then we eventually stop acting for D_{i} and so d_{i,t} eventually remains fixed. Moreover, if d_{i,s} never changes after t, then, for any sequence x_{1}, …, x_{n}, d_{i,t} that is increasing in both L and natural order, σ_{n+1} includes an atom about c_{0}, …, c_{x_{n}} where Φ(x_{1}, …, x_{n}, d_{i,t}) = ⟨σ_{1}, …, σ_{n+1}⟩.

Similarly, if we act for a requirement U_{i} at s and never act for any requirement of higher priority again then we eventually stop acting for U_{i} and so u_{i,t} eventually remains fixed. Moreover, if u_{i,s} never changes after t, then, for any sequence x_{1}, …, x_{n}, u_{i,t} that is decreasing in L and increasing in natural order, σ_{n+1} includes an atom about c_{0}, …, c_{x_{n}} where Φ(x_{1}, …, x_{n}, u_{i,t}) = ⟨σ_{1}, …, σ_{n+1}⟩.

Proof. We prove the first part of the lemma. The proof of the second part is symmetric.

Suppose we act for D_{i} at s. We then appoint some r as d_{i,s+1}. We now act for D_{i} again only if we discover a new witness as described in the definition of needing attention. As we never act for any requirement of higher priority the numbers L-below d_{i,s+1} are fixed in D_{t} forever. We then act again for D_{i} at t > s only when we discover some new witness that some σ is not an atom, where σ is the final value of Φ(x_{1}, …, x_{n}, d_{i,t}) for some increasing (in both L and natural order) sequence x_{1}, …, x_{n} of numbers L-below d_{i,t}. Each such sequence x_{1}, …, x_{n} produces a fixed σ(x_{1}, …, x_{n}) as the next to last value under Φ. The only variations arise from trying to find the first node τ(x_{1}, …, x_{n}) extending σ(x_{1}, …, x_{n}) that includes an atom about c_{1}, …, c_{x_{n}}. The set of such σ(x_{1}, …, x_{n}) is finite and each has such an atom extending it by the assumption that T is atomic. We can avoid the use of BΣ_{2} that might naturally be invoked to find a common bound on all such extensions by a trick peculiar to our setting. We simply relabel each σ(x_{1}, …, x_{n}) so as to replace the constants c_{1}, …, c_{x_{n}} by new free variables that are distinct from the ones used for all the other sequences. The other constants appearing are existentially quantified out as usual. This gives a formula with x_{n} many free variables for each sequence x_{1}, …, x_{n} with all the sets of variables distinct for different sequences. We can now consider the conjunction of all these formulas as a single formula of many variables. (Note that this conjunction is consistent with T. Each conjunct is consistent with T and so the existential closure of each conjunct is a theorem of T. As all the variables are distinct, the conjunction of these existential closures is the existential closure of the conjunct which is therefore itself consistent with T.) As T is atomic this formula can be extended to an atom Ψ. If in Ψ we existentially quantify out the variables not free in the relabeled σ(x_{1}, …, x_{n}), we have an atom extending σ(x_{1}, …, x_{n}). Thus there is a single bound on atoms extending all the relevant σ(x_{1}, …, x_{n}) and so by IΣ_{1} there is a first one for each and a bound on the witnesses needed to show that all smaller candidates are not such atoms. Once we are above such a stage, no change occurs in d_{i,t} and its value must also be above the stage at which the correct extensions are found for each σ(x_{1}, …, x_{n}). After such a stage D_{i} will never need attention again. In particular, this stage is large enough so that the search incorporated in Φ produces a σ_{n+1} including an atom about c_{1}, …, c_{x_{n}}.

Returning to our verification that P determines an atomic model of T, we choose any m = x_{j+1} ∈ R so that x_{j} is larger than n and let t be the last stage at which m is put into D_{t}. If it is moved into D_{t} (say by the action of some U_{i}) then it is part of a block of numbers moved all of which are L-below u_{i,t}. Otherwise, it is just put into D_{t} on its own as some d_{i,t} at t and never moves. In the second case, by the lemma applied to D_{i}, if Φ(x_{1}, …, x_{j}, m) = ⟨σ_{1}, …, σ_{j+1}⟩ then σ_{j+1} includes an atom about c_{0}, …, c_{x_{j}} and so one about c_{0}, …, c_{n} as required. In the first case, no D_{k} of higher priority than U_{i} can act after t as that would move m. The highest priority requirement that acts at a t′ ⩾ t must be a U_{j} for j ⩽ i. Let U_{j} be that requirement and (by the lemma) let v the last stage at which it acts. At v, the marker u_{j,v} and a block of numbers are moved from U_{v} to U_{v+1}. They include m (if v = t) and otherwise are all L-above m. At v + 1 no requirement can need attention as all of lower priority than U_{j} have had their markers undefined at v and no higher priority ones can act by our assumptions. Thus we insert some number r as the L-greatest element of D_{v+1} and let it be d_{j+1,v+1}. By the lemma there is a stage w ⩾ v + 1 at which we last act for D_{j+1}. At w we appoint some r′ as d_{j+1,w} and it too is L-above m. Let m′ be the last element of R in [m, r′) and m′′ be the first element of R greater than or equal to r′. By the lemma, if Φ(x_{1}, …, x_{j}, m′, r′) = ⟨σ_{1}, …, σ_{j+2}⟩ then σ_{j+2} includes an atom about c_{1}, …, c_{m′}. As m′′ ⩾ r′, the search to produce the last element of Φ(x_{1}, …, x_{j}, m′, m′′) begins with the same σ_{j+1} and runs for at least as many steps as the one that produced the correct answer in r′ many steps. Thus it too produces the desired atoms and as x_{1}, …, x_{j}, m′, m′′ is an initial segment of R, the sequence Φ(R) contains an atom about c_{1}, …, c_{m′} and so, of course, about c_{1}, …, c_{n} as required.

The above argument is a finite injury one that we carried out in RCA_{0} and so only using IΣ_{1}. The amount of induction needed for various types of priority arguments has been extensively studied as reverse recursion theory but primarily in the setting of first order arithmetic (where one talks about r.e. or Δ_{2} sets in terms of their indices). Good basic references here include Chong and Yang [1998] and [2000]. A number of finite injury arguments have been carried out in IΣ_{1}, such as the Friedberg-Muchnik theorem and even the Sacks splitting theorem. The general situation described by Groszek and Slaman [nd] is that ones with recursive bounds on the number of injuries (as in the Friedberg-Muchnik type arguments) can be carried out in IΣ_{1}. Ones with unbounded (but still finite) injuries (as in the Sacks splitting theorem) can at times be carried out in IΣ_{1} or BΣ_{2}. However, the ability to carry out all such arguments implies IΣ_{2} over BΣ_{2}. On the other hand, until now there did not seem to be a known example of a single theorem of this type that cannot be carried out in BΣ_{2}.

Our theorem about SADS and atomic models involves a finite injury priority argument as does the one in [HS] building low solutions to SADS. One could also frame the basic construction of an atomic model of an atomic theory as an argument of this sort. Viewed as a forcing argument, the general construction of an atomic model involves meeting a uniformly Π_{1}^{0} set of dense sets (the atoms along the tree of the Henkin construction). Our construction in Theorem 4.1 gets by with IΣ_{1} because of two special properties of the argument. The first corresponds to the technique developed in α-recursion theory (Shore [1975]) and latter called Shore blocking in applications to reverse recursion theory in models of first order arithmetic (as in Mytilinaios [1989]). It relies on the fact that producing an atom for the single n-tuple c_{1}, …, c_{n} automatically produces one for all j-tuples from the set {c_{1}, …, c_{n}} for all j ⩽ n. Thus at any stage s we can take care of all requirements of this form up to s by a single action. The second use of such a special property allowed us to avoid BΣ_{2} in the argument that action for each single requirement was bounded by combining finitely many formulas into one before finding an atomic extension.

If we move on to the general case of meeting arbitrary uniformly Π_{1}^{0} collections of dense sets we actually find a theorem proven by a priority argument of the unbounded but finite type that requires IΣ_{2} in the sense of reverse mathematics. The theorem is that for any uniformly Π_{1}^{0} collection of sets D_{i} each of which is dense in 2^{<ℕ} there is a set G that meets each of them, i.e. ∀i∃s(G ↾ s ∈ D_{i}) and is low, i.e. G′ is Δ_{2}. This theorem is easily proved assuming IΣ_{2} by a standard finite injury argument. The number of times we act to get into a single D_{i} is finite but, in general, unbounded. (Each lowness requirement acts at most once after it has highest priority.) We denote the formal version of this theorem by Π_{1}^{0}G (for Π_{1}^{0} Generic), and claim that it implies IΣ_{2} over the base theory BΣ_{2}. To remain in keeping with the rest of this paper we formulate our result in second order arithmetic over RCA_{0} but it is not difficult to translate it to the more usual setting of first order arithmetic.

(Π_{1}^{0}G) For any uniformly Π_{1}^{0} collection of sets D_{i} each of which is dense in 2^{<ℕ} there is a G such that ∀i∃s(G ↾ s ∈ D_{i}).

Theorem 4.3. RCA_{0} + BΣ_{2} ⊢ Π_{1}^{0}G → IΣ_{2}.

Proof. Let (M, S) be a model of RCA_{0} + BΣ_{2} in which each uniformly Π_{1}^{0} collection of dense subsets of 2^{<ℕ} has a G meeting all its members. Suppose for the sake of a contradiction that IΣ_{2} fails in M. Then there is a Σ_{2} cut I in M, i.e. x ∈ I ⇔ ∃y∀zφ(x, y, z) and I is an initial segment of M closed under successor. The dense sets D_{i} we consider correspond to the actions of getting a gap large enough to correctly recognize one more witness for membership in I (and also in a D_{i}). To be precise we let

D_{i} = {σ ∈ 2^{<ℕ} | the last two elements of σ are w and ⟨i, x, y⟩ ∧ ∃y′ < y∀zφ(x, y′, z) ∧ ∀y′ ⩽ w∃z′ < y(¬φ(x, y′, z′))}.

Clearly the D_{i} are uniformly Π_{1}^{0}. As I is a cut and so not a member of S, there is no bound on the least witnesses y such that ∀zφ(x, y, z) for x ∈ I, while by IΣ_{1} every x ∈ I has such a least witness y, and by BΣ_{2} there is a bound on the z′ needed to show that y is in fact the least witness for x. Thus each D_{i} is dense, for if we consider any τ with last element w there is an x ∈ I whose least witness y is larger than w and a z > y such that counterexamples for all y′ ⩽ w can be found below z. So if we let σ extend τ by adding on as its first new element ⟨i, x, z⟩ we have our extension of τ in D_{i} as required.

Let G be as in Π_{1}^{0}G and let a be any number above all those in I. By our assumption ∀i < a∃s(G ↾ s ∈ D_{i}). As being in D_{i} is a Π_{1} property uniformly, by BΣ_{2} there is a t such that ∀i < a∃s < t(G ↾ s ∈ D_{i}). Moreover, the set R = {s < t | ∃i < a(G ↾ s ∈ D_{i})} is M-finite (i.e. coded in M by a number) as is the relation

S = {⟨i, x⟩ | i, x < a ∧ ∃s < t(G ↾ s ∈ D_{i}) ∧ ∃y(the last element of G ↾ s is ⟨i, x, y⟩)}

by BΣ_{2}. Finally, we claim S is, in fact, a one-one function from a into I and so into a proper subset of a for the desired contradiction. We have already seen that for every i < a there is an x ∈ I such that ⟨i, x⟩ ∈ S. Suppose then that we have i ≠ j both below a and r, s < t such that G ↾ r ∈ D_{i} and G ↾ s ∈ D_{j}, the next to last and last elements of G ↾ r are v and ⟨i, x_{i}, y_{i}⟩, and the next to last and last elements of G ↾ s are w and ⟨j, x_{j}, y_{j}⟩. Without loss of generality, we assume that r < s and so v < ⟨i, x_{i}, y_{i}⟩ ⩽ w < ⟨j, x_{j}, y_{j}⟩. (As i ≠ j, we know that G ↾ r and G ↾ s have different last elements and so r ≠ s.) If x_{i} = x_{j} = x, we would have an immediate contradiction as the definitions of D_{i} and D_{j} would say that ∃y′ < y_{i}∀zφ(x, y′, z) and ∀y′ ⩽ w∃z′ < y(¬φ(x, y′, z′)), respectively, but y_{i} ⩽ w.

Note that Π_{1}^{0}G is obviously implied by the assumption of the existence of sets Cohen 2-generic with respect to any given set. The addition of such a set by standard Cohen forcing preserves IΣ_{1} and IΣ_{2} (if true in the ground model). Thus the arguments of Theorem 3.13 and Corollary 3.15 show that Π_{1}^{0}G, while not conservative over BΣ_{2}, is r-Π_{2}^{1} conservative over both IΣ_{1} and IΣ_{2} as is AMT.

To conclude our analysis, we show that retreating to AMT gives us Π_{1}^{1}-conservativity over BΣ_{2} as well as IΣ_{1} and IΣ_{2}. The only other known examples of mathematical principles conservative over all three theories are WKL_{0} (Hájek [1993]) and COH (Chong, Slaman and Yang [ta]). Here too we use a priority argument with Shore blocking.

Theorem 4.4. Let M be a model of BΣ_{2} and T an atomic theory in M. Let F be the tree of Henkin constructions of models of T in M (as in Definition 3.5). Then there is a path P through F such that M[P] ⊧ BΣ_{2} and the model of T given recursively in P as in Remark 3.6 is atomic.

Proof. Our goals for P are that it preserve BΣ_{2} and that the associated formulas S_{σ} for σ ∈ P (when extraneous new constants are replaced by new free variables and existentially quantified) include atoms for each initial segment c_{1}, … c_{n} of Henkin constants. As auxiliary requirements we will make P be 1-generic (for every e there is a σ ⊆ P such that Φ_{e}^{σ}(e)↓ or ∀τ ⊇ σ(Φ_{e}^{τ}(e)↑)) and preserve IΣ_{1}. Our construction will be a movable marker one that produces P as a limit of approximations σ_{s} so that P will be Δ_{2} with convergence at all initial segments σ: (∀σ ∈ 2^{<ℕ})[σ ⊆ P ⇔ ∃s∀t > s(σ ⊆ σ_{t}) ⇔ ∀s∃t > s(σ ⊆ σ_{t})]. Thus we will have Π_{1}^{P} ⊆ Σ_{2}: Φ_{e}^{P} (e)↑ ⇔ (∃σ)(σ ⊆ P ∧ ∀τ ⊇ σ(Φ_{e}^{τ}(e)↑)). In particular, any Σ_{2}^{P} formula in M[P] will then be equivalent to one that is Σ_{2} in M and so BΣ_{2} will hold in M[P] since it holds in M.

We have the following requirements:

R_{⟨e,n⟩}: Decide the e^{th} Σ_{1}^{0} sentence with parameter n, i.e. get a σ ⊆ P such that Φ_{e}^{σ}(n)↓ or ∀τ ⊇ σ(Φ_{e}^{τ}(n) ↑). If we satisfy the R_{⟨e,n⟩} corresponding to a Σ_{1}^{0} formula ∃xψ(x, n) by forcing convergence, we act to preserve IΣ_{1} by guaranteeing that there is a least m such that ∃xψ(x, m) by getting a σ ⊆ P such that Φ_{e}^{σ}(n) ↓ and, for every k < m and τ ⊇ σ, we have Φ_{e}^{τ}(k)↑.

A_{e}: There is a σ ⊆ P such that S_{σ} implies an atom for c_{1}, … c_{e}.

At each stage s of the construction we have an approximation σ_{s} to P and movable markers q_{i,s} (which may be of type R or A) for an initial segment of i’s indicating the place (σ_{s} ↾ q_{i,s}) at which we think we have satisfied Q_{j} (Q = R or A) for j < q_{i−1,s}. At stage s we define whether a marker q_{i,s} needs attention and the associated action for q_{i,s} by cases.

Q = R: First, q_{i} needs attention if there is an ⟨e, n⟩ < q_{i−1,s} such that Φ_{e}^{σ_{s}↾q_{i,s}}(n) ↑ and a τ ⊇ σ_{s} ↾ q_{i,s} with |τ| < s such that Φ_{e}^{τ}(n)↓. If so, we find the least such ⟨e, n⟩ and the least τ for it and set σ_{s+1} = τˆ 0^{k} where k is chosen so that |σ_{s+1}| = s; then q_{i,s+1} = s. If not, but there is an ⟨e, n⟩ < q_{i−1,s} such that Φ_{e}^{σ_{s}↾q_{i,s}}(n)↓, a k < n and τ ⊇ σ ↾ q_{i,s} such that Φ_{e}^{τ}(k) ↓, but no l ⩽ k such that Φ_{e}^{σ_{s}↾q_{i,s}}(l)[s] ↓, then q_{i} also needs attention. In this case, we find the least such ⟨e, n⟩ and the least k and τ for it and set σ_{s+1} = τˆ 0^{k} where k is chosen so that |σ_{s+1}| = s; then q_{i,s+1} = s.

Q = A: If we see in s many steps that S_{σ_{s}↾q_{i,s}} does not imply an atom about c_{1}, … c_{q_{i−1,s}}, then q_{i} needs attention. If so, we let τ ⊇ σ_{s} ↾ q_{i−1,s} be least such that in s many steps we do not find a witness that S_{τ} does not includes an atom about c_{1}, … c_{q_{i−1,s}} and set σ_{s+1} = τˆ 0^{k} where k is chosen so that |σ_{s+1}| = s; then q_{i,s+1} = s.

In each case, all markers q_{j} for j > i become undefined and all with j < i remain as they were at s.

Of course, at stage s we act for the least q_{i} that needs attention. If no marker now defined requires attention we let σ_{s+1} = σ_{s}ˆ 0 and set q_{i,s+1} = |σ_{s+1}| for the least i for which q_{i,s} is undefined.

As in the proof of Theorem 4.1 and as usual in blocking arguments, it suffices to show that if, for all j < i, the q_{j,s} have reached their final positions q_{j} by stage t then q_{i,s} eventually stops moving (with final value q_{i}) and so P is well defined as the union of the σ_{q_{i}}. (The q_{i} are cofinal in M by the construction as they are the stage at which q_{i,s} is last changed and if none are changed at s then a new one larger than all the others is added to the list of defined markers.) Moreover, we argue that the associated requirements are all satisfied. We have two cases.

Q = A: By our assumption that T is atomic there is a τ ⊇ σ ↾ q_{i−1} such that S_{τ} includes an atom for c_{1}, … c_{q_{i−1}}. There is a least one by IΣ_{1} (in the form of the equivalent principle IΠ_{1}) and by BΣ_{1} a stage by which all smaller ρ ⊇ σ_{q_{i−1}} have been seen to not do so. At the first such stage s after q_{i−1} has settled down, we set σ_{s} = τˆ 0^{k} for some k and q_{i,s} = s and never change q_{i,s} or σ_{s} ↾ q_{i,s} again.

Q = R: Once q_{i−1,s} has settled down, q_{i,s} moves monotonically upward. It moves only for the sake of some ⟨e, n⟩ < q_{i−1} as in the first case of the description of the action of R, or some ⟨e, n⟩ < q_{i−1} and k < n as in the second case of that description. In any event, it moves at most once for each such ⟨e, n⟩ or pair of ⟨e, n⟩ and k. The set of ⟨e, n⟩ < q_{i−1} and pairs of ⟨e, n⟩ < q_{i} and k < n for which q_{i,s} moves is Σ_{1} and so by IΣ_{1} finite in M, and the set of stages at which it moves is then bounded as well. Once q_{i,s} has settled down to its final value q_{i}, the value of σ_{s} ↾ q_{i} never changes either, by construction. Finally, it is clear from the definition of markers of type R requiring attention and the associated action that we satisfy the requirements: for every ⟨e, n⟩ < q_{i−1} either Φ_{e}^{P ↾q_{i}}(n)↓ or (∀τ ⊇ P ↾ q_{i})(Φ_{e}^{τ}(n) ↑), and if Φ_{e}^{P ↾q_{i}}(n) ↓ then there is a k ⩽ n such that Φ_{e}^{P ↾q_{i}}(k) ↓ while for every l < k and τ ⊇ P ↾ q_{i}, we have Φ_{e}^{τ}(l)↑.

Thus for each i in an initial segment of M the q_{i,s} settle down to a sequence q_{i} cofinal in M and we have satisfied all the R requirements. Once q_{i} has stopped moving σ ↾ q_{i} never changes either and so P settles down in the way required by the argument given at the beginning of this proof to show that M[P] ⊧ BΣ_{2}. Moreover, the model defined in M[P] by S_{P} as in Remark 3.6 is an atomic model of T as we have satisfied the A requirements.

The usual iteration of this construction gives an ω-extension of M that satisfies both BΣ_{2} and AMT and so we have our final result here.

Corollary 4.5. AMT is Π_{1}^{1}-conservative over BΣ_{2}.

For any complete decidable atomic theory T, let S be the tree of standard Henkin constructions of models of T. For any tuple of constants c⃗, the set of nodes of T that are atoms about c⃗ is dense, and these sets are uniformly Π_{1}^{0} when taken over all tuples of constants. Thus Π_{1}^{0}G implies AMT. On the other hand, Theorem 4.3 and Corollary 4.5 show that the converse does not hold. However, Conidis [ta] has shown that every ω-model of AMT is also a model of Π_{1}^{0}G, so the use of non-ω-models is essential in establishing this nonimplication. As, like AMT, Π_{1}^{0}G can be forced by iterating the addition of Cohen 2-generics, it is also r-Π_{2}^{1} conservative over RCA_{0} by Theorem 3.13. Thus it (even with the addition of COH as in Corollary 3.16) does not imply any of WKL_{0}, RT_{2}^{2}, SRT_{2}^{2}, CAC, ADS, SADS or DNR (even for ω-models). As we remarked above, it is easy in the standard model to meet any uniformly Π_{1}^{0} collection of dense sets with a low set, so the degree theoretic properties mentioned in Corollary 3.10 show that it does not imply COH or CADS either, even for ω-models.

We do not know whether RT_{2}^{2} implies Π_{1}^{0}G. It is straightforward to check that the construction used in Conidis’ proof mentioned in the previous paragraph can be carried out and verified in RCA_{0} + IΣ_{2}, and hence RCA_{0} + IΣ_{2} ⊢ AMT → Π_{1}^{0}G. Since RT_{2}^{2} implies AMT, we have that RT_{2}^{2} + IΣ_{2} implies Π_{1}^{0}G. On the other hand, by Hirst [1987], RT_{2}^{2} implies BΣ_{2}, so by Theorem 4.3, RT_{2}^{2} + Π_{1}^{0}G implies IΣ_{2}. Thus the question of whether RT_{2}^{2} implies Π_{1}^{0}G is equivalent to the question of whether RT_{2}^{2} implies IΣ_{2}, which is the first part of Question 13.7 in [CJS]. Of course, this equivalence remains true if we replace RT_{2}^{2} by any of the principles considered in [HS] such as SRT_{2}^{2}, CAC and ADS that lie between RT_{2}^{2} and AMT and imply BΣ_{2}.

5 Type omitting and hyperimmunity

In this section we consider a version of the Omitting Types Theorem that has close connections with the Atomic Model Theorem. We begin with a recursion theoretic analysis, and later derive some reverse mathematical consequences. The classical Omitting Types Theorem states that if T is a complete theory and S is a countable set of nonprincipal types of T, then there is a model of T omitting all the types in S. Millar [1983] proved the following effective version of this fact.

Theorem 5.1 (Millar [1983]). Let T be a complete decidable theory. Let S_{0} be a recursive set of complete types of T. Let S_{1} be a recursive set of nonprincipal partial types of T. There is a decidable model of T omitting all nonprincipal types in S_{0} and all partial types in S_{1}.

Millar’s proof involves an effective Henkin construction with additional requirements of two kinds: For each partial n-type Γ in S_{1} and each n-tuple of constants c⃗, there is a requirement that c⃗ should not realize Γ. Also, for each n-type Γ in S_{0} and each n-tuple of constants c⃗, there is a requirement that if Γ is nonprincipal then c⃗ should not have type Γ. At a given stage of the construction, we can satisfy a requirement of the first kind simply by extending what we have currently said about c⃗ to disagree with Γ, which we know we can do because we are guaranteed that Γ is nonprincipal.

To satisfy requirements of the second kind, we need to be a little more careful. At a given stage, when deciding whether to add a sentence φ or its negation to the elementary diagram of the model we are building, we find the strongest priority requirement (if any) that would be satisfied by adding φ or its negation, and proceed accordingly. We can then easily argue that, for any given requirement R, once all previous requirements have been satisfied, R will also eventually be satisfied.

This argument is by induction, of course, but the construction involves no injuries. Once a requirement acts, it is permanently satisfied, even if stronger requirements act later on. So we can cast our argument as a Σ_{1}^{0} induction as follows. Given a requirement R, let F be the (finite) set of all stronger requirements that ever act. By the inductive hypothesis, there is a stage s such that every requirement in F has acted by stage s. Now we know that no requirement stronger than R will ever act after stage s, so if the type mentioned in R is nonprincipal, then R will eventually act and be satisfied.

Thus Millar’s proof carries through in RCA_{0}, and hence RCA_{0} proves the following statement: Let T be a complete theory. Let S_{0} be a set of complete types of T. Let S_{1} be a set of nonprincipal partial types of T. There is a model of T omitting all nonprincipal types in S_{0} and all partial types in S_{1}.

On the other hand, Millar [1978] also showed that there is a sense in which the Omitting Types Theorem cannot be made fully effective, as a corollary to the following result on atomic models.

Theorem 5.2 (Goncharov and Nurtazin [1974]; Millar [1978]). There is a complete decidable atomic theory T such that all types of T are recursive but T has no recursive atomic model.

Since the set of all partial types of such a theory T has a recursive listing, we have the following corollary.

Corollary 5.3 (Millar [1978]). There is a complete decidable theory T and a recursive set S of partial types of T such that no decidable model of T omits all nonprincipal partial types in S.

Improving a result of Csima [2004], Hirschfeldt [2006] showed that Theorem 5.2 cannot be improved, in the following sense.

Theorem 5.4 (Hirschfeldt [2006]). Let T be a complete decidable atomic theory such that all types of T are recursive, and let d > 0. Then T has a d-decidable atomic model.

We will consider a version of this result in the context of reverse mathematics in the next section. It is natural to ask whether a similar result holds for the kind of type omitting in Corollary 5.3. Csima [2004] obtained the following partial result.

Theorem 5.5 (Csima [2004]). Let T be a complete decidable theory, let S be a recursive set of partial types of T, and let d be such that 0 < d ⩽ 0′. Then there is a d-decidable model of T that omits all nonprincipal partial types in S.

However, outside the Δ_{2} degrees, the situation for type omitting is different from that for atomic models. As we now show, the degrees that can always carry out the kind of type omitting in Corollary 5.3 are exactly the hyperimmune degrees. Recall that a degree is hyperimmune if it contains a total function f that is not dominated by any recursive function, that is, for each total recursive function g, there are infinitely many n such that f(n) > g(n). If a degree is not hyperimmune then it is hyperimmune-free.

Theorem 5.6. 1. Let T be a complete decidable theory, let L be a recursive set of partial types of T, and let d be a hyperimmune degree. Then there is a d-decidable model of T that omits all nonprincipal partial types in L.

2. There is a complete decidable theory T and a recursive set L of partial types of T such that any countable model of T that omits all nonprincipal partial types in L has hyperimmune degree.

Proof. 1. Since d is hyperimmune, we can fix a d-recursive function f that is not dominated by any recursive function. We use the tree S of Henkin constructions of models of T as in Definition 3.5 and Remark 3.6 so that we think of our d-decidable model as a path in S.

Thus it is enough to show that there is an f-recursive path P of S such that for every nonprincipal Γ ∈ L and every tuple c⃗ of new constants of the same arity as Γ, the following requirement is met:

R_{Γ,c⃗} : if Γ is nonprincipal then there is a γ ∈ Γ with ¬γ(c⃗) ∈ θ^{P} .

We give these requirements a priority ordering in the usual way.

We build P = ⋃ σ_{i}, where we will have σ_{0} ⊂ σ_{1} ⊂ ⋯ and |σ_{i}| = i. At each stage in the construction, each requirement may have a target string. Begin by letting σ_{0} be the empty sequence, and declaring that no requirement has a target.

At stage i, given σ_{i} ∈ S, define σ_{i+1} as follows. Say that R_{Γ,c⃗} is satisfied if there is a γ ∈ Γ with ¬γ(c⃗) ∈ S_{σ_{i}}. Once a requirement is satisfied, cancel its target. Suppose that R_{Γ,c⃗} is not satisfied and does not have a target, and there is a τ ∈ S with S_{τ} propositionally extending S_{σ_{i}} such that |τ| < f(i) and ¬γ(c⃗) ∈ S_{τ} for some γ ∈ Γ. Then declare the least such τ (in some fixed ordering of 2^{<ℕ}) to be the target of R_{Γ,c⃗}.

Let R_{Γ,c⃗} be the strongest among the first i requirements that is not satisfied and has a target, and let τ be its target. If there is no such requirement, let τ be the least immediate successor of σ_{i} on S. Let σ_{i+1} be the immediate successor of σ_{i} extended by τ. Cancel the targets of all requirements weaker than R_{Γ,c⃗}.

Clearly P is an f-recursive path of P. We show by induction that each requirement is satisfied. Assume by induction that there is a stage s after which no requirement stronger than R_{Γ,c⃗} has a target. If there is a stage t ⩾ s at which R_{Γ,c⃗} has a target τ, then P extends τ, which, by the way targets are chosen, implies that R_{Γ,c⃗} is eventually satisfied. Thus it is enough to assume for a contradiction that Γ is nonprincipal and never satisfied, and show that there is a stage t ⩾ s at which R_{Γ,c⃗} has a target.

Define the recursive function g as follows. Given n, let M_{n} be the set of all σ ∈ S such that |σ| = n. For each σ ∈ M_{n}, let τ_{σ} be the least extension of σ on S such that ¬γ(c⃗) ∈ S_{τ_{σ}} for some γ ∈ Γ. Such a τ_{σ} must exist, since otherwise we would have T ∪ S_{σ} ⊢ γ(c⃗) for all γ ∈ Γ, contradicting the assumption that Γ is nonprincipal. Let g(n) = max{|τ_{σ}| : σ ∈ M_{n}}. Now g is a total recursive function, so there is a t > s such that f(t) > g(t). Since σ_{t} ∈ M_{t}, there is a τ extending σ_{t} such that |τ| < f(t) and ¬γ(c⃗) ∈ S_{τ} for some γ ∈ Γ. Since we are assuming R_{Γ,c⃗} is not satisfied at stage t, this means that R_{Γ,c⃗} acquires a target at stage t, as desired.

2. Let T be a subtree of 2^{ℕ} with no dead ends. A partial path of T is a collection G of pairs ⟨n, i⟩ with n ∈ ℕ and i < 2, such that there is a path P of T with P (n) = i for all ⟨n, i⟩ ∈ G. We call any such path P a completion of G. We can think of a path P of T as a partial path by identifying P with {⟨n, P (n)⟩ : n ∈ ℕ}. A partial path G is isolated if there is a σ ∈ T such that every path of T extending σ is a completion of G.

We translate T into a theory T in the language with infinitely many unary relation symbols U_{0}, U_{1}, … as follows. Let Δ be the set consisting of the following axioms:

1. For each σ ∈ T and each n,

∃^{⩾n}x ( ⋀_{σ(i)=1} U_{i}(x) ∧ ⋀_{σ(i)=0} ¬U_{i}(x)).

2. For each σ ∉ T ,

¬∃x ( ⋀_{σ(i)=1} U_{i}(x) ∧ ⋀_{σ(i)=0} ¬U_{i}(x)).

Let T be the theory axiomatized by Δ. It is straightforward to show that T is a complete theory, and is decidable if T is recursive. Furthermore, the partial paths of T correspond to partial 1-types of T in a natural way, and a partial path of T is isolated if and only if the corresponding partial type of T is principal. Finally, a model of T corresponds to a choice of a dense sequence of paths of T (possibly with repetitions).

Thus it is enough to build a recursive subtree T of 2^{ℕ} with no dead ends, and a uniformly recursive collection C of partial paths of T , such that any countable dense sequence of paths of T of hyperimmune-free degree must contain an extension of some nonisolated element of C. Since there are continuum many hyperimmune-free degrees, we cannot play directly against such sequences of paths. Instead, we will build T and define a functional Ψ to satisfy the requirements

R_{e} : if M is a countable dense sequence of paths of T and

either Ψ^{M} is not total or Φ_{e} dominates Ψ^{M}, then M contains an extension of some nonisolated element of C.

We reserve the portion of T above 0^{e}1 for satisfying R_{e}. The functional Ψ is defined by letting Ψ^{M}(n) be the least k such that for each e ⩽ n, there is a P ∈ M extending 0^{e}1, and for the first such P (in the order of M), there are m_{0} < m_{1} < ⋯ < m_{n+1} < k with P (m_{i}) = 1 for each i ⩽ n. We will ensure that every path of T of the form 0^{e}1σ0^{ω} is nonisolated and is in C, which will imply that if Ψ^{M} is not total then either M is not dense or M contains an extension of some nonisolated element of C.

Above 0^{e}1, we act as follows, defining T above this node and defining an element D_{e} of C. Whenever we declare a string to be in T , we of course also put all of its substrings in T . Except for this requirement, any string we do not declare to be in T is not in T . To explain the reasoning behind our construction, consider a countable dense sequence M of paths of T such that Ψ^{M} is total and Φ_{e} dominates Ψ^{M}, and let P be the first element of M extending 0^{e}1. Our task will be to define T and C so that P extends D_{e}, while making D_{e} nonisolated.

We begin by putting ⟨i, 0⟩ for i < e and ⟨e, 1⟩ into D_{e}. This action ensures that any path extending D_{e} must extend 0^{e}1. We then declare that 0^{e}10^{n} is in T for all n, and put 0^{e}10^{ω} into C. For each s such that Φ_{e}(e)[s]↑ and each n < s, we declare that 0^{e}10^{n}1^{s−n} is in T . Suppose there is a least stage t_{0} such that Φ_{e}(e)[t_{0}]↓. By the usual conventions, Φ_{e}(e) < t_{0}. Thus, by the definition of Ψ, the path P must extend 0^{e}10^{n}1 for some n < t_{0}. So for each such n we declare that the string 0^{e}10^{n}1^{t_{0}−n} is in T , and we call these strings the level 1 active nodes above 0^{e}1. For each n ⩾ t_{0}, we declare 0^{e}10^{n}1^{k} to be in T for all k. Notice that for every path Q extending a level 1 active node above 0^{e}1 (including the path P), we have Q(e + t_{0}) = 1, while for every other path Q extending 0^{e}1, we have Q(e + t_{0}) = 0. We now put ⟨e + t_{0}, 1⟩ into D_{e}, thus ensuring that any path extending D_{e} must extend some level 1 active node above 0^{e}1.

We now work only above the level 1 active nodes above 0^{e}1. Above these nodes, we repeat a version of the above construction. More precisely, given a level m active node σ above 0^{e}1, we proceed as follows. (We will have already defined t_{0}, …, t_{m−1} so that |σ| = e + t_{0} + ⋯ + t_{m−1}.) We declare that σ0^{n} is in T for all n and put σ0^{ω} into C. For each s such that Φ_{e}(e + t_{0} + ⋯ + t_{m−1})[s]↑ and each n < s, we declare that σ0^{n}1^{s−n} is in T . If there is a least stage t_{m} such that Φ_{e}(e + t_{0} + ⋯ + t_{m−1})[t_{m}]↓ then we proceed as follows. For each n < t_{1}, we declare that the string σ0^{n}1^{t_{m}−n} is in T , and we call these strings the level m + 1 active nodes above 0^{e}1. For each n ⩾ t_{m}, we declare σ0^{n}1^{k} to be in T for all k. Finally, we put ⟨e + t_{0} + ⋯ + t_{m}, 1⟩ into D_{e}. As argued above for the m = 1 case, every path Q extending a level m active node above 0^{e}1 (including the path P), we have Q(e + t_{0} + ⋯ + t_{m}) = 1, while for every other path Q extending 0^{e}1, we have Q(e + t_{0} + ⋯ + t_{m}) = 0.

We have completed the definition of T and C. Now suppose that M is a countable dense sequence of paths of T and that M has hyperimmune-free degree. If Ψ^{M} is not total, then there is a path P in M of the form 0^{e}1σ0^{ω} for some e and σ. But every such path is put into C during the construction, and is made to be nonisolated. Thus in this case M contains a path extending a nonisolated element of C. On the other hand, if Ψ^{M} is total then there is some e such that Φ_{e} dominates Ψ^{M}. Let P be the first element of M extending 0^{e}1. As argued during the construction, for every m, we have P (e+t_{0}+⋯+t_{m}) = 1. Since D_{e} = {⟨i, 0⟩ : i < e}∪{⟨e, 1⟩}∪{⟨e+t_{0}+⋯+t_{m}, 1⟩ : m ∈ ℕ}, we see that P extends D_{e}. Furthermore, D_{e} is nonisolated, since for every path Q extending D_{e} and every σ ⊂ Q, there is a τ ⊃ σ that is not extended by any node active at any level, which implies that no path extending τ can also extend D_{e}. Thus in this case also, M contains a path extending a nonisolated element of C.

The previous results lead us to consider the following principle.

(OPT) Omitting Partial Types: Let T be a complete theory and let S be a set of partial types of T. Then there is a model of T that omits all nonprincipal partial types in S.

Since there is an ω-model of WKL_{0} consisting entirely of sets of hyperimmune-free degree (see Simpson [1999]), part 2 of Theorem 5.6 implies that WKL_{0} ⊬ OPT.

Iterating Theorem 5.5 and dovetailing in the usual way (also using the density of the r.e. degrees), we see that every r.e. degree bounds an ω-model of OPT. This fact means that OPT does not imply any of the principles mentioned above, except those that follow from RCA_{0} and possibly IΣ_{2} and BΣ_{2}. As we will see below, AMT implies OPT, and hence OPT also does not imply IΣ_{2} or BΣ_{2}.

The reverse mathematical analogue of Theorem 5.6 also holds. Let HYP be the statement that for every set X there is a degree that is hyperimmune relative to X, in other words, there is a function not dominated by any X-recursive function. (See Definition VII.1.4 of Simpson [1999] for a definition of relative recursiveness in RCA_{0}.)

Theorem 5.7. RCA_{0} ⊢ OPT ↔ HYP.

Proof. It is straightforward to check that the proof of part 2 of Theorem 5.6 relativizes to any set X and can be carried out in RCA_{0}.

The proof of part 1 of Theorem 5.6 can also be carried out in RCA_{0}. As usual, the only worry is the induction required to prove that every requirement is satisfied. Notice, however, that while a requirement’s target may be canceled by a stronger priority requirement, once a requirement is satisfied, it can no longer be injured. Therefore we can argue by Σ_{1}^{0} induction as follows.

Fix a requirement R_{Γ,c⃗} and let F be the (finite) set of all stronger requirements that are ever satisfied. By induction, there is a stage s by which all requirements in F have been satisfied. If Γ is not principal then, by the same argument as before, there is a stage i > s at which there is a τ ∈ S with S_{τ} propositionally extending S_{σ_{i}} such that |τ| < f(i) and ¬γ(c⃗) ∈ S_{τ} for some γ ∈ Γ. We claim that no requirement stronger than R_{Γ,c⃗} acquires a target at a stage ⩾ i. Indeed, suppose otherwise and let R_{Γ′,c′} be the strongest requirement that acquires a target at a stage ⩾ i. Then this target is never canceled, and hence R_{Γ′,c′} is eventually satisfied. But no requirement stronger than R_{Γ,c⃗} is satisfied after stage s, so we have a contradiction. Thus, if R_{Γ,c⃗} does not have a target at stage i, then it acquires one at that stage. This target is never canceled, so R_{Γ,c⃗} is eventually satisfied.

Corollary 5.8. RCA_{0} ⊢ AMT → OPT.

Proof. The theory built in part 2 of Theorem 5.6 is atomic, and hence AMT also implies HYP.

Corollary 5.9. RCA_{0} ⊢ COH → OPT.

Proof. Jockusch and Stephan [1993] proved that every p-cohesive set (i.e., one that is cohesive for the collection of primitive recursive sets) has hyperimmune degree. Their proof goes through a degree theoretic characterization of the p-cohesive sets, so we give a more direct proof in RCA_{0}.

Let s_{n}^{e} be the least s such that Φ_{e} ↾ n + 1[s]↓, if such an s exists. So s_{n}^{e} ⩽ s_{n+1}^{e}. We assume the convention that Φ_{e}(n) ⩽ s_{n}^{e}. Let r_{0}^{e} = s_{0}^{e} and r_{n+1}^{e} = s_{∑_{i=0}^{n} r_{i}^{e}}^{e}.

For each e, let S_{e} be the set whose characteristic function is given by the sequence 0^{r_{0}^{e}}1^{r_{1}^{e}}0^{r_{2}^{e}}1^{r_{3}^{e}}0^{r_{4}^{e}}1^{r_{5}^{e}} … if Φ_{e} is total, and 0^{r_{0}^{e}}1^{r_{1}^{e}}0^{r_{2}^{e}}1^{r_{3}^{e}} … (1−i)^{r_{n−1}^{e}}i^{ω} if n is the least number such that r_{n}^{e} is undefined, and i = n mod 2. It is easy to see that the sequence S_{0}, S_{1}, … can be defined in RCA_{0}. Let C be cohesive for this sequence.

Let f be the C-recursive function defined by letting f(n) be the least m such that the sequence giving the characteristic function of C has n zeroes and n ones among its first m bits. We claim that f is not dominated by any recursive function. To show this, let Φ_{e} be total. Suppose C is almost contained in S_{e} (the case where C is almost contained in the complement of S_{e} being symmetric). It follows from the definition of S_{e} that for any m we can find y > x > m such that x, y ∈ C, there is no number strictly between x and y in C, and for some n we have x < ∑_{i=0}^{n} r_{i}^{e} and y ⩾ ∑_{i=0}^{n+1} r_{i}^{e}. Then f(x) > y > r_{n+1}^{e} = s_{∑_{i=0}^{n} r_{i}^{e}}^{e} ⩾ s_{x}^{e} ⩾ Φ_{e}(x). Since we can take m as large as we want, Φ_{e} does not dominate f.

Thus C has hyperimmune degree. This proof is obviously relativizable, so COH implies HYP, and hence OPT.

6 A Weak Form of AMT

In this section we consider the effect of adding effectiveness conditions on the types of a theory to AMT.

It follows from Theorem 5.1 that a complete decidable atomic theory whose types are uniformly recursive has a decidable atomic model. Theorem 5.2 shows that this result no longer holds if we weaken the hypothesis by assuming only that the types of T are recursive, but not necessarily uniformly so. On the other hand, Theorem 5.4 shows that it does come very close to holding under this weaker hypothesis. Recall that Theorem 5.4 says that if T is a complete decidable atomic theory such that all types of T are recursive, and d > 0, then T has a d-decidable atomic model. This fact leads us to consider the following weak version of AMT, which captures the hypothesis of Theorem 5.4 without explicit reference to recursiveness.

We say that partial types Γ and Δ of a theory T are equivalent if they imply the same formulas over T. Note that if Γ is a complete type equivalent to a partial type Δ then Γ is recursive in Δ. We say that a set S is a subenumeration of the types of a theory T if for every type Γ of T there is an i such that {φ | ⟨i, φ⟩} ∈ S is equivalent to Γ. If the types of T have a subenumeration then we say that they are subenumerable.

(AST) Atomic model theorem with Subenumerable Types: Let T be a complete atomic theory whose types are subenumerable. Then T has an atomic model.

Suppose the types of T are recursive. Let ψ_{0}, ψ_{1}, … enumerate the formulas in the language of T. Let S = {⟨e, ⋀_{i⩽s} ψ_{n}⟩ | Φ_{e}(n)[s] ↓= 1}. Then S is recursive and is a subenumeration of the types of T. Thus, by Theorem 5.2, AST does not hold in the ωmodel consisting of the recursive sets, so RCA_{0} ⊬ AST. Theorem 5.4 leads us to expect that AST may indeed be equivalent to the existence of relatively nonrecursive sets. We now show that this is the case, which is remarkable given the fact that the statement of AST does not use any recursion theoretic notions. We begin with the following recursion theoretic result.

Theorem 6.1 (Goncharov and Nurtazin [1973]; Harrington [1974]). Let T be a complete decidable atomic theory whose principal types are uniformly recursive. Then T has a decidable atomic model.

This result is proven by a priority argument. It has the following analogue in reverse mathematics which we prove by a similar argument using Shore blocking.

Theorem 6.2 (RCA_{0}). Let T be a complete atomic theory such that there is a listing of the principal types of T. Then T has an atomic model.

Proof. Let Γ_{0}, Γ_{1}, … be the principal types of T. Let S be the tree of standard Henkin constructions of models of T, with Henkin constants c_{i}. For σ ∈ S, let S_{σ} be the set of sentences associated with σ as in Definition 3.5. For σ ∈ S and n ∈ ℕ, let t(σ, n) be the least t such that ∃x_{n+1}, …, x_{m} ⋀_{φ∈S_{σ}} φ[c_{0}/x_{0}, …, c_{m}/x_{m}] ∈ Γ_{t}, where c_{m} is the largest constant mentioned in S_{σ}. For a path P of S, let t(P, n) = lim_{k} t(P ↾ k, n), which of course can be infinite. Note that if t(P, n) < ∞, then c_{0}, …, c_{n} has type Γ_{t(P,n)} in the model M of T determined by P. Thus, if t(P, n) < ∞ for all n, then M is atomic.

We define a path P of S as follows. Begin at the root node of S, and define n_{i,0} = i for all i ∈ ℕ. Suppose we have reached a node σ of length k. If σ has a single successor σˆ j then proceed to that successor and let n_{i,k+1} = n_{i,k} for all i. Note that in this case t(σˆ j, n) = t(σ, n) for all n.

If σ has two successors, then for j ∈ {0, 1}, let d_{σˆ j} be the least i ⩽ k such that t(σˆ j, n_{i,k}) > t(σ, n_{i,k}), or d_{j} = ∞ if there is no such i. If d_{σˆ 0} = d_{σˆ 1} then let j = 0. (Note that this case can happen only if d_{σˆ 0} = d_{σˆ 1} = ∞.) Otherwise, let j be such that d_{σˆ j} > d_{σˆ (1−j)}. Proceed to σˆ j. For i < d_{σˆ j}, let n_{i,k+1} = n_{i,k}. For i ⩾ d_{σˆ j}, let n_{i,k+1} = k + i.

Having thus defined P, let n_{i} = lim_{k} n_{i,k}, which can be infinite. We claim that the finite values of n_{i} are unbounded. In other words, for each n there is an i such that n < n_{i} < ∞.

Suppose otherwise, and let n be such that every n_{i} is either less than n or infinite. Let e be least such that n_{e,k} > n for some k. Such an e exists by Σ_{1}^{0}-induction (and the fact that there exist i, k such that n_{i,k} > n). Let i < e. Then i < d(P ↾ k + 1, n_{i}) for all k ⩾ n, so t(P ↾ k + 1, n_{i}) = t(P ↾ k, n_{i}) for all k ⩾ n, and hence t(P, n_{i}) < ∞. Let α_{i} be an atom in Γ_{t(P,n_{i})}. Let m be such that S_{P ↾m} contains α_{i}[x_{0}/c_{0}, …, x_{n_{i}}/c_{n_{i}}] for all i < e. Note that for all τ ≻ S_{P ↾m} on S and all i < e, we must have t(τ, n_{i}) = t(P, n_{i}).

Since n_{e} > n, we have n_{e} = ∞. So there is an l ⩾ n such that d_{P ↾l+1} ⩽ e. Let τ = P ↾ lˆ (1 − P (l)). By the construction of P we have d_{τ} < d_{P ↾l+1} ⩽ e, so for some i < e we have t(τ, n_{i}) > t(P ↾ l, n_{i}) = t(P, n_{i}), contradicting the last statement of the previous paragraph.

Thus the finite values of n_{i} are unbounded. So given n there is an i such n < n_{i} < ∞. For all sufficiently large k we must have d_{P ↾k} > i, and hence t(P ↾ k+1, n_{i}) = t(P ↾ k, n_{i}), which implies that t(P ↾ k + 1, n) = t(P ↾ k, n). So t(P, n) < ∞. Thus the model of T determined by P is atomic.

We are now ready to show that AST is equivalent to the existence of relatively nonrecursive sets.

Theorem 6.3. RCA_{0} ⊢ AST ↔ ∀X ∃Y (Y ⩽̸_{T} X).

Proof. First assume AST and fix a set X. The relativized form of the component of the proof of Theorem 5.2 provided as the proof of Theorem 5.2 of [CHKS] builds an X-recursive subtree T of 2^{<ℕ} with no dead ends, all of whose paths are X-recursive, but such that there is no X-recursive listing of the isolated paths of T . It is straightforward to check that this construction can be carried out in RCA_{0}. Translate T into a tree T as in the proof of Theorem 5.6. The 1-types of T correspond to the paths of T . But because the language of T has only unary relations, any n-type is simply a union of 1-types. It follows that T is atomic and its types are X-recursive. By the same argument as in the paragraph preceding this theorem, we can X-recursively define a subenumeration of the types of T. By AST, T has an atomic model M. We can form the set of all 1-types realized in M, that is, all principal 1-types of T. From this set we get a set consisting exactly of the isolated paths of T . This set is not X-recursive, so ∃Y (Y ⩽̸_{T} X).

Now assume ∀X ∃Y (Y ⩽̸_{T} X) and let T be a complete atomic theory whose types have a subenumeration S. Let D ⩽̸_{T} S. For each n, let T_{n} be the tree of n-types of T, which we can think of as a subtree of 2^{<ω}. Let T be the result of gluing together the T_{n} into a single tree by placing a copy of T_{n} with root 0^{n}1 for each n. Then T has no dead ends and the isolated paths of T are dense. Furthermore, each path of T (other than 0^{ω}) is a type of T equivalent to one of the rows of S, and hence is recursive in S. So for each path P of T we have D ⩽̸_{T} P. It is easy to check that the proof of Theorem 2.1 of Hirschfeldt [2006] can now be carried out in RCA_{0} to show that there is a D-recursive listing of the isolated paths of T , and hence a D-recursive listing of the principal types of T. It follows from Theorem 6.2 that T has an atomic model.

Thus AST is implied by all principles mentioned above other than the ones that follow from RCA_{0}, IΣ_{2} and BΣ_{2}, and implies none of the principles mentioned above other than the ones that follow from RCA_{0}. Indeed, AST is the weakest reasonable principle that does not hold in the ω-model consisting of the recursive sets.

7 Summary and Open Questions

We summarize most of our main results in Diagram 2. As before, double arrows are strict implications and negated arrows are nonimplications. We conclude with three open questions.

[figure: COH; SADS; Π_{1}^{0}G; |; |; |; _{WKL_{0}}; |; AMT; OPT; AST; _{RCA_{0}}]

Diagram 2

Question 7.1. Does COH (or CADS) imply AMT over RCA_{0}?

Question 7.2. Does CADS imply OPT over RCA_{0}?

Question 7.3. Is AMT r-Π_{2}^{1} conservative over BΣ_{2}?

References

[1] Chang, C. C.; Keisler, H. J. [1973], Model Theory, North-Holland, Amsterdam.

[2] Cholak, P. A.; Jockusch, Jr., C. G.; Slaman, T. A. [2001], On the strength of Ramsey’s Theorem for pairs. J. Symbolic Logic 66, 1–55.

[3] Chong, C. T.; Slaman, T. A.; Yang, Y. [ta], On the strength of Ramsey’s theorem for pairs. In preparation.

[4] Chong, C. T.; Yang, Y. [1998], Recursion theory in weak fragments of Peano arithmetic: A study of cuts. Proc. Sixth Asian Logic Conference, Beijing 1996, World Scientific, Singapore, 47–65.

[5] Chong, C. T.; Yang, Y. [2000], Computability theory in arithmetic: Provability, structure and techniques. Computability Theory and Its Applications: Current Trends and Open Problems, P. Cholak, S. Lempp, M. Lerman and R. A. Shore eds., Contemporary Mathematics 257, AMS, Providence, RI, 73–82.

[6] Conidis, C. [ta], Classifying Model Theoretic Properties, to appear in J. Symbolic Logic.

[7] Cooper, S. B. [1972], Jump equivalence of the Δ_{2}^{0} hyperhyperimune sets. J. Symbolic Logic 37, 598–600.

[8] Csima, B. F. [2004], Degree spectra of prime models. J. Symbolic Logic 69, 430–442.

[9] Csima, B. F.; Hirschfeldt, D. R.; Knight, J.; Soare, R. I. [2004], Bounding prime models. J. Symbolic Logic 69, 1117–1142.

[10] Downey, R.; Hirschfeldt, D. R.; Lempp, S.; Solomon, R. [2001], A Δ_{2}^{0} set with no infinite low subset in either it or its complement. J. Symbolic Logic 66, 1371–1381.

[11] Ershov, Yu. L.; Goncharov, S. S.; Nerode, A.; Remmel, J. B. (eds.); Marek, V. W. (assoc. ed.) [1998], Handbook of Recursive Mathematics, 2 vols., Elsevier, New York.

[12] Friedman, H. [1976], Systems of second order arithmetic with restricted induction I (abstract). J. Symbolic Logic 41, 557–558.

[13] Goncharov, S. S.; Nurtazin, A. T. [1973], Constructive models of complete decidable theories. Algebra Logic 12, 67–77.

[14] Groszek, M.; Slaman, T. A. [nd], Foundations of the priority method I: finite and infinite injury. Preprint.

[15] Hájek, P. [1993], Interpretability and fragments of arithmetic. Arithmetic, Proof Theory, and Computational Complexity (Prague, 1991), Oxford Logic Guides 23, Oxford Univ. Press, New York, 185–196.

[16] Hájek, P.; Pudlák, P. [1998], Metamathematics of First-Order Arithmetic, second printing. Perspect. Math. Logic, Springer-Verlag, Berlin.

[17] Harizanov, V. S. [1998], Pure computable model theory, in Ershov et al. [1998], vol. 1, 3–114.

[18] Harrington, L. [1974], Recursively presentable prime models. J. Symbolic Logic 39, 305–309.

[19] Herrmann, E. [2001], Infinite chains and antichains in computable partial orderings. J. Symbolic Logic 66, 923–934.

[20] Hirschfeldt, D. R. [2006], Computable trees, prime models, and relative decidability. Proc. Amer. Math. Soc. 134, 1495–1498.

[21] Hirschfeldt, D. R.; Shore, R. A. [2007], Combinatorial principles weaker than Ramsey’s Theorem for pairs. J. Symbolic Logic 72, 171–206.

[22] Hirst, J. L. [1987], Combinatorics in Subsystems of Second Order Arithmetic, PhD Dissertation, The Pennsylvania State University.

[23] Jockusch, Jr., C. G. [1972], Ramsey’s Theorem and recursion theory. J. Symbolic Logic 37, 268–280.

[24] Jockusch, Jr., C. G.; Soare, R. I. [1972], Π_{1}^{0} classes and degrees of theories. Trans. Amer. Math. Soc. 173, 33–56.

[25] Jockusch, Jr., C. G.; Stephan, F. [1993], A cohesive set which is not high. Math. Log. Quart. 39, 515–530 (correction in Math. Log. Quart. 43, 569).

[26] Lerman, M. [1983], Degrees of Unsolvability, Springer-Verlag, Berlin.

[27] Millar, T. S. [1978], Foundations of recursive model theory. Ann. Math. Logic 13, 45–72.

[28] Millar, T. S. [1983], Omitting types, type spectrums, and decidability. J. Symbolic Logic 48, 171–181.

[29] Mytilinaios, M. E. [1989], Finite injury and Σ_{1}-induction. J. Symbolic Logic 54, 212–221.

[30] Paris, J. B.; Kirby, L. A. S. [1978], Σ_{n}-collection schemas in arithmetic. Logic Colloquium ’77, Stud. Logic Foundations Math. 96, North-Holland, Amsterdam-New York, 199–209.

[31] Robinson, R. W. [1971], Interpolation and embedding in the recursively enumerable degrees. Ann. Math. (2) 93, 285–314.

[32] Simpson, S. G. [1999], Subsystems of Second Order Arithmetic, Perspect. Math. Logic, Springer-Verlag, Berlin.

[33] Soare, R. I. [1987], Recursively Enumerable Sets and Degrees, Springer-Verlag, Berlin.