Conservativity of ultrafilters over subsystems of second order arithmetic

Antonio Montalbán^{∗} Department of Mathematics

University of California, Berkeley Berkeley CA 94720 USA

Richard A. Shore^{∗∗} Department of Mathematics Cornell University Ithaca NY 14853

October 15, 2017

Abstract

We extend the usual language of second order arithmetic to one in which we can discuss an ultrafilter over of the sets of a given model. The semantics are based on fixing a subclass of the sets in a structure for the basic language that corresponds to the intended ultrafilter. In this language we state axioms that express the notion that the subclass is an ultrafilter and additional ones that say it is idempotent or Ramsey. The axioms for idempotent ultrafilters prove, for example, Hindman’s theorem and its generalizations such as the Galvin-Glazer theorem and iterated versions of these theorems (IHT and IGG). We prove that adding these axioms to IHT produce conservative extensions of ACA_{0} (+IHT), ACA_{0}^{+}, ATR_{0}, Π_{2}^{1}-CA_{0} and Π_{2}^{1}-CA_{0} for all sentences of second order arithmetic and for full Z_{2} for the class of Π_{4}^{1} sentences. We also generalize and strengthen a metamathematical result of Wang [1984] to show, for example, that any Π_{2}^{1} theorem ∀X∃Y Θ(X, Y) provable in ACA_{0} or ACA_{0}^{+} there are e, k ∈ ℕ such that ACA_{0} or ACA_{0}^{+} proves that ∀X(Θ(X, Φ_{e}(J^{(k)}(X))) where Φ_{e} is the eth Turing reduction and J^{(k)} is the kth iterate of the Turing or Arithmetic jump respectively. (A similar result is derived for Π_{3}^{1} theorems of Π_{1}^{1}-CA_{0} and the hyperjump.)

1 Introduction

An increasingly common phenomena in combinatorics is the use of higher order notions, objects and principles to prove combinatorial facts about the natural numbers ℕ (or some other countable set) and its subsets. One particularly fruitful such notion has been that of a (nonprincipal) ultrafilters on ℕ. (The definition of ultrafilters and most of the other notions mentioned in this introduction are given in §2. Hindman [2005] gives a brief survey of some examples. See Todorcevic [2010] and, especially, Hindman and Strauss [2012] for more extensive treatments.) These results provide a challenge to the analysis of the inherent complexity of such second order theorems in terms of the axioms (of second order arithmetic) needed to prove them and the computational complexity of the objects whose existence are asserted by such theorems. The study of such questions of complexity in general is the realm of reverse mathematics. (See the standard text on the subject, Simpson [2009] for a general introduction.)

∗Partially supported by NSF grant DMS-1363310 and by a Packard fellowship.

∗∗Partially supported by NSF Grant DMS-1161175.

One successful approach to this problem has been to replace the ultrafilters used in the proofs by countable approximations of various sorts that can be proven to exist in different axiomatic subsystem of second order arithmetic. (See for example Avigad [1998], Hirst [2004] and Towsner [2011], [2011a].) Another attractive idea is to attack the problem in a more wholesale fashion by expanding the language of second order arithmetic and the associated axiomatic systems in a way that enables one to carry out the proofs using ultrafilters but in a system that one can prove is conservative over the associated set of second order axioms. (For a set of sentences Γ in some language L and sets R and T of axioms the language L, we say that R is Γ-conservative over T if, for every Φ ∈ Γ, if R ⊢ Φ then T ⊢ Φ.) So, in our situation we want L to be an extension of the language of second order arithmetic in which we can talk about an ultrafilter is some reasonable way. We want Γ to be a natural subclass of the sentences of second order arithmetic containing theorems of interest. T should be a (standard) axiom system of second order arithmetic and R a natural extension of T to the language L. The system R should assert the existence of some type of ultrafilter and in it we should be able to carry out the proofs of the second order combinatorial theorems of interest. If we can then prove that R is Γ-conservative over T we will have shown that the theorems of interest are actually provable in the known second order theory T.

We first saw this approach carried out in Towsner [2014] who proved the desired results for (general) nonprincipal ultrafilters and several of the standard subsystems T of reverse mathematics (ACA_{0}, ATR_{0} and Π_{1}^{1}-CA_{0}). His approach was to extend the language by adding a unary predicate (for the ultrafilter) as well as some technical term formation rules to allow various natural operations using the ultrafilter to be expressed in the extension. He then defined axiom systems R extending T in which one might be able to carry out arguments using the ultrafilter. Finally, he used forcing for this language and proved in T that all the axioms of R were all forced to be true (as then are all their consequences in second order arithmetic). In the standard way, this then shows that R is conservative over T for all sentences of second order arithmetic. (Towsner points out that this result for ACA_{0}, as well as the very strong theory (Z_{2}) + Π_{∞}^{1}-DC_{0}, also follow from Enayat [2006] and that Kreuzer [2012] gives a proof for ACA_{0} and Π_{2}^{1} conservation using the functional interpretation.)

Unfortunately, most (if not all) of the classical and more recent examples of the applications of ultrafilters to second order combinatorics depend on the existence of ultrafilters with various special properties. Towsner provides two examples, Ramsey ultrafilters and divisible ultrafilters when the notion of divisibility is arithmetically definable, where his methods apply but no examples of proofs of known combinatorial theorems in the relevant systems. Historically, the basic and motivating example of uses of ultrafilters was the Galvin-Glazer proof of Hindman’s theorem and its many generalizations. Hindman’s theorem can be phrased in terms of a more complicated (Σ_{1}^{1} complete) divisibility property (called IP). So the existence of an ultrafilter all of whose members are IP would prove Hindman’s theorem. Towsner conjectures that such an assumption is conservative over ATR_{0}. We prove more below.

Hindman’s original proof and the direct reverse mathematical analyses of his theorem are all long and difficult combinatorial arguments. The Galvin-Glazer proof of Hindman’s theorem is a very short one based on the existence an algebraically defined type of ultrafilter called idempotent. (The algebra of ultrafilters on a countable set is based on an operation inherited from one in the underlying countable set such as + on ℕ.) Towsner then asks for which (of the standard) theories T is the existence of an idempotent ultrafilter conservative. (The point here is that every member of an idempotent ultrafilter is easily seen to be IP.)

Our goal in this paper is to answer these questions positively except for the fundamental one of whether the existence of idempotent ultrafilters is conservative over ACA_{0}. (Such a result would show that IHT is provable in ACA_{0} and so settle a long standing open problem.) We do prove, however, that it is conservative over a variation of Hindman’s theorem (Iterated Hindman’s theorem, IHT). Thus, in terms of our systems and languages, IHT is equiconsistent with the existence of an idempotent ultrafilter. Reverse mathematically, it is known that both Hindman’s theorem (HT) and the iterated version, IHT, imply ACA_{0} and are provable in ACA_{0}^{+} (Blass, Hirst, Simpson [1987]). Our methods also show that the existence of an idempotent ultrafilter (§4) or a Ramsey ultrafilter (§5) is conservative (for all sentences of second order arithmetic) over ACA_{0}^{+}, ATR_{0}, Π_{1}^{1}-CA_{0} and Π_{2}^{1}-CA_{0} and conservative over full Z_{2} for Π_{4}^{1} sentences.

Of course, as did Towsner, we must also define an extension of the language of second order arithmetic to include ways of talking about and using the intended ultrafilters. We also use forcing notions designed so that the generic objects will be ultrafilters with the properties we want. Our proofs of conservativity take the semantic approach of analyzing the structure for our extended language defined from a generic object as the intended ultrafilters rather than the relation between provability and forcing.

As we were writing this paper, we found that Kreuzer [2015] had proved some of our results in a different (higher order) setting and by proof theoretic methods to get conservation results over systems like ACA_{0} for Π_{2}^{1} sentences and had extended them to minimal idempotent ultrafilters and so to applications to other well known combinatorial principles [2015a]. We present the standard ultrafilter proof of IHT (and so some generalizations as well) in our system (ACA_{0}^{IU}) in Theorem 3.3. We also give another example of a standard proof of the Milliken-Taylor theorem using ultrafilters in our system in Theorem 3.4. Our general conservation result then shows that it is provable from IHT (Hirst [2004]).

Most applications of ultrafilters to combinatorics, however, use ultrafilters with more properties than idempotence and/or considerations of extra structural features beyond addition on ℕ or, more generally, multiplication in various semigroups. In future work, we hope to apply some of the ideas in this paper to another approach to conservation results that will handle additional properties such as minimality for ultrafilters and additional structure on the underlying algebra as well as a more robust language and setting for working with the ultrafilters. We then hope to apply this approach to well known combinatorial theorems such as Gowers’ Fin_{k} Theorem and the Infinite Hales-Jewett Theorem.

2 Definitions and Notations

We use one of the common notations to view a single set X as a sequence of sets ⟨X^{[n]}⟩ where X^{[n]} = {i| ⟨n, i⟩ ∈ X}. We let X^{[<n]} = {⟨j, i⟩ ∈ X|j < n} and use X̄ to denote the complement of X. The set of finite subsets of X is denoted by [X]^{<ω}. We denote the standard natural numbers by ℕ.

Note that all sets and structures considered will be countable.

2.1 Subsystems of Second Order Arithmetic

We first briefly review the five standard systems of reverse mathematics as well as a couple of other systems that we will use. Details, general background and results can be found in Simpson [2009], the standard text on reverse mathematics. Each of the systems is given in the (two sorted) language L of second order arithmetic, that is, the usual first order language of arithmetic augmented by set variables with their quantifiers and the membership relation ∈ between numbers and sets. A structure for this language is one of the form M = ⟨M, S, +, ×, <, 0, 1, ∈⟩ where M is a set (the set of “numbers” of M) over which the first order quantifiers and variables of our language range; S ⊆ 2^{M} is the collection of subsets of “numbers” in M over which the second order quantifiers and variables of our language range; + and × are binary functions on M; < is a binary relation on M while 0 and 1 are members of M. We also use ω to denote the set of numbers in such a structure in many familiar notations such as writing 2^{<ω} to mean the set of all finite binary strings where we are taking for granted some standard coding of binary strings by numbers of the structure. Indeed, in general, when we talk about finite sets or sequences of elements in M we are assuming some standard coding in the usual reverse mathematical style. Thus M^{<ω} is the collection of all finite sequences in M and [M]^{<ω} is the collection of all finite sets in M.

Each subsystem of second order arithmetic that we consider contains the standard basic axioms for +, ·, and < (which say that M is an ordered semiring). In addition, they all include a form of induction that applies only to sets (that belong to the model):

(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 five standard systems are defined by adding various types of set existence axioms to P_{0}. All but one are determined by comprehension axioms for a standard class Γ of formulas. Note that these formulas may have free set or number variables. As usual the existence assertion ∃X.... of the axiom is taken to mean that for each instantiations of the free variables there is an X as described.

(RCA_{0}) Recursive Comprehension Axioms: This is a system just strong enough to prove the existence of the computable sets. 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}) (φ(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.

(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 (i.e. Σ_{n}^{0} for some n) φ in which X is not free.

This system is equivalent to the totality of the Turing jump operator, i.e. for every X, X′ exists. The next system 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 for each arithmetic formula Θ(n, Z): If ⟨X, <_{X}⟩ is (a code for) a wellordering, then there is a set Y such that, for each x ∈ X, ∀n(n ∈ Y^{[x]} ⇔ Θ(n, Y^{[<x]}).

The last of the standard systems is characterized by the comprehension axiom for Π_{1}^{1} formulas:

(Π_{1}^{1}-CA_{0}) This system consists of RCA_{0} plus the Π_{1}^{1} comprehension axioms: ∃X ∀k (k ∈ X ↔ Φ(k)) for every Π_{1}^{1} formula Φ in which X is not free.

(Z_{2}) Full second order arithmetic, Z_{2} consists of RCA_{0} plus all the Π_{n}^{1}-CA_{0}, i.e. the comprehension axioms as above but for Π_{n}^{1} formulas φ for every n ∈ ℕ.

We also we refer to a system between ACA_{0} and ATR_{0} that corresponds to the ability to iterate the Turing jump ω many times, i.e. the totality of the ω-jump operator.

(ACA_{0}^{+}) This system consists of RCA_{0} plus the axiom ∀X∃Y (Y^{[0]} = X & ∀n > 0(Y^{[n]} = (Y^{[n−1]})′)). (Here we take some standard definition of the Turing jump in first order arithmetic.) The axiom says we can iterate the Turing jump through the numbers (of the model).

The above axiom systems are strictly ordered in the obvious way. We also need to use some choice principles whose relationships to the ones above are not so easily categorized. (See Simpson [2009].)

(strong Σ_{n}^{1}-DC_{0}) For every Σ_{n}^{1} formula Φ(k, X, Y), ∃Z∀k∀Y (Φ(k, Z^{[<n]}, Y) → Φ(k, Z^{[<n]}, Z^{[n]}).

We note for later use that Π_{1}^{1}-CA_{0} implies (indeed is equivalent to) strong Σ_{1}^{1}-DC_{0} and Π_{2}^{1}-CA_{0} implies (indeed is equivalent to) strong Σ_{2}^{1}-DC_{0} (Simpson [2009, VII.6.9]).

2.2 Combinatorics

Definition 2.1. Let M be a structure for the language L of second order arithmetic with M ⊨ RCA_{0}. An M-filter is a nonempty subset F of S which is closed upward and under intersection, i.e. if X, Y ∈ S, X ⊆ Y and X ∈ F, then Y ∈ F; and if X, Y ∈ F then X ∩Y ∈ F. An M-filter is principal if there is an A ∈ S such that F = {X ∈ S|X ⊇ A}; otherwise it is nonprincipal. A nonprincipal M-filter U is an M-ultrafilter if for every A ∈ S, A ∈ U or Ā ∈ U.

Definition 2.2. An M-ultrafilter U is Ramsey if for every partition ⟨X_{n}⟩ ∈ S of M into nonempty pairwise disjoint sets such that X_{n} ∉ U for every n, there is a Z ∈ U such that |X_{n} ∩ Z| = 1 for every n.

Before we can, even classically, define a notion of an idempotent ultrafilter we need a number of definitions.

Definition 2.3. A (partial) semigroup (Z,∗) is a set Z with a (partial) binary operation

∗ which is associative. An idempotent is an element x such that x ∗ x = x. A partial semigroup is directed if, for every finite sequence x_{0},…, x_{n} of elements of Z, there is a y ∈ Z such that y ≠ x_{i} for each i ≤ n and x_{0} ∗ y, …, x_{n} ∗ y are all defined. It is left-cancelative, if, for every x, y, z with x ∗ y = x ∗ z, y = z. A basic sequence in a partial semigroup is a finite or infinite sequence ⟨x_{i}⟩ of pairwise distinct elements such that x_{n_{0}} ∗ x_{n_{1}} ∗ … ∗ x_{n_{k}} is defined for every finite sequence n_{0} < … < n_{k}.

Notation 2.4. For X ⊆ M, FS(X) = {x_{0} + x_{1} + … + x_{n}| for any ⟨x_{i}⟩ ∈ M^{<ω} with x_{0} < x_{1} < … < x_{n} each in X}. We let X +n = {x+n|x ∈ X} and X −n = {m|n+m ∈ X}. For X = {D_{i}} ⊆ [M]^{<ω}, F U(X) = {∪{D_{i}|i ∈ E}| E ∈ [M]^{<ω}}. We define X ∗ n and X/n similarly for X ⊆ Z and n ∈ Z for a partial semigroup (Z, ∗). We extend the operations F S(X) and F U(X) to basic sequences X = ⟨x_{i}⟩ in a semigroup (Z, ∗) by setting [X] = {x_{n_{0}} ∗ ⋯ ∗ x_{n_{k}}|n_{0}, n_{1}, ⋯, n_{k} an increasing sequence in X^{<ω}}.

For background information and intuition for some of the standard terminology, we now describe some notions in the setting of classical mathematics.

One can extend the ∗ operation on a partial semigroup (Z, ∗) to a total operation ∗ on a subclass γZ of the class βZ of all ultrafilters over Z: γZ = {U ∈ βZ|(∀x ∈ Z)({y ∈ Z|x ∗ y is defined} ∈ U}. For U, V ∈ γZ, U ∗ V = {A ⊆ Z|{x ∈ Z|{y ∈ Z|x ∗ y ∈ A} ∈ V ∈ U}. (One can read this as the collection of subsets A of Z such that, for almost all x (w.r.t. to U) and almost all y (w.r.t. V), x ∗ y ∈ A.) One can check that this operation is total and associative on γZ. (See e.g. Todorcevic [2010, 2.1 and 2.2] for all of this.) An ultrafilter U ∈ γZ is then idempotent if U ∗ U = U.

After we introduce our extension of second order arithmetic in §3, we will give an axiom (AU5) which is easily seen to be a translation of this definition into our language.

We now state several versions of, and variations on, Hindman’s theorem in structures M for second order arithmetic without considering, at this point, the axiom systems needed to prove them. The first is what is usually called Hindman’s Theorem (HT) (or the Finite Sums Theorem). The second is the Finite Union Theorem (FU) but also sometimes called Hindman’s Theorem. The third is the analog for directed partial semigroups and is usually called the Galvin-Glazer Theorem (GG). Each one asserts the existence of a type of homogeneous set for various colorings. We then state the (obviously at least as strong) variations of these theorems for sequences of colorings. Finally, we prove the equivalences for the iterated versions and note that the proofs specialize to the ones for the ordinary versions of these theorems.

Theorem 2.5 (Hindman’s Theorem (HT)). If f is a finite coloring of M, i.e. f : M → k, then there is an infinite X ⊆ M such that F S(X) is monochromatic, i.e. there is an i < k such that for every finite sum z of distinct elements of X, f(z) = i. Such a set is called homogeneous for f.

Theorem 2.6 (Finite Union Theorem (FU)). If f is a finite coloring of [M]^{<ω}, then there is an infinite subset X of [M]^{<ω} such that F U(X) is monochromatic, i.e. all finite unions of members of X have the same color. Moreover, we may choose X = ⟨x_{i}⟩ to be a block sequence, i.e. ∀i(max x_{i} < min x_{i+1}). Such a set is called homogeneous for f.

Of course, FU is equivalent (over RCA_{0}) to the same theorem for any countable set W in place of M.

Theorem 2.7 (Galvin-Glaser Theorem (GG)). If (Z, ∗) is a directed partial semigroup with no idempotents or which is left-cancelative and f is a finite coloring of Z, then there is an infinite basic sequence X = ⟨x_{n}⟩ in S such that [X] is (necessarily infinite and) monochromatic. Such a set is called homogeneous for f.

Theorem 2.8 (Iterated Hindman’s Theorem (IHT)). Given a sequence ⟨f_{n}, k_{n}⟩ where f_{n} is a k_{n} coloring of M, there is an infinite sequence X = ⟨x_{i}⟩ from M such that, for each n, F S({x_{i}|i ≥ n}) is monochromatic for f_{n}. Such a set is called homogeneous for ⟨f_{n}⟩.

Note that this theorem is equivalent (over RCA_{0}) to the one where all k_{n} = 2.

Theorem 2.9 (Iterated Finite Union Theorem (IFU)). Given a sequence ⟨f_{n}, k_{n}⟩ where f_{n} is a k_{n} coloring of [M]^{<ω}, there is an infinite block sequence X = ⟨x_{i}⟩ from [M]^{<ω} such that, for each n, F U({x_{i}|i ≥ n}) is monochromatic for f_{n}. Such a set is called homogeneous for ⟨f_{n}⟩.

Again this theorem is equivalent (over RCA_{0}) to the one where all k_{n} = 2. Of course, IFU implies the same theorem for any countable set W in place of M.

Theorem 2.10 (Iterated Galvin-Glaser Theorem (IGG)). If (Z, ∗) is as in Theorem 2.7, and we are given a sequence ⟨f_{n}, k_{n}⟩ where f_{n} is a k_{n} coloring of Z, then there is an infinite basic sequence X = ⟨x_{n}⟩ in Z such that for each n, [{x_{i}|i ≥ n}] is monochromatic for f_{n}. Such a set is called homogeneous for ⟨f_{n}⟩.

We now wish to prove that HT, FU and GG are equivalent over RCA_{0} as are the iterated versions. These equivalences were all essentially known to Hindman and others although they were not working in the framework of RCA_{0}. There are proofs of these equivalences for HT, FU and GG in Bergelson and Hindman [1993, Lemma 2.1] which are described there as “well known among aficionados” and are also outlined in Hindman and Strauss [2012, §5.5, Ex. 5.2.1-5.2.4] but the proofs in both cases for GG are only for semigroups. The ones for partial semigroups suggested in Ex 5.2.5 and Todorcevic [2010] for partial semigroups uses ultrafilters. We present similar proofs for the iterated versions in RCA_{0} which also specialize to the noniterated versions. We begin with a simple Lemma.

Lemma 2.11 (RCA_{0} (Hindman [1972], Lemma 2.2 )). If F ∈ [M]^{<ω} and |F | = 2^{n} then there is a G ⊆ F such that 2^{n}|ΣG.

Proof. As Hindman [1972] points out this is a simple induction. It clearly works in RCA_{0}.

Now for a bit more complicated Lemma that we need for the analysis of IGG.

Lemma 2.12. If (Z, ∗) is a directed partial semigroup it has an infinite basic sequence. If Z has no idempotents or is left-cancelative, then there is an infinite basic sequence Y = ⟨y_{n}⟩ in Z such that the products y_{n_{0}} ∗ ⋯ ∗ y_{n_{k−1}} = Πū and y_{m_{0}} ∗ ⋯ ∗ y_{m_{l−1}} = Πv̄ are all distinct for n_{k−1} < m_{0} which we write as ū < v̄ where ū = ⟨y_{n_{0}}, …, y_{n_{k−1}}⟩ and v̄ = ⟨y_{m_{0}}, …, y_{m_{l−1}}⟩.

Proof. If Z is directed we can easily build a basic sequence by induction: Given y_{i}, i < n, directedness shows that there is a z (indeed infinitely many) such that Πū ∗ z is defined for all ū with n_{k−1} < n. So we may take any such z as y_{n}.

If Z is left-cancelative we also want maintain the inductive hypothesis that Πū ≠ Πv̄ for all ū < v̄ with the last component of v̄ having subscript less than n. Now, for each such ū < v̄, there can be at most one z with ū = v̄ ∗ z as if ū = v̄ ∗ z_{1} = v̄ ∗ z_{2} then z_{1} = z_{2} since Z is left-cancellative. Thus we can choose a z as required to continue the block sequence and such that for all such ū < v̄, ū ≠ v̄ ∗ z and so maintain our inductive hypothesis by taking any such a z as y_{n}.

If Z has no idempotents let Y be any infinite basic sequence. If there is a z such that there are infinitely many k for which there are ū with y_{n_{0}} = k and Πū = z, then we can find ū_{i} with Πū_{i} = z and ū_{i} < ū_{j} for i < j. Since Y is a basic sequence, all the products Πu_{0} ∗ ⋯ ∗ Π_{u_{n}} i.e. all the z^{n} are defined. If they are all distinct then ⟨z^{2^{i}}⟩ is a basic sequence as desired. Otherwise there are n and m such that z^{n} = z^{m} and so the subsemigroup Ẑ generated by z is finite (of size at most m). We claim it has an idempotent for a contradiction: If not, Let t ≤ m be the size of the smallest subsemigroup Z′ of Ẑ generated by some z^{k} = w which has no idempotent. Clearly t > 1 and so there are p < q ≤ t such w^{p} = w^{q}. Now w^{q−p} ∗w^{p} = w^{q} = w^{p} and so by repeated multiplication by w^{p}, w^{q−p} ∗ w^{p·l} = w^{p·l} for every l ≤ t. If the subsemigroup generated by w has size less than t it (and so Ẑ) would have an idempotent. Thus it has size t and is all of Z′. In particular, some w^{p·l} = w^{q−p} and so is our desired idempotent.

Finally, we have the case that for every z there are only finitely many k such that there are ū with y_{n_{0}} = k and Πū = z. With this assumption we can easily thin out Y to satisfy the conclusions of the Lemma. Suppose we have y_{m_{0}}, …, y_{m_{l}} and a_{l} so that Πū ≠ Πv̄ for all ū from this sequence so far and all v̄ from Y with first component v_{i} with i ≥ a_{l}. By our assumption we may now take m_{i+1} = a_{l} and choose a_{l+1} large enough to continue the induction. The new basic sequence clearly has the desired property.

Proposition 2.13 (RCA_{0}). IHT, IFU and IGG are all equivalent as are HT, FU and GG as are HT_{n}, FU_{n} and GG_{n} for each n ∈ M where each of these subscripted versions is the restriction of the full theorem to n-colorings.

Proof. We assume IHT and prove IFU. Let ⟨f_{n}, k_{n}⟩ be as in the hypothesis of IFU and define g_{n} from f_{n} by g_{n}(x) = f_{n}(B_{x}) where B_{x} is the set of a_{i} which appear in the binary expansion of x, i.e. if x = Σ2^{a_{i}}. Now let X = ⟨x_{i}⟩ be homogeneous for ⟨g_{n}, k_{n}⟩ as in IHT. We define a sequence ⟨y_{i}⟩ by recursion and show it is homogeneous for ⟨f_{n}, k_{n}⟩:

In addition to the y_{i} we define z_{i} ∈ F S{x_{j}|j ≥ n} such that y_{i} = B_{z_{i}}. We begin with z_{0} = x_{0} and y_{0} = B_{z_{0}}. Assume for the recursion step that we have y_{i} = B_{z_{i}} for i ≤ n defined as desired. By Lemma 2.11, we may choose n < j_{0} < ⋯ < j_{m} so that if z_{n+1} = Σx_{j_{k}} and y_{n+1} = B_{z_{n+1}} then max y_{n} < min y_{n+1}.

As for the required homogeneity, consider any n ≤ i_{0} < ⋯ < i_{m}. As ⟨y_{i}⟩ is a block sequence and y_{i} = B_{z_{i}}, the definition of g_{n} says that f_{n}(∪{y_{i_{k}}|k ≤ m}) = g_{n}(Σ{z_{i_{k}}|k ≤ m}).

As z_{i_{k}} ∈ F S{x_{j}|j ≥ i_{k}} ⊆ F S{x_{j}|j ≥ n} the fact that F S{x_{j}|j ≥ n} is monochromatic for g_{n} implies that F U({x_{i}|i ≥ n}) is monochromatic for f_{n} as required.

That HT (HT_{n}) implies FU (FU_{n}) now follows by the same proof applied to a single coloring f of M^{<ω}.

Next we assume IFU and prove IGG. Let an appropriate semigroup (Z, ∗) be given along with a sequence ⟨f_{n}, k_{n}⟩ of colorings as in IGG. We begin with an infinite basic sequence Y as given by Lemma 2.12. For F = {y_{n_{0}}, …, y_{n_{k−1}}} let g_{n}(F) = f_{n}(y_{n_{0}} ∗ ⋯ ∗ y_{n_{k−1}}). Now choose a block sequence X = ⟨x_{i}⟩ homogeneous for the g_{n} in the sense of IFU. The definition of the g_{n} and the properties of the sequences now show that if x_{i} = {y_{n_{i,0}}, …, y_{n_{i},n_{k_{i}−1}}} then ⟨z_{i}⟩ is homogeneous for f_{n} in the sense of IGG where z_{i} = y_{n_{i,0}} ∗ ⋯ ∗ y_{n_{i},n_{k_{i}−1}}.

As above, this proof specializes to show that FU (FU_{n}) implies GG (GG_{n}).

Finally, for the implication from IGG to IHT, just note that if we take our semigroup to be ⟨M, +⟩ (which is left-cancelative) and consider any ⟨f_{n}, k_{n}⟩ as in the hypothesis of IHT then it is also a sequence of colorings in the sense of IGG. It is then clear that any homogeneous set in the sense of IGG is also homogeneous in the sense of IHT. The same observation shows that GG (GG_{n}) implies HT (HT_{n}).

3 Extended Language

To be able to work with ultrafilters in the setting of reverse mathematics and second order arithmetic, we must extend our language L of second order arithmetic. The expressiveness that we need introduces, at least, a way of talking about an individual third order object such as a specified ultrafilters U. To do this we extend L by adding on a unary function symbol δ_{U} from sets to sets. This introduces new terms such as δ_{U}(X) (or δ_{U}^{k}(X) for an k-fold iteration with k ∈ ℕ) and so we have new atomic formulas such as n ∈ δ_{U}(X), Y = δ_{U}(X) and δ_{U}(X) = δ_{U}(Y).

The structures for this language L^{U} are formed from ones M = ⟨M, S, +, ×, <, 0, 1, ∈⟩ for L and a subset U of S to get a structure M^{U} = ⟨M, S, U, +, ×, <, 0, 1, ∈⟩. The semantics for L^{U} are determined by fixing a U ⊆ S and interpreting δ_{U}(X) as the subset of M given by 0 ∈ δ_{U}(X) ⇔ X ∈ U and n + 1 ∈ M ⇔ X^{[n]} ∈ U . Of course, we must make sure that this operation is well-defined and the the class S of subsets of M which form the sets of M is closed under δ_{U}(X) to get a structure for L^{U}.

We can now say in L^{U}, for example, that U is an M-ultrafilter or is any of a variety of special M-ultrafilters (or a Z-ultrafilter for any Z ∈ S). We incorporate these sentences as axioms for our extensions R of theories T of second order arithmetic that essentially assert the existence of an ultrafilter (with some additional properties) to form the desired conservative extensions. The following sentences of L^{U} say that U is a nonprincipal ultrafilter:

AU1 ∀X(0 ∈ δ_{U}(X) → ∀x∃y(y > x & y ∈ X). (Every set in U is infinite.)

AU2 ∀X∀Y (X ⊆ Y & 0 ∈ δ_{U}(X) → 0 ∈ δ_{U}(Y)). (U is closed under supersets.)

AU3 ∀X∀Y ∀Z(0 ∈ δ_{U}(X) & 0 ∈ δ_{U}(Y) & X ∩ Y = Z → 0 ∈ δ_{U}(Z)). (U is closed under intersections.)

AU4 ∀X∀Y (Y = X̄ → (0 ∈ δ_{U}(X) ∨ 0 ∈ δ_{U}(Y). (For every X, X or X̄ is in U.)

The next axiom guarantees that U satisfies the translation of the classical definition of an ultrafilter being idempotent as given after Notation 2.4.

AU5 ∀X∀Y ∀Z(0 ∈ δ_{U}(X) & ∀n(Y^{[n]} = X − n)) & ∀i(i ∈ Z ⇔ i + 1 ∈ δ_{U}(Y)) → 0 ∈ δ_{U}(Z)). (If X ∈ U then {{n|(X − n) ∈ U} = {n|{y|{n + y} ∈ U} ∈ U.)

We now explain how to extend theories T of second order arithmetic.

Definition 3.1. If T is theory of second order arithmetic specified by a set of axioms as well as axiom schemes giving an axiom involving φ for each φ ∈ Γ for some syntactically defined class Γ (in the usual way as for comprehension axioms), then T^{IU} (T^{U}) is the same set of axioms as T but we replace the class Γ by the class of formulas of L^{U} with the same syntactic specification with the understanding, of course, that formulas of the form n ∈ δ_{U}(X), Y = δ_{U}(x) and δ_{U}(X) = δ_{U}(Y) are atomic. (For example, For ACA_{0}^{IU} we include comprehension axioms for all arithmetic formulas in the language L^{U}.) In addition, T^{IU} (T^{U}) has axioms AU1 − AU5 (AU1 − AU4).

Remark 3.2. For those familiar with the extended language of Towsner [2014], it is not hard to see that ours is at least as expressive as his. His language introduces second order terms T_{t} for each second order term T and each first order term t and a unary predicate U on second order terms written T ∈ U. The intended semantics for the T_{t} are expressed by the added axioms saying that n ∈ T_{t} ⇔ ⟨t, n⟩ ∈ T. We can convert his formulas to ours by replacing an arbitrary new atomic formula of the form X ∈ U by 0 ∈ δ_{U}(X), ones of the form (… (X_{t_{1}})_{t_{2}})_{t_{3}} …)_{t_{n}} ∈ U by ⟨t_{1}, …, t_{n}⟩ + 1 ∈ δ_{U}(X) and ones of the form s ∈ (… (X_{t_{1}})_{t_{2}})_{t_{3}} …)_{t_{n}} by ⟨t_{1}, …, t_{n}, s⟩ ∈ X. It is not immediately obvious that (in ACA_{0}) one can express formulas such as n ∈ δ_{U}^{k}(X) in his language.

In the next section we will prove conservation results for T^{IU} over T for many of the standard systems of reverse mathematics. To see that this is meaningful in the sense of possibly showing that proofs using idempotent ultrafilters can be replaced by ones in second order arithmetic otherwise at the same level of complexity, we show how to convert the standard proof of IHT using an idempotent ultrafilters to one in ACA_{0}^{IU}.

We mimic the standard Galvin-Glazer proof using an idempotent ultrafilters on ⟨M, +⟩ (as in Todorcevic [2010, Theorem 2.20]). Like many other proofs using ultrafilters, this proof uses an inductive construction choosing sets in the ultrafilter in an inductive fashion that depends at each step on the previously chosen sets. In general this is not a procedure that can be done in ACA_{0}^{IU} (even if the inductive step is arithmetic). (On its face, such a construction may use something like strong Σ_{1}^{1}-DC_{0} and certainly some are provably beyond the reach of ACA_{0}^{IU}.) We make one simple change for this construction. Instead of choosing the successive sets in the ultrafilter, we describe the results of all possible paths through the inductive argument in advance. This allows us to work inside ACA_{0} after using only one instance of our operator δ_{U} instead of something that seems like a dependent sequence of choices. This type of argument will play a crucial role in the analysis of our notion of forcing and our conservation results in §4. Two different approaches to this problem appear in our treatment of another example (the Milliken-Taylor theorem) in Theorem 3.4 in ACA_{0}^{IU} and in Theorem 4.16 in stronger systems but ones still weaker than Σ_{1}^{1}-DC_{0}.

Theorem 3.3. ACA_{0}^{IU} ⊢ IHT.

Proof. We work in ACA_{0}^{IU}. Let ⟨f_{k}, n_{k}⟩ be a sequence of colorings of M as in the statement of IHT (Theorem 2.8). We recursively define by induction on levels a tree of sequences σ labeled with sets X_{σ} which will be downward nested with increasing σ. We begin with the root ∅ labeled with M. Given σ of length 2k the immediate successors of σ are σˆ i for i < n_{k} and we set X_{σˆ i} = {x ∈ X_{σ}|f_{k}(x) = i}. If σ is of length 2k + 1, its immediate successors are σˆ x with x ∈ X_{σ} and X_{σˆ x} = {y|y, x + y ∈ X_{σ}}. We now let X be the code of the sets X_{σ}. We suppress the recursive coding of strings as numbers as usual but note that for convenience we assume that the numbers which are codes for strings σ begin with 1 rather than 0. (This allows us to avoid the notational problems engendered by reserving δ_{U}(X)(0) to code the membership of X in U and using the numbers larger than 0 for the columns of X.)

Using δ_{U}(X) and the tree above, we now arithmetically (or indeed as we shall see recursively) define a path in the tree with nodes σ_{n} at level n and a sequence x_{2n+2} ∈ X_{σ_{2n+1}} that will satisfy the requirements for the given instance of IHT. We begin with σ_{0} = ∅. Given σ_{2k} we let σ_{2k+1} = σ_{2k}ˆ i for the least i < n_{k} such that σ_{2k}ˆ i ∈ δ_{U}(X) (i.e. X_{σ_{2k}ˆ i} ∈ U). Given σ_{2k+1} we let σ_{2k+2} = σ_{2k+1}ˆ x for the least x > 0, x_{2k+1} (necessarily in X_{σ_{2k+1}}) such that σ_{2k+1}ˆ x ∈ δ_{U}(X) (i.e. X_{σ_{2k+1}ˆ x} ∈ U) and let x_{2k+2} = x. In either case, if there is no such extension the sequences terminates.

We now prove by induction on n that σ_{n} ∈ δ_{U}(X) (i.e. X_{σ_{n}} ∈ U) and the sequences of strings σ and sets X_{σ} never terminate. Given σ_{2k} ∈ δ_{U}(X), there are only n_{k} many immediate successors σ_{2k}ˆ i and the corresponding X_{σ_{2k}ˆ i} partition X_{σ_{2k}}. As U is an ultrafilter, one of them must be in U. More formally, one of the σ_{2k}ˆ i is in δ_{U}(X) by Axiom AU3 and so there is a least one i which gives us σ_{2n+1} = σ_{2n}ˆ i with σ_{2n+1} ∈ δ_{U}(X) as required. (Note that arithmetic comprehension for formulas of L^{U} and open induction easily imply that U is closed under M-finite intersections.) Given σ_{2k+1} ∈ δ_{U}(X), the axiom AU5 for U being an idempotent ultrafilters, guarantees that for some (indeed U many) x ∈ X_{σ_{2n+1}}, σ_{2n+1}ˆ x ∈ δ_{U}(X) (i.e. X_{σ_{2n+1}ˆ x} ∈ U). (The axiom says that, as X_{σ_{2n+1}} ∈ U, {x|X_{σ_{2n+1}} − x ∈ U} = {x|{y|x + y ∈ X_{σ_{2n+1}}} ∈ U} ∈ U and so by AU3 {x| {y ∈ X_{σ_{2n+1}}|x + y ∈ X_{σ_{2n+1}}} ∈ U}} ∈ U. For any x in this last set, X_{σ_{2n+1}ˆ x} = {y|y, x + y ∈ X_{σ_{2n+1}}} ∈ U as required.) Thus there is a least one x and σ_{2n+2} = σ_{2n+1}ˆ x and x_{2n+2} = x for the least such x.

Finally we prove that the sequence of x_{2n+2} witnesses the desired conclusion of IHT. Consider any m. We want to prove that F S({x_{2n} + 2|n ≥ m}) ⊆ X_{σ_{2m+1}} and so is monochromatic for f_{m} as if σ_{2mˆ i} = σ_{2m+1,} f_{m}(x) = i for all x ∈ X_{σ_{2m+1}} by the definition of σ_{2m+1}. We claim that F S({x_{2n+2}|n ≥ m}) is contained in X_{σ_{2m+1}} and so monochromatic to i for f_{m}. Consider any sum x = x_{2n_{0}+2} +x_{2n_{1}+2} +…+x_{2n_{k}+2} with m ≤ n_{0} < … < n_{k}. We prove by induction on k that x ∈ X_{σ_{2n_{0}+1}} and so x ∈ X_{σ_{2m+1}} as n_{0} ≥ m and the X_{σ_{n}} are downward nested. We have the base case k = 0 by the argument above taking m = n_{0}. Consider now the case that k > 0 and let z = x_{2n_{1}+2} +…+x_{2n_{k}+2}. By induction z ∈ X_{σ_{2n_{1}+2}} ⊆ X_{σ_{2n_{0}+1}ˆ x_{2n_{0}+2}} = {y|y, x_{2n_{0}+2}+y ∈ X_{σ_{2n_{0}+1}}}. Thus x = x_{2n_{0}+2}+z ∈ X_{σ_{2n_{0}+1}} as required.

As another example of a common ultrafilter proof of a standard combinatorial principle that can be done in ACA_{0}^{IU}, we consider the proof of the Milliken-Taylor theorem in Bergelson and Hindman [1989, Corollary 2.4]. This theorem is a combination of Ramsey’s theorem for r-colorings of size k sets of natural numbers and Hindman’s theorem for finite sums.

Theorem 3.4 (Milliken-Taylor). Let k, r ∈ ℕ and let [ℕ]^{k} = ∪{A_{i}|i < r}. Then there exists an i < r and an increasing sequence ⟨x_{i}⟩ such that whenever −1 = n(0) < n(1) < ⋯ < n(k) and, for 1 ≤ t ≤ k, a_{t} ∈ F S(⟨x_{m}|n(t − 1) + 1 ≤ m ≤ n(t)⟩), {a_{1}, …, a_{k}} ∈ A_{i}.

Proof (in ACA_{0}^{IU}). We denote by MT(k) the assertion of the theorem for fixed k (but for all r). We indicate how to read the proof in Bergelson and Hindman [1989] as one for a model M^{U} of ACA_{0}^{IU}. Note that while we may take r to be any number in the model, we restrict ourselves to proving MT(k) for standard k so that we can handle the backward induction on k in Bergelson and Hindman [1989], Theorem 2.3] in ACA_{0}^{IU}. We fix both k ∈ ℕ and r ∈ M for the argument.

The basic tool in the proof is a form of Ramsey’s theorem for k-tuples (and r colors) where the homogeneous set is constructed from a descending sequence D_{n} of sets in the given ultrafilter U (called p in their notation) with certain extension properties. As Bergelson and Hindman point out, the proof of their Theorem 2.3 does not use the idempotence of the ultrafilter and so we carry it out in ACA_{0}^{U}. The main issue from the viewpoint of ACA_{0}^{U} is the construction of the sets B_{t}(E, i) for t ≤ k, i < r and E ∈ [M]^{t−1}. The definition begins innocuously enough with B_{k}(E, i) = {y ∈ M\E| E ∪ {y} ∈ A_{i}}. It then proceeds by backward induction on t < k by setting B_{t}(E, i) = {y ∈ M\E| B_{t+1}(E∪ {y}, i) ∈ U}. Assuming we have (a real in our model coding) which of all the B_{t+1}(E, i) for E ∈ [M]^{t} are in U (which we certainly do for k itself by ACA_{0}^{U}), we can clearly define (a real coding) all the B_{t}(E, i) and so there would be a real in our model coding which of all the B_{t}(E, i) are in U again by ACA_{0}^{U}. Thus as long as k is standard we can show (by an external induction through k many steps) that there is a real in the model coding all the B_{t}(E, i) for t ≤ k and which of them are in U. Equipped with this real as a parameter the construction of the D_{n} in Bergelson and Hindman [1989, Theorem 2.3] is carried out routinely in ACA_{0}^{U} using just the properties for U being an ultrafilter.

Bergelson and Hindman [1989] then deduce our Theorem 3.4 as their Corollary 2.4 using the fact that U is idempotent. The procedure is much like the Galvin-Glazer proof of Hindman’s theorem and can be modified to fit ACA_{0}^{IU} in the same way as in our proof of Theorem 3.3, by building a tree of all possible choices of the x_{i} and corresponding sets C_{i} with C = D_{0}, x_{0} ∈ C_{0} and C_{0} −x_{0} ∈ U. Inductively if we have the sequences up to C_{n} we consider the x ∈ C_{n} along with C_{n} − x and intend to choose as x_{n+1} an x larger than l(n) = the sum of all the previous x_{i} with C_{n}−x ∈ U and set C_{n+1} = C_{n}∩C_{n}−x∩D_{l(n+1)}. As before, we can recursively lay out the tree of all possible constructions with a single real coding all the possible choices of the x_{n} and C_{n} along each path. Asking the appropriate array of questions about membership in U then produces a real which guides the choice of an infinite path in this tree to construct a specific sequences which has all the desired sets in U. (The proof of nontermination is just the proof that the inductive step in Bergelson and Hindman [1989, Corollary 2.4] works, i.e. that U is idempotent.) Armed with this sequence the proof that ⟨x_{n}⟩ is as desired, is as they say routine and we note that it works in ACA_{0}^{IU} without any concerns .

We note that essentially the same ultrafilter proof of Theorem 3.4 appears in Hindman and Strauss [2012, Ch. 18] along with two other versions of the theorem bearing the same relationships to the Milliken-Taylor theorem that FU and GG bear to HT. The derivations of these results there from the Milliken-Taylor Theorem are purely combinatorial and work in ACA_{0}. Thus they too are consequences of IHT. Thus all of these theorems are provable in IHT and so ACA_{0}^{+}.

We also note that Hirst [2004] has shown this result for MT(k) for each k ∈ ℕ by a much more direct proof. We discuss the proof theoretic strengths of ∀kMT (k) in the explication of Theorem 4.16 after the analysis of conservation results over ATR_{0} (Theorem 4.14 and Corollary 4.15) and its recursion theoretic strength in the appendix after Corollary 6.2.

4 Notions of Forcing

We assume from now on that all structures M for second order arithmetic are models of ACA_{0}. We use the language of forcing to construct the models of T^{IU} (for various theories T that include at least IHT and so ACA_{0}) but need very little of even the basic lemmas on forcing for the theories considered in Towsner [2014].

Recall that our language is that of second order arithmetic augmented by a unary function symbol δ_{U} taking sets to sets. Our goal is, given a model M of T, to build a subset U of the “sets” S of M and to interpret δ_{U}(X) so that 0 ∈ δ_{U}(X) ⇔ X ∈ U and n + 1 ∈ M ⇔ X^{[n]} ∈ U. We define a notion of forcing ⊩_{IU} with a definition of the forcing relation which differs slightly from the usual one. It is defined globally and directly for all arithmetic sentences to correspond to being true for every sufficiently generic filter extending the condition. We take U to be canonically defined from a generic (over M) filter for this forcing.

Definition 4.1. Our notion ℙ_{IU} of forcing (really this should be ℙ_{IU}^{M} but we omit the superscript when no confusion should arise) has as conditions sequences u in M of the form ⟨U_{0}, U_{1}, …, U_{i}, …⟩_{i∈M} such that there is a sequence y_{0} < y_{1} < y_{2} < … (in M) such that, for every i, U_{i} = F S(y_{i}, y_{i+1}, …). We define extension for ℙ_{IU} by v = ⟨V_{i}⟩ ≤ ⟨U_{i}⟩ = u ⇔ ∀i∃j(U_{i} ⊇ V_{j}).

Remark 4.2. This definition clearly implies that, if u = ⟨U_{0}, U_{1}, …⟩ ∈ ℙ_{IU} then, for each i, U_{i} is infinite, U_{i} ⊇ U_{i+1} and ∩U_{i} = ∅. Moreover, we can uniformly arithmetically translate between the representations of u as ⟨U_{i}⟩ and ⟨y_{i}⟩: Clearly, U_{i} is uniformly arithmetic in ⟨y_{i}⟩ as U_{i} = F S(y_{i}, y_{i+1}, …). In the other direction y_{i} is the least element of U_{i} − U_{i+1}. We are thinking of u as representing the filter F_{u} = {A ∈ S|∃i(A ⊇ U_{i})}. It is easy to see that this set is an M-filter for any u ∈ ℙ_{IU} and, for example, if v ≤ u then F_{v} ⊇ F_{u}. So we abuse notation by using A ∈ u (for A ∈ S and u a condition in ℙ_{IU}) to mean that ∃i(A ⊇ U_{i}). Given any (M-generic) filter 𝕌 on ℙ_{IU} (i.e. a filter on ℙ_{IU} which meets all dense sets definable in M), the corresponding (M-generic) object U is {A ∈ S|(∃u ∈ 𝕌)(A ∈ u)}. Note that both membership and extension in ℙ_{IU} are arithmetic relations in M.

Lemma 4.3. If ⟨u_{i}⟩ is a descending sequence in ℙ_{IU} in M then there is a condition u extending every u_{i}.

Proof. Let the sequences y_{i,j} and U_{i,j} be associated with u_{i} as in Definition 4.1. By Remark 4.2 and the definition of extension there is a function h defined by the following recursion:

h(0) = 0

h(i + 1) = μk(k > h(i) & (∀n, m ≤ h(i))(U_{n,m} ⊇ U_{h(i),k}).

We now let z_{i} = y_{h(i),h(i+1)} and define v to be the associated condition. We claim that v ≤ u_{i} for every i. Indeed, for any U_{n,m} choose an i such that n, m < h(i) and note that, by induction on j, for every j > i, U_{n,m} ⊇ U_{h(j),h(j+1)} and so z_{j} = y_{h(j),h(j+1)} ∈ U_{n,m} and U_{n,m} ⊇ V_{j} as required.

To get the forcing relation started (for arithmetic sentences of L^{U} with set parameters) we begin with the idea of deciding a set X.

Definition 4.4. A condition u ∈ ℙ_{IU} decides a set X ∈ S if (X ∈ u ∨ X̄ ∈ u) and ∀n(X^{[n]} ∈ u ∨ \overline{X^{[n]}} ∈ u).

Proposition 4.5. If u decides X, then there is a set Y ∈ S such that 0 ∈ Y ⇔ X ∈ u and n + 1 ∈ Y ⇔ X^{[n]} ∈ u. We then say that u ⊩ δ_{U}(X) = Y. The relation u decides X, the set Y such that u ⊩ δ_{U}(X) = Y and the relation u ⊩ δ_{U}(X) = Y are uniformly arithmetic (in u, X and Y as relevant).

Proof. That the relation u decides X is uniformly arithmetic is immediate from the definition of deciding. (Note, for example that, X^{[n]} ∈ u means that (∃i)(∀m)(m ∈ U_{i} → ⟨n, m⟩ ∈ X.) The first assertion then follows immediately from the definitions and the fact that M ⊨ ACA_{0}. The other assertions then follow from the definitions.

Definition 4.6. As a matter of notation at this point, we let δ_{U}^{0}(X) = X and δ_{U}^{n+1}(X) = δ_{U}(δ_{U}^{n}(X)). We say u decides δ_{U}^{n+1}(X) if u decides Y for the Y such that u ⊩ δ_{U}^{n}(X) = Y where we are also defining u ⊩ δ_{U}^{n}(X) = Y by the obvious induction.

Proposition 4.7. By iterating the previous Proposition, the relations u decides δ_{U}^{n+1}(X), u ⊩ δ_{U}^{n}(X) = Y and the set Y ∈ S such that u ⊩ δ_{U}^{n}(X) = Y are uniformly arithmetic in the sense that there is a recursive function that, for each n, supplies arithmetic formulas φ_{1}^{n}, φ_{2}^{n} and φ_{3}^{n} (whose complexity depends on n) such that φ_{1}^{n}(u, X) holds if and only if u decides δ_{U}^{n+1}(X); φ_{2}^{n}(u, X, Y) holds if and only if u ⊩ δ_{U}^{n}(X) = Y and φ_{3}^{n}(u, X, m) holds if and only if m is a member of the set Y such that φ_{2}^{n}(u, X, Y), i.e. u ⊩ δ_{U}^{n}(X) = Y.

We define the forcing relation between conditions and sentences of L^{U} for arithmetic sentences in terms of these relations.

Definition 4.8. Let Φ(Z_{1}, … Z_{m}) be an arithmetic formula of L^{U} with the free second order variables displayed. Consider an instance of Φ(X_{1}, … X_{m}) specified by choosing values X_{i} ∈ S for the Z_{i} and a condition u. We say that u ⊩ Φ(X_{1}, … X_{m}) if u decides every δ_{U}^{n_{j}}(X_{i}) occurring in Φ and M satisfies the sentence gotten from Φ(X_{1}, … X_{m}) by substituting the formula saying that k ∈ Y_{i,j} for the Y_{i,j} such that u ⊩ δ_{U}^{n_{j}}(X_{i}) = Y_{i,j} for the new atomic formulas k ∈ δ_{U}^{n_{j}}(X_{i}), X_{i} = Y_{j,k} for X_{i} = δ_{U}^{n_{k}}(X_{j}) and Y_{i,j} = Y_{l,k} for δ_{U}^{n_{j}}(X_{i}) = δ_{U}^{n_{k}}(X_{l}). We now proceed by induction to define forcing for second order sentences of L^{U} (which we assume to be in prenex normal form) in the obvious way. We say u ⊩ ∃ZΦ((X_{1}, … X_{m}, Z) if there is an X_{m+1} ∈ S such that u ⊩ Φ((X_{1}, … X_{m}, X_{m+1}). On the ∀ side we say u ⊩ ∀ZΦ((X_{1}, … X_{m}, Z) if there is no v ≤ u and no X_{m+1} ∈ S such that v ⊩ ¬Φ((X_{1}, … X_{m}, X_{m+1}) where we use ¬Φ as an abbreviation of the standard prenex normal form equivalent of the negation of Φ.

Proposition 4.9. For arithmetic sentences Φ(X_{1}, … X_{m}) of L^{U}, the relation u ⊩ Φ(X_{1}, … X_{m}) is uniformly arithmetic in u and X_{1}, … X_{m}. For Σ_{n}^{1} (Π_{n}^{1}) sentences Φ(X_{1}, … X_{m}) of L^{U} the relation u ⊩ Φ(X_{1}, … X_{m}) is uniformly Σ_{n}^{1} (Π_{n}^{1}).

Proof. The arithmetic case follows directly from the definition of forcing and Proposition 4.7. The second order cases then follow by the obvious induction.

Proposition 4.10 (IHT). Assume M ⊨ IHT. For each sequence ⟨X_{m}⟩ ∈ S, the set {u|∀m(u decides X_{m})} is dense in ℙ_{IU}. For each sentence Φ of L^{U} (with set parameters), the set {u|u decides Φ} is also dense in ℙ_{IU}. (We say u decides Φ if u ⊩ Φ or u ⊩ ¬Φ as usual.)

Proof. Consider any ⟨X_{m}⟩ ∈ S and v ∈ ℙ_{IU} generated by the sequence ⟨z_{i}⟩ as in Definition 4.1. By Lemma 2.11 we may, by a refinement gotten by replacing z_{i} by sums of z_{j} for j ≥ i, assume that there is an increasing sequence s_{i} such that 2^{s_{i}}|z_{i} but 2^{s_{i}+1} ∤ z_{i}. So for z = z_{i_{0}} + … + z_{i_{n}} with i_{0} < … < i_{n}, z ∈ V_{i_{0}} − V_{i_{0}+1} and i_{0} is the maximum j such that z ∈ V_{j}. Now consider the subsemigroup Z of M generated by the z_{i} and apply IGG for the sequence of colorings given by f_{⟨0,m⟩}(x) = 1 if x ∈ X_{m}, f_{⟨0,m⟩}(x) = 0 if x ∉ X_{m}, f_{⟨n+1,m⟩}(x) = 1 if x ∈ X_{m}^{[n]} and f_{⟨n+1,m⟩}(x) = 0 if x ∉ X_{m}^{[n]} to get a homogeneous subset q_{i} of Z. We may now refine the condition w generated by the q_{i} (which are themselves finite sums of z_{i}) as before to get one u generated by y_{i} with an increasing sequence t_{i} > s_{i} such that 2^{t_{i}}|y_{i} but 2^{t_{i}+1} ∤ y_{i} but that is still homogeneous in the sense of IGG. Thus for each y_{i} there is a maximal j such that y_{i} ∈ V_{j}. (As with the sum z above, this j is determined by the positions of the t_{k} with respect to the s_{l}.) For this j, U_{i} ⊇ V_{j} as required for u to be an extension of v. The IGG homogeneity of the sequence y_{i} guarantees that for each m, X_{m} ⊇ U_{i} or \overline{X_{m}} ⊇ U_{i} and for each ⟨n + 1, m⟩, X_{m}^{[n]} ⊇ U_{i} or \overline{X_{m}^{[n]}} ⊇ U_{i} for some i as required.

The second assertion now follows easily from the definitions of deciding sentences Φ and terms δ_{U}^{n}(X) by induction on both the complexity of Φ and the depth of δ_{U} terms occurring in Φ.

Theorem 4.11. If M ⊨ IHT and both 𝕌 and the associated U are M-generic for ℙ_{IU}, then M^{U} is an L^{U} structure and a model of ACA_{0}^{IU}. Moreover, any sentence Φ of L^{U} (with second order parameters) is true in M^{U} if and only if there is a u ∈ 𝕌 such that u ⊩ Φ. Finally, U is an idempotent M-ultrafilter.

Proof. Consider any M-generic U and any X ∈ S. By Proposition 4.10, there is a u ∈ 𝕌 (which decides X) and a (necessarily unique) Y ∈ S such that u ⊩ δ_{U}(X) = Y. Moreover, for any v ∈ U and Z ∈ S such that v ⊩ δ_{U}(X) = Z, Y = Z. If not, then, without loss of generality, there is some n such that X^{[n]} ∈ u but X^{[n]} ∉ v (or X ∈ u but X ∉ v) and so \overline{X^{[n]}} ∈ v (X̄ ∈ v). So there are i and j such that X^{[n]} ⊇ U_{i} but \overline{X^{[n]}} ⊇ V_{j} (or X ⊇ U_{i} but \overline{X} ⊇ V_{j}). This would contradict the compatibility of all u, v ∈ 𝕌 as any w ≤ u, v would have some W_{k} ⊆ U_{i} ⊆ X^{[n]} (or X) and some W_{l} ⊆ V_{j} ⊆ \overline{X^{[n]}} (or X̄) and so W_{k} ∩ W_{l} = ∅. Thus there is a well-defined function specified on S by δ_{U}(X) = Y where u ⊩ δ_{U}(X) = Y for some u ∈ 𝕌. This function makes M^{U} into an L^{U} structure as desired.

Next consider any arithmetic sentence Φ(Y_{1}, … Y_{k}) of L^{U} with second order parameters displayed. By Proposition 4.10, there is a u ∈ 𝕌 which decides Φ(Y_{1}, … Y_{k}). It is clear from the definition of forcing and our interpretation of δ_{U}(X) in M^{U} that M^{U} ⊨ Φ if u ⊩ Φ and M^{U} ⊨ ¬Φ if u ⊩ ¬Φ. It is now an easy induction to show that every sentence Φ of L^{U} is true in M^{U} if and only if it is forced by some u ∈ 𝕌.

Now consider any instance of a comprehension axiom of ACA_{0}^{IU} given by Φ(Y_{1}, … Y_{k}, x) with Φ as above except that it now has one free number variable x. By Proposition 4.10, there is a u ∈ 𝕌 which decides every δ_{U}^{n}(Y_{i}) occurring in Φ and so for each a, u forces Φ(Y_{1}, … Y_{k}, a) or its negation and the corresponding sentence is true in M^{U}. As u forcing Φ(Y_{1}, … Y_{k}, a) and forcing its negation are arithmetic relations in M, the set of a ∈ M such that M^{U} ⊨ Φ(Y_{1}, … Y_{k}, a) is arithmetically definable in M (using u) and so a member of S as required (as M ⊨ ACA_{0}).

Finally, we show that M^{U} satisfies the special axioms for U being an idempotent ultrafilter. If X ∈ U, i.e. 0 ∈ δ_{U}(X), then by definition X ∈ u for some u ∈ 𝕌, i.e. X ⊇ U_{i} for some i and so is infinite by Definition 4.1 and M^{U} satisfies AU1. If Y ⊇ X ∈ U then for some u ∈ 𝕌, Y ⊇ X ⊇ U_{i} and so Y ∈ U and M^{U} satisfies AU2. If X, Y ∈ U then there are u, v ∈ 𝕌 and i and j such that X ⊇ U_{i} and Y ⊇ V_{j}. As 𝕌 is a generic filter it contains a condition w ≤ u, v. The definition of extension provides k and l such that U_{i} ⊇ W_{k} and V_{j} ⊇ W_{l}. Now clearly, X ∩ Y ⊇ W_{k} ∩ W_{l} = W_{max{k.l}} by Definition 4.1. So X ∩ Y ∈ U and M^{U} satisfies AU3. Next for any X there is a u ∈ 𝕌 which decides X and so an i such that X ⊇ U_{i} or X̄ ⊇ U_{i}, i.e. X ∈ U or X̄ ∈ U and M^{U} satisfies AU4 .

For the last axiom, AU5, suppose X ∈ U and so X ⊇ U_{i} for some u ∈ 𝕌 (determined by ⟨y_{i}⟩). We also suppose that ∀n(Y^{[n]} = X − n)) and ∀i(i ∈ Z ⇔ i + 1 ∈ δ_{U}(Y)). By Definition 4.1, U_{i} = F S{y_{j}|j ≥ i} and if we take any z ∈ U_{i} with z = y_{i_{0}} + ⋯ + y_{i_{m}} (i ≤ i_{0} < ⋯ < i_{m}) then X − z ⊇ U_{i} − z ⊇ U_{j} for any j > i_{m} and so X − z ∈ U for every z ∈ U_{i_{m}+1} and we satisfy AU5.

Corollary 4.12. ACA_{0}^{IU} is a conservative extension of IHT for all sentences of second order arithmetic.

Proof. Note that by Theorem 3.3, ACA_{0}^{IU} ⊢ IHT. On the other hand, suppose ACA_{0}^{IU} ⊢ Φ. Theorem 4.11 shows that every model of IHT can be extended to one M^{U} of ACA_{0}^{IU} with the same M and S. So, if for any sentence Φ of second order logic there is an M ⊨ IHT & ¬Φ, then for any M-generic U, M^{U} ⊨ ¬Φ & ACA_{0}^{IU} for the desired contradiction.

As noted in Towsner [2014] for his language in the context of ACA_{0}^{U}, it does not make sense to consider weaker systems than ACA_{0} as ACA_{0}^{IU} is a conservative extension of RCA_{0}^{IU} for all sentences of second order arithmetic. Indeed the axioms of the apparently stronger theory are provable in the weaker. (He says this follows from results of Kirby [1984].) We give a easy proof.

Proposition 4.13. RCA_{0}^{U} ⊢ACA_{0}^{U}.

Proof. We consider definitions of sets by arithmetic formulas in prenex normal form {n|φ(n, x̄, W̄)} (with additional free number and set variables x̄, W̄). We prove by (external) induction on the number of (first order) quantifiers in φ ∈ L^{U} that a set as defined by the formula exists, i.e. ∀W̄ ∀x̄∃Y (n ∈ Y ↔ φ(n, x̄, W̄)). (As usual we can suppress the W̄ which gets carried along for the ride in the proof.) Consider the case that φ has one existential quantifier φ = ∃x_{1}φ_{1}(n, x_{1}, x_{2}, …, x_{k}). In RCA_{0}^{U} we see that there is a set Z such that Z^{[⟨n,x_{2},...,x_{k}⟩]} = {s|(∃x_{1} < s)(φ_{1}(n, x_{1}, x_{2}, …, x_{k}). It is clear that each such column of Z is either empty or cofinite. Moreover, for every ⟨x_{2}, …, x_{k}⟩, the set {n| ⟨n, x_{2}, …, x_{k}⟩ + 1 ∈ δ_{U}((Z)} exists (by RCA_{0}^{U}) and supplies the witnesses needed for this φ. Indeed one has Y_{1} with Y_{1}^{⟨x_{2},...,x_{k}⟩} = {n|∃x_{1} < t)(φ_{1}(n, x_{1}, x_{2}, …, x_{k})}. We can now prove the existence of Y_{2} with Y_{1}^{⟨x_{3},...,x_{k}⟩} = {n|∀x_{2}∃x_{1} < t)(φ_{1}(n, x_{1}, x_{2}, …, x_{k})} in the same way using Y_{1} as an additional parameter and then proceed by induction.

On the other hand, it makes perfect sense to ask about theories stronger than ACA_{0}.

Theorem 4.14. If T is any one of ACA_{0}^{+}, ATR_{0}, Π_{1}^{1}-CA_{0} or Π_{2}^{1}-CA_{0}, M ⊨ T and U is M-generic for ℙ_{IU} then M^{U} ⊨ T^{IU}.

Proof. ACA_{0}^{+}: The desired result follows immediately from Theorem 4.11 and the definition of ACA_{0}^{+}: Every X ∈ M^{U} is in M by the definition of M^{U}. If M ⊨ ACA_{0}^{+} then there is a (unique) set Y in M satisfying (in M) the implicit arithmetic definition of Y from X given by the defining axiom of ACA_{0}^{+}. Again, by the definition of M^{U}, this Y is in M^{U}. As the numbers of M^{U} are the same as those of M, X and Y satisfy the implicit definition of the defining axiom in M^{U} as required.

ATR_{0}: We just have to prove the comprehension axioms for ATR_{0}^{IU} and so, for each instance of the axiom and each condition u (forcing the hypotheses of the axiom) we need an extension v of u which forces the conclusion. Note that a set codes a well ordering in M if and only if it codes one in M^{U} by Theorem 4.11. Suppose we are given an instance of the axioms specified by a well ordering ⟨X, <_{X}⟩ in M^{U} and an arithmetic formulas Φ(z, Z) of L^{U} possibly with number and set parameters. For convenience we assume that ⟨X, <_{X}⟩ is one of the set parameters and x one of the number parameters.

The given instance of ATR_{0}^{IU} is then specified by an arithmetic formula Θ(n, Z) of L^{U} containing these parameters with n and Z free. We want a set Y such that, for each x ∈ X, ∀n(n ∈ Y^{[x]} ⇔ Θ(n, Y^{[<x]}). The basic idea is that we want to prove the existence of a set ⟨Y, Z⟩ such that, for each x ∈ X, Z^{[x]} ⊩ ∀n(n ∈ Y^{[x]} ⇔ Θ(n, Y^{[<x]})) and, for x <_{X} y, Z^{[y]} ≤ Z^{[x]} ≤ u. Our plan is to expand <_{X} by inserting additional steps so that a fixed Θ̂ will define the desired sequence of pairs. For each set ⟨Y^{[<x]}, Z^{[<x]}⟩ ,

and x ∈ X we know that there is a ⟨Ŷ , Ẑ⟩ with ⟨Ŷ^{[<x]}, Ẑ^{[<x]}⟩ = ⟨Y^{[<x]}, Z^{[<x]}⟩ such

that Z^{[x]} ⊩ ∀n(n ∈ Ŷ^{[x]} ⇔ Θ(n, Ŷ^{[<x]})) and Z^{[x]} ≤ Z^{[y]} for every y < x. (For notational simplicity, we are assuming that ⟨Y, Z⟩^{[x]} = ⟨Y^{[x]}, Z^{[x]}⟩.) We want to specify a well-ordered sequence of arithmetic operators that will produce such a result. One could do this by hand but we use a metatheorem that relies on the fact that this Π_{2}^{1} assertion is provable in IHT and so in ACA_{0}^{+} (Blass, Hirst and Simpson [1987,4.13]). Theorem 6.1 says that there are e, k ∈ ℕ such that ∀X∀x∀ ⟨Y, Z⟩ ∃ ⟨Ŷ , Ẑ⟩ (⟨Ŷ^{[<x]}, Ẑ^{[<x]}⟩ =

⟨Y^{[<x]}, Z^{[<x]}⟩ & Z^{[x]} ⊩ ∀n(n ∈ Ŷ^{[x]} ⇔ Θ(n, Ŷ^{[<x]})) &(∀y <_{X} x)(Z^{[x]} ≤ Z^{[y]}) &

⟨Ŷ , Ẑ⟩ = Φ_{e}(⟨Ŷ^{[<x]}, Ẑ^{[<x]}, ⟨X, <_{X}⟩ , x⟩^{(ω·k)}). So we can form a new well ordering which inserts ω · k steps between each x ∈ X and its immediate successor x + 1 each of which produces the Turing jump of its input and at the step at the end corresponding to x+1 in

<_{X} applies Φ_{e} to ⟨Ŷ^{[<x]}, Ẑ^{[<x]} ⟨X, <_{X}⟩ , x⟩^{(ω·k)} which is arithmetic in the new sequence

inserted between x and x + 1. (In the usual way, we are using Z^{(ω·k)} to denote the result of iterating the Turing jump ω · k many times beginning with Z.)

The fact that the relations of extension and forcing the relevant sentences are arithmetic follow from Remark 4.2 and Proposition 4.9. The existence of some ⟨Y^{[x]}, Z^{[x]}⟩ as required follows from Proposition 4.10 at successor steps in <_{X}. For x a limit point, one would first arithmetically define a strictly ascending sequence in <_{X} with limit x and apply Lemma 4.3 before using Proposition 4.10. Thus the desired Π_{2}^{1} assertion is provable in IHT and so ACA_{0}^{+} as required for Theorem 6.1

Now given the ⟨Y, Z⟩ witnessing the truth of this new instance of ATR_{0} in M, we can define Ŷ by the arithmetic formula n ∈ Ŷ^{[x]} ⇔ Z^{[x]} ⊩ Θ(n, Ŷ^{[<x]}). A standard transfinite induction together with the representation of truth in M^{U} by forcing conditions in ℙ_{IU} now shows that the Ŷ so defined is the one required for the instance of ATR_{0}^{IU} with which we began and one more application of Lemma 4.3 gives the z ≤ Z^{[x]} ≤ u for every x ∈ X that forces everything and gives the density result needed to show that there is a Ŷ as required in every M^{U}.

Π_{1}^{1}-CA_{0}: We prove Σ_{1}^{1}-CA_{0} which is obviously equivalent to Π_{1}^{1}-CA_{0}. Suppose ∃XΦ(X, i) is a Σ_{1}^{1} formula of M^{U}. As u ⊩ Φ(Y, n) and being an extension in ℙ_{IU} are arithmetic predicates (of Y, u and n), we can apply strong Σ_{1}^{1}-DC_{0} (which is a consequence of Π_{1}^{1}- CA_{0}) to get a sequence ⟨Y_{i}, u_{i}⟩ with u_{0} ∈ ℙ_{IU} arbitrary, u_{i+1} ≤ u_{i} and u_{i+1} ⊩ Φ(Y_{i}, i) if there is any ⟨Y, v⟩ with v ≤ u_{i} such that v ⊩ Φ(Y, i). By Lemma 4.3, there is a condition u extending all the u_{i}. By genericity, then there is such a u ∈ U. We claim that M^{U} ⊨ ∃XΦ(X, i) ⇔ u ⊩ Φ(Y_{i}, i). Of course, by our previous argument, if u_{i+1} ⊩ Φ(Y_{i}, i), M^{U} ⊨ Φ(Y_{i}, i) (and so u ⊩ Φ(Y_{i}, i)) and M^{U} ⊨ ∃XΦ(X, i). For the other direction, if u_{i+1} ⊮ Φ(Y_{i}, i), then, by strong Σ_{1}^{1}-DC_{0}, no v ≤ u_{i} forces ∃XΦ(X, i) so, in particular, u ⊮ ∃XΦ(X, i). In this case, M^{U} ⊭ ∃XΦ(X, i) by the usual facts about forcing. (In this case, we could argue for this directly from the definitions and above results.)

Π_{2}^{1}-CA_{0}: The argument is essentially the same as for the previous case since Π_{1}^{1}-CA_{0} proves strong Σ_{2}^{1}-DC_{0}.

Corollary 4.15. For T any of the theories mentioned in Theorem 4.14, T^{IU} is a conservative extension of T for all sentences of second order arithmetic.

We now return to the example of the Milliken-Taylor theorem, MT(k), for all k and the problem of carrying out constructions that inductively define sets using the ultrafilter at each step. Using the analysis in Theorem 4.14 for special cases of ATR_{0} we can now handle situations in which the sets required are defined from the previous ones by an arithmetic formula including the ultrafilter (in the disguise of δ_{U}). Of course, we must now deal with all k in our model M^{U} not just the standard ones in ℕ. Note that MT(k) clearly implies RT_{r}^{k}, Ramsey’s theorem for k-tuples and all colors r by taking a_{t} = x_{n(t)}. As ∀k∀rRT_{r}^{k} is not provable in ACA_{0} (see Hirschfeldt [2104, Corollary 6.24]), ∀kMT (k) is not provable in ACA_{0}^{IU} by Theorem 4.15.

The only part of the proof of MT(k) for standard k outlined in Theorem 3.4 that used the fact that k ∈ ℕ was in the construction of the sets B_{t}(E, i) for t ≤ k. Note that the definition of B_{t}(E, i) in Bergelson and Hindman [1989, Theorem 2.3] given above is arithmetic in the real coding all the B_{t+1}(E, i) for E ∈ [ℕ]^{t} in L^{U}. Thus for each k ∈ M_{0} we can represent this definition as an example of ATR_{0}^{IU} over an ordering of length k. Thus we immediately have that ∀kMT (k) is provable in ATR_{0}. Of course, much less is needed as we only need instance of orderings of length k for each k ∈ M_{0}. Looking at the proof for ATR_{0} in Theorem 4.14, one sees that all one needs in the ground model are instances of ATR_{0} of length k(ω·n) for some fixed n ∈ ℕ (the k in that proof). Moreover, if IHT is provable in ACA_{0} then (still by Theorem 6.1) we can replace the ω-jump in this calculation by the Turing jump and so instances of ATR_{0} of length k · n (for some fixed n ∈ ℕ) in the model M would suffices.

It is clear that all instances of ATR_{0} for orderings of length a number in M_{0} are provable in the system usually denoted ACA0^{′} which asserts the existence of X^{(k)}, the kth Turing jump of X, for each k and X. (Indeed these two systems are clearly equivalent.) By analogy one could label the system which asserts the existence of X^{ω·k}, the, the ω · k jump of X, for each k and X, (ACA_{0}^{+})′. It is equivalent to the axioms for ATR_{0} restricted to orderings of type ω · k, so an alternative notation for ACA0^{′} and (ACA_{0}^{+})′ might be ATR_{0}^{<ω} and ATR_{0}^{<ω·ω} for instances of ATR_{0} of length less than ω and ω · ω, respectively. We thus have good bounds on the proof theoretic strength of ∀kMT (k).

Theorem 4.16. (ACA_{0}^{+})′ ⊢ ∀kMT (k). If ACA_{0} ⊢ IHT then ACA0^{′} ⊢ ∀kMT (k) and indeed ACA0^{′} and ∀kMT (k) are equivalent over RCA_{0}.

Proof. We have already argued for everything except the last claimed equivalence. This follows from our previous observation that ∀kMT (k) ⊢ ∀k, rRT_{r}^{k} while McAloon [1985, Theorem B] (or see Hirschfeldt [2104, Theorem 6.27]) proves that ∀k, rRT_{r}^{k} ⊢ ACA0^{′}.

Note that even if ACA_{0} does not prove IHT, we are still quite close to the best possible result as even MT(3) proves IHT (Hirst [2004, Theorem 6]).

If we are interested essentially in the divide between second and third order methods, then we would like results analogous to Theorem 4.14 and Corollary 4.15 for Z_{2}. The same proof does not work as the relevant instances of strong dependent choice are not provable in Z_{2} (see Simpson [2009, VII.6.3]). Nonetheless, our methods applied to theories satisfying ∃X(V = L[X]) yield a conservation result for Z_{2}^{IU} over Z_{2} for essentially all sentences of combinatorial interest.

Proposition 4.17. If T = Z_{2} + ∃X(V = L[X]), M ⊨ T and U is M-generic for ℙ_{IU} then M^{U} ⊨ T^{IU}.

Proof. Proceed as in the case for Π_{1}^{1}-CA_{0} in Theorem 4.14 but use strong Σ_{n}^{1}-DC_{0} for each n as needed. (By Simpson [2009, VII.6.5], strong Σ_{n}^{1}-DC_{0} is a theorem of Z_{2} + ∃X(V = L[X]) for each n

Corollary 4.18. Z_{2}^{IU} is Π_{4}^{1}-conservative over Z_{2}.

Proof. Suppose, for the sake of a contradiction, that Φ(X, Y, Z, W) is arithmetic and Z_{2}^{IU} ⊢ ∀X∃Y ∀Z∃W Φ(X, Y, Z, W) but M = ⟨M, S, +, ×, <, 0, 1, ∈⟩ ⊨ ∃X∀Y ∃Z∀W ¬Φ(X, Y, Z, W) and M ⊨ Z_{2}. Let X ∈ S be a witness to the failure of our Π_{4}^{1} sentence in M and let Ŝ = (L[X])^{M} and N = ⟨M, Ŝ, +, ×, <, 0, 1, ∈⟩. Note that, as usual, N ⊨ Z_{2} & V =

L[X]. We claim that N ⊨ ∀Y ∃Z∀W ¬Φ(X, Y, Z, W): Consider any Y ∈ Ŝ ⊆ S. By our assumptions, M ⊨ ∃Z∀W ¬Φ(X, Y, Z, W) and so, by Shoenfield absoluteness (see Simpson [2104, VII.4.14]), N ⊨ ∃Z∀W ¬Φ(X, Y, Z, W). Now by Proposition 4.17, we can extend N to N^{IU} while maintaining the same numbers M and the same class of sets Ŝ so that N^{IU} ⊨ Z_{2}^{IU} + V = L[X]. As we also have N^{IU} ⊨ ∀Y ∃Z∀W ¬Φ(X, Y, Z, W) we have contradicted our assumption that Z_{2}^{IU} ⊢ ∀X∃Y ∀Z∃W Φ(X, Y, Z, W) as desired

5 Ramsey Ultrafilters

We follow the same course as for idempotent ultrafilters with the natural changes. In place of AU5 we have the following axiom saying that U is Ramsey:

AU5R ∀X(⟨X^{[n]}⟩ partitions M into pairwise disjoint nonempty sets & ∀n(n + 1 ∉ δ_{U}(X)) → ∃Z(0 ∈ δ_{U}(Z) & ∀n|X^{[n]} ∩ Z| = 1))

The language is the same as before. We denote by T^{RU} the same theory as T^{IU} except that we replace AU5 by AU5R. The notion of forcing ℙ_{RU} is the same as ℙ_{IU} except that the only restrictions on the U_{i} making up a condition u are that the U_{i} are infinite and nested with empty intersection. We now adopt the same definitions as for ℙ_{IU} (4.4, 4.6 and 4.8) for ℙ_{RU}. All the same results hold with minor simplifications of some of the proofs as we no longer need to guarantee the extra requirements for conditions being in ℙ_{IU}. We give the proofs only for those results where changes are needed. Note that we only need ACA_{0} as our base theory rather than IHT.

Lemma 5.1 (4.3). If M ⊨ ACA_{0} and u_{i} is a descending sequence in ℙ_{ℝU} then there is a condition u extending every u_{i}.

Proof. Let u_{i} as specified by U_{i,j} be a descending sequence in ℙ_{RU}. As in Lemma 4.3 there is a function h defined by the following recursion:

h(0) = 0

h(i + 1) = μk(k > h(i) & (∀n, m ≤ h(i))(U_{n,m} ⊇ U_{h(i),k}).

We now set V_{i} = U_{h(i),h(i+1)} and verify as before that the associated condition v ≤ u_{i} for every i.

Proposition 5.2 (4.10 in ACA_{0}). For each sequence X_{m} ∈ S, the set {u|∀m(u decides X_{m})} is dense in ℙ_{RU}. For each sentence Φ of L^{U} (with set parameters), the set {u|u decides Φ} is also dense in ℙ_{RU}.

Proof. It is clear that by coding the X_{m} and X_{m}^{[n]} as the columns X^{[k]} of a single X that it suffices to find, for any condition u = ⟨U_{i}⟩, an extension v = ⟨V_{k}⟩ such that, for each k, X^{[k]} ∈ v or \overline{X^{[k]}} ∈ v. Begin with X^{[0]}. It is clear that either there are infinitely many (and so all as the U_{i} are nested) i such that U_{i} ∩X^{[0]} ≠ ∅ or there are infinitely many (and so all) such that U_{i} ∩ \overline{X^{[0]}} ≠ ∅. Let Z_{0} be X^{[0]} or \overline{X^{[0]}} accordingly and V_{0} = U_{0} ∩ Z_{0}. We now define Z_{k} and V_{k} by induction: Z_{k+1} is either X^{[k]} or \overline{X^{[k]}} whichever has nonempty intersection with all the U_{j}∩Z_{0}∩⋯∩Z_{k}. We then set V_{k+1} = U_{k+1}∩Z_{0}∩⋯∩Z_{k}∩Z_{k+1}. It is clear that the V_{k} are nested, nonempty with empty intersection and so form a condition v, As U_{k} ⊇ V_{k}, v ≤ u. It is also clear by the definition of the Z_{k} that X^{[k]} or \overline{X^{[k]}} contains V_{k} and so v decides X as required.

Theorem 5.3 (4.11). If M ⊨ ACA_{0} and 𝕌 and the associated U are M-generic for ℙ_{RU} then M^{U} is an L^{U} structure and a model of ACA_{0}^{RU}. Moreover, any sentence Φ of L^{U} (with second order parameters) is true in M^{U} if and only if there is a u ∈ 𝕌 such that u ⊩ Φ. Finally, U is a Ramsey M-ultrafilter.

Proof. No changes (other than replacing IU by RU) are needed except for the verification that U is a RamseyM-ultrafilter, i.e. M^{U} ⊨ AU5R (rather than AU5). By what we know at this point it suffices to show that for every X such that ⟨X^{[n]}⟩ partitions M into pairwise disjoint nonempty sets and every condition u which decides X and W where W^{[m]} = ∪{X^{[n]}|n ≥ m} with n + 1 ∈ δ_{U}(W) and n + 1 ∉ δ_{U}(X) for all n that there is a v ≤ u which forces the conclusion of AU5R: ∃Z(0 ∈ δ_{U}(Z) & ∀n|X^{[n]} ∩ Z| = 1.

By definition, ∀m∃i(W^{[m]} ⊇ U_{i}) so, by the properties of the U_{i} determining a condition and the fact that the X^{[n]} partition M, there is an increasing function g such that ∀i(U_{i} ∩ X^{[g(i)]} ≠ ∅). We let r_{i} be the least element of U_{i} ∩ X^{[g(i)]} and R = {r_{i}|i ∈ M} so V_{i} = U_{i} ∩ R is infinite for every i and defines a condition v ≤ u with R ⊇ V_{0}. Now choose t_{j} ∈ X^{[j]} for each j ∉ rg(g) and set T = {t_{j}|j ∉ rg(g)}. Let Z = R ∪ T. Clearly |Z ∩ X^{[n]}| = 1 for all n (the set consists of precisely r_{n} or t_{n} depending on whether n ∈ rg(g) or not. Moreover, Z ⊇ R ⊇ V_{0} and so v forces that Z is a witness to the conclusion of AU5R as required.

The same arguments as for the remaining results in §4 with RU replacing IU and the corresponding versions of all the previous results of §4 now give all the same results for Ramsey ultrafilters as we had for idempotent ultrafilters.

Corollary 5.4. ACA_{0}^{RU} is a conservative extension of ACA_{0} for all sentences of second order arithmetic.

As for IU, it does not make sense to consider theories weaker than ACA_{0} for such conservation results (as the same proof as for Proposition 4.13 shows that ACA_{0}^{RU} is a conservative extension of RCA_{0}^{RU}). However, the analogous theorems hold for the stronger theories.

Theorem 5.5. If T is any one of ACA_{0}^{+}, ATR_{0}, Π_{1}^{1}-CA_{0} or Π_{2}^{1}-CA_{0}, M ⊨ T and U is M-generic for ℙ_{RU} then M^{U} ⊨ T^{RU}.

Corollary 5.6. For T any of the theories mentioned in Theorem 5.5, T^{RU} is a conservative extension of T for all sentences of second order arithmetic.

Proposition 5.7. If T = Z_{2} + ∃X(V = L[X], M ⊨ T and U is M-generic for ℙ_{RU} then M^{U} ⊨ T^{RU}.

Corollary 5.8. Z_{2}^{RU} is Π_{4}^{1}-conservative over Z_{2}.

6 Appendix

Hirschfeldt [2014, §6.3] mentions an old proof theoretic result of Wang [1993] as saying that if a Π_{2}^{1} formula ∀X(Θ(X) → ∃Y Ψ(X, Y)) is provable in ACA_{0} then there is a k ∈ ℕ such that ACA_{0} proves that for every X there is a Y ∈ Σ_{k}^{0,X} such that Ψ(X, Y). (Note that this means that in a nonstandard model the Σ_{k}^{0} formula may have nonstandard parameters.) We strengthen this result and extend it to ACA_{0}^{+} as we use this new version to prove our preservation and so conservation result over ATR_{0} in Theorem 4.14 and Corollary 4.15. We also derive some recursion theoretic bounds on results provable from IHT and so also by the ultrafilter arguments that are conservative over it.

The basic theorem can be generalized to systems containing RCA_{0} and specified by additional Π_{2}^{1} axioms. The strengthened version applies to systems which, like ACA_{0} and ACA_{0}^{+}, contain ACA_{0} and have axioms which define operators which preserve the order of Turing reducibility. The basic proof (for ACA_{0}^{+} and the general case) follows the compactness style argument given in Hirschfeldt [2014, Theorem 6.23] and attributed there to Jockusch. We then apply a simple observation for the strengthening. Rather than carry out the general proofs we simplify notation by considering just ACA_{0} and ACA_{0}^{+}. We then state the more general results which follow by the same arguments.

Theorem 6.1. Let T be ACA_{0} or ACA_{0}^{+}, J be the (implicitly arithmetically defined) Turing or arithmetic jump operator, respectively, with its iterates J^{(k)} and let R be a Π_{2}^{1} sentence ∀X∃Y (Ψ(X, Y)) (with Ψ arithmetic) such that T ⊢ R. Then ∃e, k ∈ ℕ such that, T ⊢ ∀X∃Y (Y = Φ_{e}(J^{(k)}(X)) & Ψ(X, Y)), i.e. T ⊢ ∀X((∃Y, Z)(Z, X satisfy the Π_{2}^{0} formula implicitly defining J^{(k)}(X) & Y = Φ_{e}(Z) & Ψ(X, Y)) where Φ_{e}(Z) is the function given by the eth Turing machine with oracle Z.

Proof. We first prove the apparently weaker conclusion analogous to the result of Wang that, for some k ∈ ℕ, T ⊢ ∀X∃i∃Y (Y = Φ_{i}(J^{(k)}(X) & Ψ(X, Y)), i.e. T ⊢ ∀X∃i((∃Y, Z)(Z, X satisfy the Π_{2}^{0} formula implicitly defining J^{(k)}(X) & Y = Φ_{i}(Z) & Ψ(X, Y)). (Note that, for ACA_{0} this is the same as saying that there is a solution to Ψ for X which is Δ_{k+1}^{X} (with possibly nonstandard parameters) and we have Wang’s theorem above.) Consider the parameterless arithmetic formulas Θ_{k}(X), for k ∈ ℕ, which say that ∃iΨ(X, Φ_{i}(X^{(k)})). (Formally, Ψ(X, Φ_{i}(X^{(k)})) denotes the formula saying Φ_{i}(X^{(k)}) is a total characteristic function and that the formula gotten by replacing, as usual, appearances of m ∈ Y in Ψ by Φ_{i}(X^{(k)}))(m) = 1.) If our desired result fails then T ∪ {¬Θ_{k}(C)} is consistent for each k. Indeed, as it is obvious that T ⊢ Θ_{k}(C) → Θ_{k+1}(C), T ∪ {¬Θ_{k}(C)|k ∈ ℕ} is also consistent by compactness. So we may suppose that we have a countable model M of T with a set C such that M ⊨ ¬Θ_{k}(C) for each k ∈ ℕ. Now form the subset Ŝ of the sets S of M generated from C by J and closure under Turing reductions in M. Define M̂ as the substructure of M with first order part that of M (i.e. M) and second order part Ŝ. As the first order parts of M and M̂ are the same, truth of first order sentences with second order parameters in Ŝ are the same in M and M̂. Thus, M̂ is also a model of T and the J operator in M̂ is the restrictions of that in M. Now, by the usual (external) construction of the closure in M of {C} under J and Turing reductions (in ω many steps) and the fact that J preserves Turing reducibility, every Y ∈ Ŝ is of the form Φ_{i}(C^{(k)}) for some i ∈ M and k ∈ ℕ and none of them satisfy Ψ(X, Y) in M by assumption and so none do in M̂. Thus M̂ is a model of T but not of R, for the desired contradiction.

Now we know that T ⊢ ∀X∃iΨ(X, Φ_{i}(X^{(k̂)})) for some fixed k̂ ∈ ℕ. Suppose that Ψ is Σ_{n}^{0} for some n ∈ ℕ. By standard arguments, we can choose e, k ∈ ℕ (uniformly recursively in k̂, the quantifier rank of Ψ and whether J is the Turing or arithmetic jump) such that (provably in T), for every X, m: m ∈ Φ_{e}(J^{(k)}(X)) ⇔ ∃iΨ(X, Φ_{i}(J^{(k̂)}(X))) & m ∈ Φ_{j}((J^{(k̂)}(X)) for j the least such i). A point to notice here is that as k > k̂, J^{(k̂)}(X) is uniformly recursive in J^{(k)}(X) and the properties we need can all be expressed in terms of indices relative to J^{(k̂)}(X) while k is taken to be sufficiently larger than k̂ that we can decide all the relevant sentences about J^{(k̂)}(X) uniformly recursively in J^{(k)}(X). It is now immediate that T ⊢ ∀XΨ(X, Φ_{e}(X^{(k)})).

We can now draw some recursion theoretic consequences which bound the complexity of witness to Π_{2}^{1} theorems of T (ACA_{0} or ACA_{0}^{+}) in the standard model of arithmetic. The first is the obvious one that if T ⊢ ∀X∃Y (Ψ(X, Y)) then there is a k such that for each X such that Y ≤_{T} J^{(k)}(X) (and indeed there is a fixed e such Φ_{e}(J^{(k)}(X)) is such a witness). Thus, for example, as MT(n) is provable in IHT for each n ∈ ℕ (Theorem 3.4) there is, for each n ∈ ℕ a k ∈ ℕ and and e ∈ ℕ such that for every instance X of MT(n), Φ_{e}(J^{(k)}(X) is the desired homogenous set. Here J being the ω-jump works as IHT is provable in ACA_{0}^{+}. If it turns out that IHT is provable in ACA_{0} then the Turing jump will work for J. Now the proof only works for standard n and so it does not say much on purely general grounds about the strength of the assertion ∀nMT (n) which we analyzed proof theoretically in Theorem 4.16. We can, however, use our Theorem 6.1 to derive recursion theoretic bounds. These comments and the Corollary we now give will apply just as well to the extensions of Theorem 6.1 in Corollary 6.6 and Theorem 6.8.

Corollary 6.2. Let T, J and R(n) = ∀X∃Y (Ψ(X, Y, n)) be as in Theorem 6.1. If for each n ∈ ℕ, T ⊢ R(n) then there is are recursive functions k(n) and e(n) such that for every n and X, Ψ(X, Φ_{e(n)}(J^{k(n)}(X), n).

Proof. We define the functions k(n) and e(n) by searching for the least triple consisting of a k, n and a proof in T of ∀X∃Y (Y = Φ_{e}(J^{(k)}(X)) & Ψ(X, Y)). This recursive search terminates by Theorem 6.1 and the functions so defined clearly satisfy the conclusion of our Corollary.

Now in some cases the numbers e and k of Theorem 6.1 can be read off (easily or with a bit of work) from the proof of R in T and it may be that the dependence on n of the proofs used in Corollary 6.2 can also be directly determined but in others it may not be at all clear how to produce this information. This is particularly true for Corollary 6.2 when the proof that ∀n(T ⊢ R(n)) is produced by an external induction on n ∈ ℕ. For MT(n) our proof is quite indirect and recovering these numbers not at all simple. On the other hand, the proofs in Hirst [2004] are much more amenable to such an analysis. In future work (on Gowers’ Fin_{k} theorem), we expect to see examples where recovering the number of jumps needed seems much more difficult and so Corollary 6.2 will give results that are far from obvious.

We now provide a generalization of Wang’s result that is proved by the same method.

Definition 6.3. We say that a proof theoretic system T (of second order arithmetic) is a Π_{2}^{1} system if it is specified by adding a set of Π_{2}^{1} axioms A_{i} = ∀X∃Y Γ_{i}(X, Y) to RCA_{0}.

Examples include ACA_{0} and ACA_{0}^{+} as they can be specified as the closure under the Turing and arithmetic jumps, respectively, and these operators are defined by arithmetic (even Π_{2}^{0}) formulas Φ(X, Y) with unique solutions Y for every X. Most of the systems weaker than ACA_{0}^{+} studied in reverse mathematics are of this form as are many stronger ones.

Theorem 6.4. Let T be a Π_{2}^{1} system generated over RCA_{0} by the Π_{2}^{1} axioms A_{i} = ∀X∃Y Γ_{i}(X, Y). Let R be a Π_{2}^{1} sentence ∀X∃Y (Ψ(X, Y)) such that T ⊢ R. Then ∃k ∈ ℕ such that T ⊢ ∀X∃l ≤ k∃i_{0}, …, i_{l} ≤ k(∃Z_{0}, … Z_{l}, Y_{0}, … Y_{l}, e_{0}, … e_{l})(X = Z_{0} & (∀j)_{0≤j≤l}(Y_{j} = Φ_{e_{j}}(Z_{j})) & (∀j)_{0≤j<l}(Γ_{i_{j}}(Y_{j}, Z_{j+1})) & Ψ(X, Y_{l})).

Proof. The proof is essentially the same as the proof above for the weak version of Theorem 6.1. The sentences Θ_{k}(X), for k ∈ ℕ, now assert that there are l ≤ k, i_{0}, …, i_{l} ≤ k, Z_{0}, … Z_{l}, Y_{0}, … Y_{l}, e_{0}, … e_{l} with the desired property. As above, if our conclusion fails T ∪ {¬Θ_{k}(C)} is consistent for each k. Indeed, as it is again obvious that T ⊢ Θ_{k}(C) → Θ_{k+1}(C), T ∪ {¬Θ_{k}(C)|k ∈ ℕ} is also consistent by compactness. So we may suppose that we have a countable model M of T with a set C such that M ⊨ ¬Θ_{k}(C) for each k ∈ ℕ.

The generation process for a submodel M̂ of M ⊨ T from C proceeds in ω many steps starting with C by alternately applying some Turing reduction Φ_{i} for i ∈ M and adding a set Z of M such that M ⊨ Γ_{i}(Y, Z) for some Y already added to our list and some i ∈ ℕ. As before M̂ is absolute with respect to M for arithmetic formulas with set parameters from M̂ and, moreover, is a model of T. By our our choice of C, M ⊨ ¬Θ_{k}(C) for every k ∈ ℕ. On the other hand, every set Y in M̂ is, for some l, i_{0}, … i_{l} ∈ ℕ, the Y_{l} of a sequence Z_{0}, … Z_{l}, Y_{0}, … Y_{l}, e_{0}, … e_{l} such that (X = Z_{0} & (∀j)_{0≤j≤l}(Y_{j} = Φ_{e_{j}}(Z_{j})) & (∀j)_{0≤j<l}(Γ_{i_{j}}(Y_{j}, Z_{j+1})))and so M ⊨ ¬Ψ(C, Y) for every Y ∈ M̂. Thus M̂ ⊨ ∀Y ¬Ψ(C, Y), i.e. M̂ is a model of T but not of R for the desired contradiction.

We now turn to the strengthening of Theorem 6.4 analogous to Theorem 6.1. Here we need additional assumptions on the axioms of our system T corresponding to the properties of ACA_{0} and ACA_{0}^{+} used to go from the weaker version above to the full theorem.

Definition 6.5. We say that the axiom A = ∀X∃Y Γ(X, Y) of a Π_{2}^{1} system corresponds to an operator J_{Γ}(X) if T ⊢ ∀X∃!Y Γ(X, Y). For k ∈ ℕ, we denote the k-fold iteration of such a J_{Γ} by J^{(k)}: J^{(0)}(X) = X and J^{(k+1)}(X) = JJ^{(k)}(X). We say that such an operator J_{Γ} is monotonic if ∀X∀Y ∀Z∀W (X ≤_{T} Y & Γ(X, W) & Γ(Y, Z) → W ≤_{T} Z).

In the setting of Theorem 6.4, if the axioms A_{i} correspond to monotonic operators J_{i} (such as the Turing or arithmetic jump) one of which is the Turing jump (so T ⊢ ACA_{0}), then we can deduce additional uniformities that provide a generalization of the full Theorem 6.1.

Corollary 6.6. Let T be a Π_{2}^{1} system all of whose axioms A_{i}, i ∈ ℕ, correspond to monotonic operators J_{i} one of which, say J_{0}, is the Turing jump and let R be a Π_{2}^{1} sentence ∀X∃Y (Ψ(X, Y)) such that T ⊢ R. Then there are e, k ∈ ℕ such that T ⊢ ∀XΨ(X, Φ_{e}(J^{(k)}(X))) where J(X) = J_{k}J_{k−1} … J_{0}(X).

Proof. By Theorem 6.4, we have a k ∈ ℕ such that T ⊢ ∀X∃l ≤ k∃i_{0}, …, i_{l} ≤ k(∃Z_{0}, … Z_{l}, Y_{0}, … Y_{l}, e_{0}, … e_{l})(X = Z_{0} & (∀j)_{0≤j≤l}(Y_{j} = Φ_{e_{j}}(Z_{j})) & (∀j)_{0≤j<l}(Γ_{i_{j}}(Y_{j}, Z_{j+1})) & Ψ(X, Y_{l})).

Let J(X) = J_{k}J_{k−1} … J_{0}(X). As the axioms A_{j} all define monotonic operators J_{j}, we see for any X, l, i_{0}, …, i_{l} ≤ k and sequences Z_{0}, … Z_{l}, Y_{0}, … Y_{l}, e_{0}, … e_{l} as above, Z_{j}, Y_{j} ≤_{T} J_{i_{j}}J_{i_{j−1}} … J_{i_{0}}(X) ≤_{T} J^{(k)}(X) for all j ≤ k. So all possible such sequences can be represented by indices relative to J^{(k)}(X). Moreover, for some n larger than the quantifier complexities of Ψ and the Γ_{i} for i ≤ k, the assertions about sequences of indices satisfying the conditions described can all be decided uniformly recursively in (J^{(k)}(X))^{(n)} = J_{0}^{(n)}J^{(k)}(X) ≤_{T} J^{(k+n)}(X). Thus as before, by minimizing the sequence of indices defining the sequence of sets desired, we can calculate, uniformly recursively in k, Ψ and the Γ_{i}, i ≤ k, an index e which relative to J^{(k+n)}(X) calculates (provably in T) a Y such that Ψ(X, Y). This e along with k + n are the standard numbers required for the Corollary.

Theorems 6.1 and 6.4 as well as Corollary 6.6 all have analogous versions for Π_{1}^{1}-CA_{0} and the hyperjump operator replacing ACA_{0} and the Turing jump and Π_{3}^{1} axioms A_{1} and sentences R replacing the Π_{2}^{1} ones. For definiteness and simplicity we define the hyperjump by HJ(X) = {e|Φ_{e}(X) is the characteristic function of a well ordering}. This is one of the standard versions of the complete Π_{1}^{1}(X) set but any of the usual ones would do just as well. The crucial standard fact that we need to note is an absoluteness result for well-foundednes or, equivalently, Π_{1}^{1} sentences. We denote the finite iterates of the hyperjump by HJ^{(n)}(X) for n ∈ ℕ.

Proposition 6.7. If M ⊨ Π_{1}^{1}-CA_{0} and M̂ is an ω-submodel of M, i.e. it has the same first order part as M, and is closed under hyperjump then it is a β-submodel, i.e. for any Π_{1}^{1} sentence Φ with parameters in M̂, M ⊨ Φ ⇔ M̂ ⊨ Φ.

Proof. See Simpson [2009, VII,1.8].

We explicitly state the basic case of our metatheorem for Π_{1}^{1}-CA_{0} and leave the other analogs to the reader.

Theorem 6.8. If R = ∀X∃y∀ZΦ(X, Y, Z) is a Π_{3}^{1} sentence, T = Π_{1}^{1}-CA_{0} and T ⊢ R then there are e, k∈ ℕ such that T ⊢ ∀X∃Y (Y = Φ_{e}(HJ^{(k)}(X) & ∀ZΦ(X, Y, Z)).

Proof. The proof is essentially the same as Theorem 6.1 with hyperjump replacing the Turing or arithmetic jump J. Now, however, there are Π_{1}^{1} formulas defining each of the nth hyperjumps for n ∈ ℕ and one uses Proposition 6.7 to show that Π_{1}^{1} formulas with parameters in M̂ are absolute to M, i.e. M̂ is a β-submodel of M.

7 Bibliography

Avigad, Jeremy [1998], An effective proof that open sets are Ramsey, Arch. Math. Logic 37, 235–240.

Blass, Andreas, Hirst, Jeffry L. and Simpson, Stephen G. [1987], Logical analysis of some theorems of combinatorics and topological dynamics in Logic and combinatorics (Arcata, Calif., 1985), Stephen G. Simpson ed., Contemp. Math., 65, Amer. Math. Soc., Providence, RI, 1987, 125–156.

Bergelson, V. and Hindman, N. [1989], Ultrafilters and Multidimensional Ramsey Theorems, Combinatorica 9, 1-7.

Enayat. Ali [2006], From bounded arithmetic to second order arithmetic via automorphisms in Logic in Tehran, Ali Enayat, Iraj Kalantari, Mojtaba Moniri EDS., LNL 26, Association for Symbolic Logic (La Jolla CA), distributed by A.K. Peters (Wellesley MA).

Hindman, Neil [1972], The existence of certain ultrafilters on ℕ and a conjecture of Graham and Rothschild. Proc. Amer. Math. Soc. 36, 341-346.

Hindman, Neil [2005], Algebra in the Stone-Čech Compactification and its Applications to Ramsey Theory, Scientiae Mathematicae Japonicae 62, 321-329.

Hindman, Neil and Strauss, Dona [2012], Algebra in the Stone-Čech Compactification, Theory and Applications 2nd ed., De Gruyter, Berlin/Boston,

Hirschfeldt, Denis [2014], Slicing the Truth: On the Computable and Reverse Mathematics of Combinatorial Principles, Chitat Chong, Qi Feng, Theodore A Slaman, W. Hugh Woodin, and Yue Yang eds., World Scientific, Singapore.

Hirst, Jeffrey L. [2004], Hindman’s Theorem, Ultrafilters, and Reverse Mathematics, J. Sym. Logic 69, 65-72.

Kirby. l. A. S. [1984], Ultrafilters and types on models of arithmetic, Ann. Pure and Applied Math. 27, 215-252.

Kreuzer, Alexander [2012], Non-principal ultrafilters, program extractions and higher order reverse mathematics, J. Math. Logic 12, 1250002 (16 pp.).

Kreuzer, Alexander [2015], On Idempotent Ultrafilters in Higher-order Reverse Mathematics, J. Sym. Logic 80, 179-193.

Kreuzer, Alexander [2015a] Minimal Idempotent Ultrafilters and the Auslander-Ellis Theorem, Preprint. arXiv:1305.6530.

McAloon, K. [1985], Paris-Harrington incompleteness and progressions of theories in Recursion Theory (Ithaca, N.Y., 1982), Anil Nerode and Richard A. Shore, eds., Proc. Sympos. Pure Math. 42, Amer. Math. Soc., Providence, RI.

Simpson, Stephen G. [2009] Subsystems of Second Order Arithmetic 2^{nd} ed., Perspectives in Logic, ASL and Cambridge University Press, New York.

Todorcevic, Stevo [2010] Introduction to Ramsey Spaces, Annals of Mathematical Studies 174, Princeton University Press, Princeton NJ.

Towsner, Henry [2011], A combinatorial proof of the dense Hindman’s theorem, Discrete Math. 311, 1380–1384.

Towsner, Henry [2011a], Hindman’s theorem: An ultrafilter argument in second order arithmetic, J. Sym. Logic 76, 353–360.

Towsner, Henry [2104] Ultrafilters in reverse mathematics, J., Math. Logic 14, 145001 (11 pp.),

Wang, Hao [1993], Popular Lectures on Mathematical Logic, Revised reprint of the 1981 second edition, Dover Publications, Inc., New York.