Reverse mathematics and Peano categoricity

Stephen G. Simpson Department of Mathematics Pennsylvania State University http://www.math.psu.edu/simpson simpson@math.psu.edu

Keita Yokoyama^{∗}

Department of Mathematical and Computing Sciences Tokyo Institute of Technology yokoyama.k.ai@m.titech.ac.jp

First draft: August 18, 2011 This draft: September 5, 2013

Abstract

We investigate the reverse-mathematical status of several theorems to the effect that the natural number system is second-order categorical. One of our results is as follows. Define a system to be a triple A, i, f such that A is a set and i ∈ A and f : A → A. A subset X ⊆ A is said to be inductive if i ∈ X and ∀a (a ∈ X ⇒ f(a) ∈ X). The system A, i, f is said to be inductive if the only inductive subset of A is A itself. Define a Peano system to be an inductive system such that f is one-to-one and i ∉ the range of f. The standard example of a Peano system is ℕ, 0, S where ℕ = {0, 1, 2, …, n, …} = the set of natural numbers and S : ℕ → ℕ is given by S(n) = n+1 for all n ∈ ℕ. Consider the statement that all Peano systems are isomorphic to ℕ, 0, S. We prove that this statement is logically equivalent to WKL_{0} over RCA∗_{0}. From this and similar equivalences we draw some foundational/philosophical consequences.

Keywords: Reverse mathematics, second-order arithmetic, Peano system, foundations of mathematics, proof theory, second-order logic.

2010 Mathematics Subject Classification: Primary 03B30; Secondary 03D80, 03F35, 00A30, 03F25.

Published in Annals of Pure and Applied Logic, 164, 2012, pp. 229-243, http://dx.doi.org/10.1016/j.apal.2012.10.014

∗Yokoyama’s research was supported by a Japan Society for the Promotion of Science postdoctoral fellowship for young scientists, and by a grant from the John Templeton Foundation.

Contents

Abstract  1
Contents  2
1 Introduction  2
2 The role of Weak König’s Lemma  3
3 The role of Σ_{1}^{0} induction  6
4 Other categoricity theorems  7
5 Summary and open questions  15
References  16

1 Introduction

Reverse mathematics^{1} is a well known [18, 20] research direction in the foundations of mathematics. The goal of reverse mathematics is to pinpoint the weakest set-existence axioms which are needed in order to prove specific theorems of core mathematics. Such investigations are most fruitfully carried out in the context of subsystems of second-order arithmetic [18]. In that context it frequently happens that the weakest axioms needed to prove a particular theorem are logically equivalent to the theorem, over a weak base theory. For example, the well known theorem that every uncountable closed set in Euclidean space contains a perfect subset is logically equivalent to ATR_{0} over the weak base theory RCA_{0} [18, Theorem V.5.5].

A key theorem in rigorous core mathematics is the categoricity of the natural number system. Stated more precisely and in 20th-century language, the Peano Categoricity Theorem [14, Theorem 2.7.1] asserts that any two Peano systems are isomorphic. The Peano Categoricity Theorem was originally proved by Dedekind in 1888 [4, Satz 132], [5, Theorem 132] as a highlight of his rigorous, set-theoretical development [3, 4, 5] of the natural number system ℕ and the real number system ℝ.

In this paper we investigate the reverse-mathematical and proof-theoretical status of the Peano Categoricity Theorem and related theorems. One of our results is as follows.

The Peano Categoricity Theorem is equivalent to WKL_{0} over the standard weak base theory RCA_{0}.

(1)

1A crucial role in the development of reverse mathematics was played by H. Friedman [7, 8]. We thank the referee for strongly suggesting that we include this historical comment.

Here RCA_{0} and WKL_{0} are familiar [18, 20] subsystems of second-order arithmetic. Namely, RCA_{0} consists of Δ_{1}^{0} comprehension plus Σ_{1}^{0} induction, and WKL_{0} consists of RCA_{0} plus Weak König’s Lemma.

Our result (1) offers further confirmation of a point made by Väänänen^{2} in a recent talk based on his recent paper [22]. Väänanen observed that various second-order categoricity theorems can be proved without resorting to the full strength of second-order logic. Clearly (1) bears this out, because WKL_{0} is a relatively weak^{3} subsystem of second-order arithmetic, much weaker than ACA_{0} and in fact Π_{2}^{0}-equivalent to Primitive Recursive Arithmetic [18, §IX.3]. Since by (1) the Peano Categoricity Theorem is provable in WKL_{0}, it follows that the Peano Categoricity Theorem is finitistically reducible in the sense of Simpson’s partial realization [17, 19] (see also [1]) of Hilbert’s Program [9].

As a refinement of (1) we obtain the following stronger result.

The Peano Categoricity Theorem is equivalent to WKL_{0} not only over RCA_{0} but over the much weaker base theory RCA∗_{0}.

(2)

Recall from Simpson [18, §X.4] and Simpson/Smith [21] that RCA∗_{0} is RCA_{0} with Σ_{1}^{0} induction weakened to Δ_{1}^{0} induction plus natural number exponentiation, i.e., the assertion that m^{n} exists for all m, n ∈ ℕ. It is known that RCA∗_{0} is Π_{2}^{0}-equivalent to Elementary Function Arithmetic [21], hence much weaker than RCA_{0} and WKL_{0} which are Π_{2}^{0}-equivalent to Primitive Recursive Arithmetic [18, §IX.3].

Our stronger result (2) provides some foundational or philosophical insight concerning Dedekind’s construction of the natural number system [4, 5]. Recall that Dedekind’s key technical lemma, the “Satz der Definition durch Induction,” is a straightforward embodiment^{4} of the idea of primitive recursion. But at the same time, according to (2), the Peano Categoricity Theorem itself requires primitive recursion. Thus (2) constitutes further evidence that primitive recursion is indeed the heart of the matter.

The plan of this paper is as follows. In §2 we prove (1). In §3 we prove (2). In §4 we investigate the reverse-mathematical status of certain variants of the Peano Categoricity Theorem, replacing the Peano system ℕ, 0, S by the ordered system ℕ, 0, < or the ordered Peano system ℕ, 0, <, S. In §5 we summarize our results and state some open questions.

2 The role of Weak König’s Lemma

Recall from [18] that RCA_{0} is the subsystem of second-order arithmetic consisting of Δ_{1}^{0} comprehension and Σ_{1}^{0} induction. Within RCA_{0} one may freely use primitive recursion and minimization to define functions g : ℕ^{k} → ℕ where ℕ is the set of natural numbers [18, §II.3]. Recall also [18] that WKL_{0} consists of RCA_{0} plus Weak König’s Lemma, i.e., the statement that every infinite tree T ⊆ {0, 1}^{<ℕ} = ⋃_{n∈ℕ}{0, 1}^{n} has an infinite path.

2We thank Jouko Väänänen for raising the question which is answered by (1).

3By the strength of a theory T we mean the set of Π_{1}^{0} sentences which are provable in T.

4Dedekind’s “Satz der Definition durch Induction” [4, Satz 126] [5, Theorem 126] may be restated in 20th-century language [14, Theorem 2.2.1] as follows. For any system A, i, f there is a unique function Φ : ℕ → A such that Φ(0) = i and Φ(n + 1) = f(Φ(n)) for all n ∈ ℕ.

The purpose of this section is to show that the Peano Categoricity Theorem is equivalent to Weak König’s Lemma, the equivalence being provable in RCA_{0}.

Definition 2.1. Within RCA_{0} we make the following definitions. A system is a triple A, i, f such that A ⊆ ℕ and i ∈ A and f : A → A. A Peano system is a system A, i, f such that i ∉ rng(f) and f is one-to-one and

(∀X ⊆ A) ((i ∈ X and ∀a (a ∈ X ⇒ f(a) ∈ X)) ⇒ X = A).

The standard example of a Peano system is ℕ, 0, S with S : ℕ → ℕ defined by S(n) = n + 1. A Peano system A, i, f is said to be isomorphic to ℕ if there exists a bijection Φ : A → ℕ such that Φ(i) = 0 and Φ(f(a)) = Φ(a) + 1 for all a ∈ A. A Peano system A, i, f is said to be almost isomorphic to ℕ if for each a ∈ A there exists n ∈ ℕ such that f^{n}(i) = a.

Lemma 2.2. The following is provable in RCA_{0}. If a Peano system is almost isomorphic to ℕ, it is isomorphic to ℕ.

Proof. We reason in RCA_{0}. Let A, i, f be a system. As in [18, §II.3] use Σ_{1}^{0} induction to prove that for all n ∈ ℕ, f^{n}(i) exists and f^{n}(i) ∈ A. Use Δ_{1}^{0} comprehension to prove the existence of the function n ↦ f^{n}(i) : ℕ → A. Assume now that A, i, f is a Peano system which is almost isomorphic to ℕ. Use Δ_{1}^{0} comprehension to prove the existence of the function Φ : A → ℕ given by Φ(a) = min{n | f^{n}(i) = a} for all a ∈ A. Clearly Φ(i) = 0 and Φ(f(a)) = Φ(a)+1 for all a ∈ A, hence Φ is one-to-one. Moreover, because A, i, f is almost isomorphic to ℕ, Φ is onto ℕ. Thus Φ maps A, i, f isomorphically onto ℕ.

Theorem 2.3. The following are equivalent over RCA_{0}.

1. WKL_{0}.

2. Every Peano system is isomorphic to ℕ.

Proof. We first prove 1 ⇒ 2. Reasoning in WKL_{0}, let A, i, f be a Peano system. Recall that A ⊆ ℕ. By Lemma 2.2 it suffices to show that for each a ∈ A there exists n ∈ ℕ such that f^{n}(i) = a. Assume for a contradiction that c ∈ A and f^{n}(i) ≠ c for all n ∈ ℕ. Let T be the set of all t ∈ {0, 1}^{<ℕ} such that

(i < lh(t) and c < lh(t)) ⇒ t(i) ≠ t(c)

and

(∀a, b < lh(t)) (f(a) = b ⇒ t(a) = t(b)).

Clearly T is a tree. We claim that T is infinite. To see this, let n ∈ ℕ be given. Define t : {0, …, n − 1} → {0, 1} by letting t(a) = 1 if there exists a finite sequence a_{0}, …, a_{k} of elements of {0, …, n − 1} such that i = a_{0} and f(a_{0}) = a_{1} and f(a_{1}) = a_{2} and … and f(a_{k−1}) = a_{k} = a. If a ∈ {0, …, n − 1} and no such finite sequence exists, let t(a) = 0. Clearly t ∈ T and lh(t) = n so our claim is proved. By Weak König’s Lemma let h be an infinite path in T. Letting X = {a ∈ A | h(a) = h(i)} we see that i ∈ X and f(X) ⊆ X and c ∉ X contradicting our assumption that A, i, f is a Peano system.

Next we prove (¬ 1) ⇒ (¬ 2). Reasoning in RCA_{0}, assume ¬ 1 and let T ⊆ {0, 1}^{<ℕ} be an infinite tree with no infinite path. Then

T′ = T ∪ \{⟨\underbrace{1, …, 1}_{n}⟩ | n ∈ ℕ\}

is a tree with exactly one infinite path. Consider the lexicographic ordering of T′. The empty sequence ⟨⟩ is the first element of T′, and T is an initial segment of T′, and each t ∈ T′ has an immediate successor in T′, and the immediate successor of t is of the form t^{⌢}⟨0⟩ or t^{⌢}⟨1⟩ or ⟨t(0), …, t(m − 1), 1⟩ where m < lh(t) and t(m) = 0. Use Δ_{1}^{0} comprehension to prove the existence of the function f : T′ → T′ defined by f(t) = the immediate successor of t.

We claim that T has a last element under the lexicographic ordering of T′. If not, then f(T) ⊆ T and we can use bounded primitive recursion to obtain the “rightmost” infinite path p in T. Namely, define p : ℕ → {0, 1} by

p(n) = \{ \begin{matrix}1 & if ⟨p(0), …, p(n − 1), 1⟩ ∈ T, \\ 0 & otherwise. \end{matrix}

Clearly ⟨p(0), …, p(n − 1)⟩ ∈ T implies ⟨p(0), …, p(n − 1), p(n)⟩ ∈ T, because otherwise the immediate successor of ⟨p(0), …, p(n − 1)⟩ would be of the form ⟨p(0), …, p(m−1), 1⟩ = f(⟨p(0), …, p(n−1)⟩) ∈ T where m < n and p(m) = 0, contradicting the definition of p(m). Since ⟨⟩ ∈ T, it follows by Δ_{1}^{0} induction that ⟨p(0), …, p(n)⟩ ∈ T for all n ∈ ℕ, i.e., p is an infinite path in T. This contradiction proves our claim.

By the previous claim, let t_{1} be the last element of T under the lexicographic ordering of T′. Note that T′ = T ∪ {f^{n}(t_{1}) | n ∈ ℕ}.

We now claim that T′, ⟨⟩, f is a Peano system. If not, let X ⊆ T′ be such that ⟨⟩ ∈ X and f(X) ⊆ X and X ≠ T′. If T ⊆ X then in particular t_{1} ∈ X so by bounded primitive recursion we have f^{n}(t_{1}) ∈ X for all n ∈ ℕ, hence X = T′, a contradiction. Thus T ⊈ X, so fix t_{2} ∈ T \ X and let Y = {t ∈ T | t precedes t_{2} in the lexicographic ordering of T }. Then ⟨⟩ ∈ Y and f(Y) ⊆ Y ⊆ T so as above we can use bounded primitive recursion to prove the existence of an infinite path q in T. Namely, define q : ℕ → {0, 1} by

q(n) = \{ \begin{matrix}1 & if ⟨q(0), …, q(n − 1), 1⟩ ∈ Y, \\ 0 & otherwise. \end{matrix}

Clearly ⟨q(0), …, q(n − 1)⟩ ∈ Y implies ⟨q(0), …, q(n − 1), q(n)⟩ ∈ Y, because otherwise the immediate successor of ⟨q(0), …, q(n − 1)⟩ would be of the form ⟨q(0), …, q(m−1), 1⟩ = f(⟨q(0), …, q(n−1)⟩) ∈ Y where m < n and q(m) = 0, contradicting the definition of q(m). Since ⟨⟩ ∈ Y, it follows by Δ_{1}^{0} induction that ⟨q(0), …, q(n)⟩ ∈ Y for all n ∈ ℕ, but also Y ⊆ T so q is an infinite path in T. This contradiction proves our claim.

Because T is an infinite initial segment of T′, the Peano system T′, ⟨⟩, f cannot be isomorphic to ℕ. We have now proved ¬ 2, Q.E.D.

3 The role of Σ_{1}^{0} induction

Recall from [18, §X.4] and [21] that RCA_{0} consists of RCA∗_{0} plus Σ_{1}^{0} induction. In particular RCA∗_{0} is weaker^{5} than RCA_{0} and does not support the full use of primitive recursion. However, RCA∗_{0} does support the use of bounded primitive recursion, as well as minimization [21]. Recall also [21] that WKL∗_{0} consists of RCA∗_{0} plus Weak König’s Lemma.

The purpose of this section is to refine the results of the previous section, using the base theory RCA∗_{0} instead of RCA_{0}. We prove within RCA∗_{0} that Weak König’s Lemma and Σ_{1}^{0} induction are equivalent to certain statements about Peano systems. As a consequence we show that RCA∗_{0} can replace RCA_{0} in the statement of Theorem 2.3.

Definition 3.1. Within RCA∗_{0} we repeat Definition 2.1. Note however that RCA∗_{0} is not strong enough to prove that f^{n}(i) exists for all n ∈ ℕ and all systems A, i, f. Consequently, the notion of a Peano system being almost isomorphic to ℕ must be understood somewhat differently. Explicitly, a Peano system A, i, f is now said to be almost isomorphic to ℕ if for each a ∈ A there exists a finite sequence ⟨a_{0}, a_{1}, …, a_{n}⟩ such that a_{0} = i and a_{n} = a and a_{m+1} = f(a_{m}) for all m < n, in which case we define f^{n}(i) = a.

Lemma 3.2. The following are equivalent over RCA∗_{0}.

1. RCA_{0}.

2. Every Peano system which is almost isomorphic to ℕ is isomorphic to ℕ.

3. For each infinite set C ⊆ ℕ there exists a one-to-one function g : ℕ → C.

4. Each infinite subset of ℕ includes finite sets of arbitrarily large cardinality.

Proof. We reason within RCA∗_{0}. Recall that, within RCA∗_{0}, a set C ⊆ ℕ is defined to be infinite if it is unbounded, i.e., ∀n ∃c (n < c and c ∈ C), and finite if it is bounded. One can prove in RCA∗_{0} that a set is infinite if and only if it is nonempty and has no greatest element. One can also prove in RCA∗_{0} that each finite set F has a cardinality, i.e., a unique n ∈ ℕ such that there exists a one-to-one correspondence between F and {1, …, n}.

The implication 1 ⇒ 2 has already been proved as Lemma 2.2. To prove 2 ⇒ 3, let C be an infinite subset of ℕ and apply 2 to the Peano system C, c_{0}, ν_{C} where c_{0} is the least element of C and ν_{C} : C → C is given by ν_{C}(c) = the least c′ ∈ C such that c′ > c.

5See footnote 3.

The implication 3 ⇒ 4 is easily proved by means of Σ_{1}^{0} bounding [21]. To prove 4 ⇒ 1 we must prove that 4 implies Σ_{1}^{0} induction. Let φ(n) be a Σ_{1}^{0} formula such that φ(0) and ∀n (φ(n) ⇒ φ(n + 1)) hold. Write φ(n) ≡ ∃k θ(k, n) where θ(k, n) is a Σ_{0}^{0} formula. Use Δ_{1}^{0} comprehension to prove the existence of the set C consisting of all (codes for) finite sequences s = ⟨k_{0}, k_{1}, …, k_{n}⟩ such that (∀m ≤ n) (θ(k_{m}, m) and ¬ (∃k < k_{m}) θ(k, m)) holds. Our assumptions φ(0) and ∀n (φ(n) ⇒ φ(n+1)) imply that C has a least element but no greatest element, hence C is infinite. Now, given n ∈ ℕ, apply 4 to get a finite set F ⊂ C of cardinality > n. Because lh : C → ℕ is one-to-one, there exists s ∈ F such that lh(s) > n. Since lh(s) > n and s ∈ C it follows that θ(k_{n}, n) holds, hence φ(n) holds. This proves ∀n φ(n), Q.E.D.

Lemma 3.3. The following are equivalent over RCA∗_{0}.

1. WKL∗_{0}.

2. Every Peano system is almost isomorphic to ℕ.

Proof. Our proof of Theorem 2.3 establishes this result.

Theorem 3.4. The following are equivalent over RCA∗_{0}.

1. WKL_{0}.

2. Every Peano system is isomorphic to ℕ.

Proof. Combine Lemmas 3.2 and 3.3.

4 Other categoricity theorems

The Peano Categoricity Theorem may be viewed as a second-order characterization of the natural number system ℕ up to isomorphism using the language consisting of the constant 0 ∈ ℕ and the successor function S : ℕ → ℕ defined by S(n) = n + 1. It is also possible to study second-order characterizations of ℕ in terms of other languages. In this section we consider two languages which include the order relation < on ℕ. The two languages which we consider are 0, S, < and 0, <. We prove that various categoricity theorems for ℕ are equivalent over RCA∗_{0} to various subsystems of second-order arithmetic. The subsystems which we consider are RCA_{0}, WKL_{0}, WKL∗_{0}, ACA_{0}, ADS_{0}, and PFO∗_{0}. Here ACA_{0} is the well known [18] system consisting of RCA_{0} plus arithmetical comprehension, ADS_{0} is the known [10, 2] system consisting of RCA_{0} plus the ascending/descending sequence principle, and PFO∗_{0} is a new system which we introduce.

Definition 4.1. Within RCA∗_{0} we make the following definitions.

1. A successor system is a triple A, i, f such that A ⊆ ℕ and i ∈ A and f : A → A is one-to-one and i ∉ rng(f). A successor system is said to be inductive if (∀X ⊆ A) ((i ∈ X and ∀a (a ∈ X ⇒ f(a) ∈ X)) ⇒ X = A).

Note that an inductive successor system is the same thing as a Peano system.

2. An ordered system is a triple A, i, ≺ such that A ⊆ ℕ and ≺ is a linear ordering of A and i is the first element of A with respect to ≺ and for each a ∈ A there exists a′ ∈ A such that a ≺ a′ and there is no b such that a ≺ b ≺ a′. Thus a′ is the immediate successor of a with respect to ≺. Note that the successor function a ↦ a′ : A → A is not assumed to exist.

3. Let A, i, ≺ be an ordered system. We say that A, i, ≺ is inductive if

(∀X ⊆ A) ((i ∈ X and ∀a (a ∈ X ⇒ a′ ∈ X)) ⇒ X = A).

A set X ⊆ A is said to be ≺-bounded if (∃c ∈ A) (∀a ∈ X) (a ≺ c). We say that A, i, ≺ is strongly inductive (see Proposition 4.2 below) if each nonempty ≺-bounded subset of A has a first element and a last element with respect to ≺. We say that A, i, ≺ is isomorphic to ℕ if there exists Φ : A → ℕ which is one-to-one and onto ℕ such that Φ(i) = 0 and Φ(a′) = Φ(a) + 1 for all a ∈ A. We say that A, i, ≺ is almost isomorphic to ℕ if for each c ∈ A the initial segment {a ∈ A | a ≺ c} is finite.

4. An ordered successor system is a quadruple A, i, ≺, f such that A, i, ≺ is an ordered system and A, i, f is a successor system and f(a) = a′ for each a ∈ A.

5. Let A, i, ≺, f be an ordered successor system. We say that A, i, ≺, f is inductive if A, i, ≺ is inductive, or equivalently, if A, i, f is inductive. We say that A, i, ≺, f is strongly inductive if A, i, ≺ is strongly inductive. We say that A, i, ≺, f is isomorphic to ℕ if A, i, f is isomorphic to ℕ, or equivalently, if A, i, ≺ is isomorphic to ℕ. We say that A, i, ≺, f is almost isomorphic to ℕ if A, i, f is almost isomorphic to ℕ, or equivalently, if A, i, ≺ is almost isomorphic to ℕ.

Proposition 4.2. It is provable in RCA∗_{0} that every strongly inductive ordered system is inductive.

Proof. Let A, i, ≺ be a strongly inductive ordered system and suppose that X ⊆ A and i ∈ X and ∀a (a ∈ X ⇒ a′ ∈ X). It suffices to prove that X = A. If not, let c ∈ A be such that c ∉ X. Then Y = {a ∈ X | a ≺ c} is ≺-bounded and nonempty, so let a_{1} be the last element of Y with respect to ≺. Then a_{1} ∈ X and a′_{1} ∉ X, a contradiction.

Theorem 4.3. The following are pairwise equivalent over RCA∗_{0}.

1. RCA_{0}.

2. Every strongly inductive ordered successor system is isomorphic to ℕ.

3. Every inductive successor system which is almost isomorphic to ℕ is isomorphic to ℕ.

4. Every strongly inductive ordered successor system which is almost isomor-

phic to ℕ is isomorphic to ℕ. Proof. The equivalence 1 ⇔ 3 has already been proved as Lemma 3.2. The implications 2 ⇒ 4 and 3 ⇒ 4 are trivial, and the proof of Lemma 3.2 establishes 4 ⇒ 1. It remains to prove 1 ⇒ 2. Reasoning in RCA_{0}, let A, i, ≺, f be a strongly inductive ordered successor system. By Δ_{1}^{0} comprehension we have g : A → ℕ and h : ℕ → A defined by g(a) = min{k | a < f^{k}(a)} and h(0) = i and h(n + 1) = f^{g(h(n))}(h(n)). Since h(n) < h(n + 1) for all n, we can use Δ_{1}^{0} comprehension to prove that X = rng(h) exists. Since h(n) ≺ h(n + 1) for all n, we see that X is cofinal in A, ≺. For any a = h(n) ∈ X we have f^{m}(i) = a where m = ∑_{k<n} g(h(k)). It follows that A, i, f is almost isomorphic to ℕ. Hence by Lemma 2.2 A, i, f is isomorphic to ℕ. This completes the proof. Theorem 4.4. The following are pairwise equivalent over RCA∗_{0}.

1. WKL∗_{0}.

2. Every inductive successor system is almost isomorphic to ℕ.

3. Every inductive ordered successor system is almost isomorphic to ℕ. Proof. Our proof of Theorem 2.3 establishes this result. Theorem 4.5. The following are pairwise equivalent over RCA∗_{0}.

1. WKL_{0}.

2. Every inductive successor system is isomorphic to ℕ.

3. Every inductive ordered successor system is isomorphic to ℕ. Proof. The equivalence 1 ⇔ 2 is Theorem 3.4. The implication 2 ⇒ 3 is trivial. To prove 3 ⇒ 1, note that 3 ⇒ RCA_{0} by Theorem 4.3, and 3 ⇒ Weak König’s Lemma by the proof of Theorem 2.3. Theorem 4.6. The following are pairwise equivalent over RCA_{0}.

1. ACA_{0}.

2. Every inductive ordered system is isomorphic to ℕ.

3. Every strongly inductive ordered system which is almost isomorphic to ℕ is isomorphic to ℕ.

4. For every strongly inductive ordered system A, i, ≺ which is almost isomorphic to ℕ, there exists f : A → A such that A, i, ≺, f is an ordered successor system.

Proof. To prove 1 ⇒ 2 we reason in ACA_{0}. Given an inductive ordered system A, i, ≺, use arithmetical comprehension to prove the existence of Ψ : ℕ → A such that Ψ(0) = i and Ψ(n + 1) = Ψ(n)′ for all n ∈ ℕ. By arithmetical comprehension the set rng(Ψ) exists, and then the inductive property implies that rng(Ψ) = A. Thus Ψ is an isomorphism of ℕ onto A, i, ≺ and we have 2.

The implications 2 ⇒ 3 and 3 ⇒ 4 are trivial.

To prove 4 ⇒ 1 we reason in RCA_{0} and assume 4. Let g : ℕ → ℕ be a one-to-one function. Define a linear ordering <_{g} of ℕ by letting m <_{g} n if and only if g(m) < g(n). Using bounded Σ_{1}^{0} comprehension [18, Theorem II.3.9], we can easily check that ℕ has a first element i with respect to <_{g} and that ℕ, i, <_{g} is a strongly inductive ordered system which is almost isomorphic to ℕ. By 4 let f : ℕ → ℕ be such that ℕ, i, <_{g}, f is an ordered successor system, i.e., for all j ∈ ℕ, f(j) = the immediate successor of j with respect to <_{g}. We then have ∀j (∃n ≤ j) (f^{n}(i) = j), hence

∀m ((∃j (g(j) = m)) ⇔ (∃n ≤ m) (g(f^{n}(i)) = m)) ,

so the range of g exists by Δ_{1}^{0} comprehension using f and g as parameters. We have now shown that rng(g) exists for all one-to-one functions g : ℕ → ℕ. By [18, Lemma III.1.3] this implies ACA_{0}, Q.E.D.

Theorem 4.7. The following are pairwise equivalent over RCA∗_{0}.

1. ACA_{0}.

2. Every inductive ordered system is isomorphic to ℕ.

3. Every strongly inductive ordered system which is almost isomorphic to ℕ is isomorphic to ℕ.

Proof. This follows from Theorems 4.3 and 4.6.

Our next goal is to determine the reverse-mathematical and proof-theoretical status of the statement that every inductive ordered system is almost isomorphic to ℕ. To this end we present Definition 4.8 and Lemmas 4.9 and 4.10 leading to Theorem 4.11.

Definition 4.8. Within RCA∗_{0} we make the following definitions (see also [10, Definition 2.3]). Let L be an infinite linear ordering in which each non-first element has an immediate predecessor and each non-last element has an immediate successor. We say that L is ω-like if each element of L has finitely many predecessors. We say that L is ω^{∗}-like if each element of L has finitely many successors. We say that L is ω + ω^{∗}-like if L is not ω-like or ω^{∗}-like and each element of L has finitely many predecessors or finitely many successors. If L is ω + ω^{∗}-like, the ω-part of L is the set consisting of all elements of L with finitely many predecessors, provided this set exists. The ω^{∗}-part of L is defined similarly. Note that the ω-part of L exists if and only if the ω^{∗}-part of L exists. Let OOP be the statement that the ω-part of every ω + ω^{∗}-like linear ordering exists. We write OOP_{0} = RCA_{0} + OOP and OOP∗_{0} = RCA∗_{0} + OOP.

Lemma 4.9. OOP_{0} and OOP∗_{0} are equivalent over RCA∗_{0}.

Proof. It suffices to show that Σ_{1}^{0} induction is provable in OOP∗_{0}. Reasoning in RCA∗_{0}, suppose Σ_{1}^{0} induction fails. By Lemma 3.2 let C be an infinite subset of ℕ which does not have arbitrarily large finite subsets. Let c_{0} be the least element of C. Since C is unbounded, we may safely assume that C has no subset of cardinality c_{0}. For each n let f(n) be cardinality of {c ∈ C | c < n}. Note that f(n) < c_{0} for all n. Let L = ℕ and define <_{L} on L by letting m <_{L} n if and only if m < n ≤ c_{0} or c_{0} < m < n or m < f(n). In other words, for each pair c, c′ of successive elements of C we are inserting the interval {n | c < n ≤ c′} between f(c) and f(c′) = f(c) + 1. Thus L is an ω + ω^{∗}-like linear ordering. By OOP let B be the ω^{∗}-part of L. Then B = {n ≤ c_{0} | C has no subset of cardinality n} and B has a least element, which is clearly impossible, Q.E.D.

Lemma 4.10. OOP_{0} is equivalent to ACA_{0} over RCA_{0}.

Proof. Clearly arithmetical comprehension implies OOP, so it remains to show that OOP_{0} proves arithmetical comprehension. By [18, Lemma III.1.3] it suffices to show that OOP_{0} proves Σ_{1}^{0} comprehension. Reasoning in OOP_{0} and letting φ(m) be a Σ_{1}^{0} formula, we shall prove the existence of the set {m | φ(m)}. Write φ(m) ≡ ∃k θ(k, m) where θ(k, m) is Σ_{0}^{0}. Let D_{s} = {m < s | (∃k < s) θ(k, m)}. Thus D_{s}, s = 0, 1, 2, … is a nondecreasing sequence of finite sets such that ∀m (φ(m) ⇔ ∃s (m ∈ D_{s})).

Using bounded primitive recursion [21] we shall define an increasing sequence of finite linear orderings L_{s}, <_{s}, s = 0, 1, 2, . . .. Actually we shall have L_{2s} = {0, 1, …, s − 1} so there will be a linear ordering L, <_{L} where L = ⋃_{s} L_{s} = ℕ and <_{L}= ⋃_{s} <_{s}. We shall also define a sequence of partitions L_{s} = A_{s} ∪ B_{s} such that (∀u ∈ A_{s}) (∀v ∈ B_{s}) (u <_{s} v). We shall also have (∀u ∈ A_{s}) (∀v ∈ A_{s}) (u <_{s} v ⇔ u < v) and ∀s (B_{s} ⊆ B_{s+1}). Except for trivial cases, L will be ω + ω^{∗}-like with ω-part A = lim_{s} A_{s} and ω^{∗}-part B = lim_{s} B_{s} = ⋃_{s} B_{s}. In addition we shall define a function f : L → ℕ with this property:

If u_{1,s} < ⋯ < u_{k,s} are the elements of A_{2s} in increasing order, then f(u_{1,s}) < ⋯ < f(u_{k,s}) are the first |A_{2s}| elements of ℕ \ D_{s} in increasing order.

(3)

Taking the limit as s goes to infinity, we shall have:

If u_{1} < u_{2} < ⋯ are the elements of A in increasing order, then f(u_{1}) < f(u_{2}) < ⋯ are the elements of ℕ \ ⋃_{s} D_{s} in increasing order.

(4)

In particular our Σ_{1}^{0} formula φ(m) ≡ ∃s (m ∈ D_{s}) will be equivalent to the Π_{1}^{0} formula ∀u (u ∈ A ⇒ f(u) ≠ m), and the existence of {m | φ(m)} will then follow by Δ_{1}^{0} comprehension.

The inductive construction of L is as follows.

Stage 0. Let L_{0} = <_{0} = A_{0} = B_{0} = the empty set.

Stage 2s + 1. Let L_{2s+1} = L_{2s} ∪ {s} and insert s between A_{2s} and B_{2s}, i.e., <_{2s+1} = <_{2s} ∪ {⟨u, s⟩ | u ∈ A_{2s}} ∪ {⟨s, v⟩ | v ∈ B_{2s}}. Let A_{2s+1} = A_{2s} ∪ {s} and let B_{2s+1} = B_{2s}. Let f(s) = the (|A_{2s}| + 1)-st element of ℕ \ D_{s} in increasing order. Our inductive hypothesis (3) implies that u_{1,s} < ⋯ < u_{k,s} < s are the elements of A_{2s+1} in increasing order and f(u_{1,s}) < ⋯ < f(u_{k,s}) < f(s) are the first |A_{2s+1}| elements of ℕ \ D_{s} in increasing order.

Stage 2s + 2. Let L_{2s+2} = L_{2s+1} and <_{2s+2} = <_{2s+1}. Case 1: If there exists u ∈ A_{2s+1} such that f(u) ∈ D_{s+1}, let a be the least such u and let A_{2s+2} = {u ∈ A_{2s+1} | u < a} and B_{2s+2} = L_{2s+2} \ A_{2s+2}. Case 2: If no such u exists, let A_{2s+2} = A_{2s+1} and B_{2s+2} = B_{2s+1}. In either case it is clear that (3) continues to hold with s replaced by s + 1.

We may safely assume that Case 1 holds at infinitely many stages, because otherwise there would be a stage t such that ∀m (φ(m) ⇔ ¬ (∃s > t) (∃u ∈ A_{s}) (f(u) = m)), hence {m | φ(m)} would exist by Δ_{1}^{0} comprehension. Since Case 1 holds infinitely often, we have B_{s} ⫋ B_{s+1} for infinitely many s.

We may safely assume that ¬ φ(n) holds for infinitely many n. Let n be such that ¬ φ(n) holds. By bounded Σ_{1}^{0} comprehension [18, Theorem II.3.9], the set {m < n | φ(m)} exists and is finite, so by Σ_{1}^{0} bounding [21] let s be such that (∀m < n) (φ(m) ⇔ m ∈ D_{s}). Then f(u) = n for some u ∈ A_{2s+2n}, and then u ∈ A_{t} for all t ≥ 2s + 2n. Since ¬ φ(n) holds for infinitely many n, it follows that lim_{s} |A_{s}| = ∞.

It is now clear that L is ω + ω^{∗}-like with ω-part A = lim_{s} A_{s} and ω^{∗}- part B = ⋃_{s} B_{s}. It is also clear that (4) holds, so {m | φ(m)} exists by Δ_{1}^{0} comprehension. This completes the proof.

Theorem 4.11. The following are pairwise equivalent over RCA∗_{0}.

1. ACA_{0}.

2. OOP∗_{0}

3. Every inductive ordered system is almost isomorphic to ℕ.

Proof. The equivalence 1 ⇔ 2 follows from Lemmas 4.9 and 4.10. The implication 1 ⇒ 3 is clear from Theorem 4.6. It remains to prove 3 ⇒ 2. Let L be ω +ω^{∗}-like such that the ω-part of L does not exist. Let i be the first element of L, let A be the disjoint union of L and ℕ, and extend the given linear ordering of L and the standard ordering < of ℕ to a linear ordering ≺ of A with u ≺ n for all u ∈ L and all n ∈ ℕ. Then A, i, ≺ is an ordered system. Let X ⊆ A be such that i ∈ X and ∀a (a ∈ X ⇒ a′ ∈ X). If L ⊈ X, fix c ∈ L \ X and let Y = {a ∈ X | a ≺ c} = {u ∈ X | u <_{L} c}. Then Y is the ω-part of L, a contradiction. Thus L ⊆ X, and from this it follows that X = A. Thus A, i, ≺ is an inductive ordered system. It follows by 3 that L is finite. This contradiction completes the proof.

Remark 4.12. We thank Richard Shore [16] for showing us a proof of Lemma 4.10. We have modified that proof to obtain our proof above. Our construction yields the following recursion-theoretical results:

1. There exists a recursive linear ordering L of type ω + ω^{∗} such that the halting problem is Turing reducible to the ω-part of L.

2. Given a recursively enumerable Turing degree b, there exists a recursive linear ordering L of type ω + ω^{∗} such that the ω-part of L is retraceable and the ω^{∗}-part of L is recursively enumerable of degree b.

Subsequently Carl Jockusch [13] noted that these results are easily deduced from his 1968 paper [12]. Namely, 1 is implicit in [12, Theorem 5.2], and 2 follows from [12, Theorem 3.2, Corollary 3.3] plus the following characterization [13]:

3. A recursively enumerable set is the ω-part of a recursive linear ordering of type ω + ω^{∗} if and only if it is recursive or simple and semirecursive.

We now end this section by commenting on the reverse-mathematical and proof-theoretical status of the statement that every strongly inductive ordered system is almost isomorphic to ℕ.

Definition 4.13. Within RCA∗_{0} we define a countable linear ordering L to be pseudofinite if every nonempty subset of L has a first element and a last element. Let PFO be the statement that every countable pseudofinite linear ordering is finite. We write PFO_{0} = RCA_{0} + PFO and PFO∗_{0} = RCA∗_{0} + PFO.

Theorem 4.14. The following are equivalent over RCA∗_{0}.

1. PFO∗_{0}.

2. Every strongly inductive ordered system is almost isomorphic to ℕ.

Proof. We reason in RCA∗_{0}. To prove 1 ⇒ 2, assume PFO and let A, i, ≺ be a strongly inductive ordered system. For each c ∈ A the initial segment {a ∈ A | a ≺ c} is pseudofinite, hence finite, so A, i, ≺ is almost isomorphic to ℕ. Thus PFO ⇒ 2, i.e., 1 ⇒ 2. To prove 2 ⇒ 1, assume that L is a pseudofinite linear ordering. Let i be the first element of L. Let A be the disjoint union of L and ℕ. Extend the given linear ordering of L and the standard ordering < of ℕ to a linear ordering ≺ of A with a ≺ n for all a ∈ L and all n ∈ ℕ. Then A, i, ≺ is a strongly inductive ordered system. It follows by 2 that L is finite. Thus 2 ⇒ PFO, i.e., 2 ⇒ 1, Q.E.D.

Definition 4.15. Within RCA∗_{0} let ADS be the ascending/descending sequence principle of Hirschfeldt/Shore [10]: every countably infinite linear ordering L has an infinite ascending sequence or an infinite descending sequence. Here an infinite ascending sequence is defined to be a function s : ℕ → L such that s(n) <_{L} s(n + 1) holds for all n ∈ ℕ, and an infinite descending sequence is defined to be a function s : ℕ → L such that s(n) >_{L} s(n + 1) holds for all n ∈ ℕ. We write ADS_{0} = RCA_{0} + ADS and ADS∗_{0} = RCA∗_{0} + ADS.

Theorem 4.16. The following are equivalent over RCA_{0}.

1. ADS_{0}.

2. Every strongly inductive ordered system is almost isomorphic to ℕ.

Proof. The proof of [10, Proposition 2.4] shows that our system PFO_{0} (Definition 4.13) is equivalent to ADS_{0}. Using this observation, Theorem 4.16 follows immediately from Theorem 4.14.

Remark 4.17.

1. In view of Theorems 4.14 and 4.16, it is natural to ask whether PFO∗_{0} is equivalent to ADS∗_{0}. It turns out that this is not the case. Indeed, we shall now show that PFO∗_{0} is proof-theoretically much weaker^{6} than ADS∗_{0}.

2. On the one hand, it is clear from Lemma 3.2 that ADS∗_{0} proves Σ_{1}^{0} induction. Thus ADS∗_{0} is equivalent to ADS_{0}. Moreover, Chong/Slaman/Yang [2] have shown that ADS_{0} is Π_{1}^{1}-equivalent to RCA_{0} + Σ_{2}^{0} bounding, hence Π_{3}^{0}-equivalent to RCA_{0}. Thus ADS∗_{0} has the same strength as RCA_{0}.

3. On the other hand, Yokoyama [23] has shown that WKL∗_{0} + {RT(k, l) | k, l ≥ 2} is Π_{2}^{0}-equivalent to RCA∗_{0}. Here RT stands for Ramsey’s Theorem. Moreover, by Theorem 4.19 below, RCA∗_{0} + RT(2, 2) proves PFO. Thus PFO∗_{0} has the same strength as RCA∗_{0} and is therefore much weaker than RCA_{0}. We conjecture that PFO∗_{0} is Π_{1}^{1}-equivalent to RCA∗_{0}.

Definition 4.18. For X ⊆ ℕ write [X]^{2} = {(a, b) | a ∈ X, b ∈ X, a < b}. Within RCA∗_{0} let RT(2, 2) be the statement that for all p : [ℕ]^{2} → {0, 1} there exists X ⊆ ℕ which is infinite and homogeneous, i.e., [X]^{2} ⊆ p^{−1}({0}) or [X]^{2} ⊆ p^{−1}({1}). Following [10, §5] we define p : [ℕ]^{2} → {0, 1} to be transitive if for all a, b, c with a < b < c, p(a, b) = p(b, c) = 0 implies p(a, c) = 0, and p(a, b) = p(b, c) = 1 implies p(a, c) = 1. Within RCA∗_{0} let TRT(2, 2) be the statement that for all transitive p : [ℕ]^{2} → {0, 1} there exists X ⊆ ℕ which is infinite and homogeneous. Note that TRT(2, 2) is a special case of RT(2, 2).

Theorem 4.19. PFO is equivalent to TRT(2, 2) over RCA∗_{0}.

Proof. We reason in RCA∗_{0}. First, assume PFO and let p : [ℕ]^{2} → {0, 1} be transitive. For a, b ∈ ℕ define a <_{L} b if ((a < b and p(a, b) = 1) or (a > b and p(a, b) = 0)). Clearly ℕ, <_{L} is an infinite linear ordering. By PFO let X ⊆ ℕ be such that, with respect to <_{L}, either X has no first element or X has no last element. If X has no first element, Y = {b ∈ X | (∀a < b) (a ∈ X ⇒ a >_{L} b)} is infinite and [Y]^{2} ⊆ p^{−1}({0}). Similarly, if X has no last element, Y = {b ∈ X | (∀a < b) (a ∈ X ⇒ a <_{L} b)} is infinite and [Y]^{2} ⊆ p^{−1}({1}). We have now proved TRT(2, 2) assuming PFO.

Conversely, assume TRT(2, 2) and let L, <_{L} be a countably infinite linear ordering. We may safely assume that L ⊆ ℕ. Using Δ_{1}^{0} comprehension, define g : ℕ → L by g(a) = the least j > a such that j ∈ L, and then define a <_{L}^{∗} b if (g(a) <_{L} g(b) or (g(a) = g(b) and a < b)). Clearly ℕ, <_{L}^{∗} is an infinite linear ordering. Define p : [ℕ]^{2} → {0, 1} by letting p(a, b) = 1 if and only if a <_{L}^{∗} b. Then p is transitive, so by TRT(2, 2) let X be an infinite homogeneous set for p. Then Y = {j ∈ L | (∃a < j) (g(a) = j)} is an infinite subset of L.

6See footnote 3.

Moreover, if [X]^{2} ⊆ p^{−1}({0}) then Y has no first element with respect to <_{L}, and if [X]^{2} ⊆ p^{−1}({1}) then Y has no last element with respect to <_{L}. Thus L is not pseudofinite. This completes the proof.

Remark 4.20. Since ADS is equivalent to PFO over RCA_{0}, Theorem 4.19 implies that ADS is equivalent to TRT(2, 2) over RCA_{0}. The latter equivalence is originally due to Hirschfeldt/Shore [10, Theorem 5.3]. Our Theorem 4.19 answers a question which was posed by the referee.

5 Summary and open questions

RCA^{0}

isomorphic almost isomorphic implies isomorphic

almost isomorphic

i.s.s.  WKL_{0}, 3.4  RCA_{0}, 3.2  WKL_{0}, 3.3
i.o.s.  ACA_{0}, 4.7  ACA_{0}, 4.7  ACA_{0}, 4.11
s.i.o.s.  ACA_{0}, 4.7  ACA_{0}, 4.7  ADS_{0}, 4.16, 4.17
i.o.s.s. WKL_{0}, 4.5  RCA_{0}, 4.3  WKL_{0}, 4.4
s.i.o.s.s. RCA_{0}, 4.3  RCA_{0}, 4.3  RCA_{0}, 4.3

Table 1: Summary of equivalences over RCA_{0}.

RCA∗_{0}

isomorphic almost isomorphic implies isomorphic

almost isomorphic

i.s.s.  WKL_{0}, 3.4  RCA_{0}, 3.2  WKL∗_{0}, 3.3
i.o.s.  ACA_{0}, 4.7  ACA_{0}, 4.7  ACA_{0}, 4.11
s.i.o.s.  ACA_{0}, 4.7  ACA_{0}, 4.7  PFO∗_{0}, 4.14, 4.17, 5.1
i.o.s.s. WKL_{0}, 4.5  RCA_{0}, 4.3  WKL∗_{0}, 4.4
s.i.o.s.s. RCA_{0}, 4.3  RCA_{0}, 4.3  ?????, 5.2

Table 2: Summary of equivalences over RCA∗_{0}.

Tables 1 and 2 are a summary of our results. Abbreviations are used. For example, s.i.o.s.s. is an abbreviation for “strongly inductive ordered successor system.” Recall also that an i.s.s. or inductive successor system is the same thing as a Peano system. Each entry in Table 1 or 2 stands for one of our results concerning the reverse-mathematical status of a categoricity theorem for ℕ. As an example, the entry PFO∗_{0}, 4.14, 4.17, 5.1 in Table 2 means that RCA∗_{0} proves PFO∗_{0} ⇔ every strongly inductive ordered system is almost isomorphic to ℕ, with references to Theorem 4.14 and Remark 4.17 and Question 5.1.

We now state some open questions which are relevant to Table 2.

Question 5.1. Is PFO∗_{0} Π_{1}^{1}-equivalent to RCA∗_{0}? See Remark 4.17.

Question 5.2. What is the reverse-mathematical status of the statement that every strongly inductive ordered successor system is almost isomorphic to ℕ? We do not know whether this statement is provable in RCA∗_{0}. By Table 2 it is provable in each of the systems RCA_{0} and PFO∗_{0} and WKL∗_{0}.

Question 5.3. Does there exist a second-order characterization of ℕ which is provable in RCA∗_{0}? More precisely, does RCA∗_{0} prove the existence of a secondorder sentence or set of sentences T such that ℕ, 0, S is a second-order model of T and all second-order models of T are isomorphic to ℕ, 0, S? One may also consider the same question with RCA∗_{0} replaced by systems which are Π_{2}^{0}- equivalent to RCA∗_{0}.

References

[1] John P. Burgess. On the outside looking in: a caution about conservativeness. In [6], pages 128–141, 2009. 3

[2] Chi-Tat Chong, Theodore A. Slaman, and Yue Yang. Π_{1}^{1}- conservation of combinatorial principles weaker than Ramsey’s Theorem for pairs. Advances in Mathematics, 230(3):1060–1077, 2012. http://dx.doi.org/10.1016/j.aim.2012.02.025. 7, 14

[3] Richard Dedekind. Stetigkeit und irrationale Zahlen. Vieweg, Braunschweig, 1872. X + 31 pages. 2, 16

[4] Richard Dedekind. Was sind und was sollen die Zahlen? Vieweg, Braunschweig, 1888. XIX + 58 pages. 2, 3, 16

[5] Richard Dedekind. Essays on the Theory of Numbers. Dover, New York, 1963. V + 115 pages, translation of [3, 4]. 2, 3

[6] S. Feferman, C. Parsons, and S. G. Simpson, editors. Kurt Gödel: Essays for his Centennial. Number 33 in Lecture Notes in Logic. Association for Symbolic Logic, Cambridge University Press, 2010. X + 373 pages. 16, 17

[7] Harvey Friedman. Some systems of second order arithmetic and their use. In [11], pages 235–242, 1975. 2

[8] Harvey Friedman. Systems of second order arithmetic with restricted induction, I, II (abstracts). Journal of Symbolic Logic, 41:557–559, 1976. 2

[9] David Hilbert. Über das Unendliche. Mathematische Annalen, 95:161–190, 1926. 3

[10] Denis R. Hirschfeldt and Richard A. Shore. Combinatorial principles weaker than Ramsey’s theorem for pairs. Journal of Symbolic Logic, 72:171–206, 2007. 7, 10, 13, 14, 15 [11] Ralph D. James, editor. Proceedings of the International Congress of Math-

ematicians, Vancouver 1974, volume 1. Canadian Mathematical Congress, 1975. XLIX + 552 pages. 16

[12] Carl G. Jockusch, Jr. Semirecursive sets and positive reducibility. Transactions of the American Mathematical Society, 131:420–436, 1968. 13

[13] Carl G. Jockusch, Jr. Personal communication, March 2012. 13

[14] Elliott Mendelson. Number Systems and the Foundations of Analysis. Academic Press, 1973. XII + 358 pages. 2, 3

[15] R. Murawski, editor. Współczesna Filozofia Mathematyki, Wybór Tekstów [Contemporary Philosophy of Mathematics, Selected Readings]. Wydawnictwo Naukowe PWN, Warszawa, 2002. Translation, introduction and footnotes by Roman Murawski. 17

[16] Richard A. Shore. Personal communication, February 2012. 12

[17] Stephen G. Simpson. Partial realizations of Hilbert’s program. Journal of Symbolic Logic, 53:349–363, 1988. 3, 17

[18] Stephen G. Simpson. Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, 1999. XIV + 445 pages; Second Edition, Perspectives in Logic, Association for Symbolic Logic, Cambridge University Press, 2009, XVI+ 444 pages. 2, 3, 4, 6, 7, 10, 11, 12

[19] Stephen G. Simpson. Częściowe realizacje programu Hilberta. In [15], pages 189–213, 2002. Translation of [17]. Translation, introduction and footnotes by Roman Murawski. 3

[20] Stephen G. Simpson. The Gödel hierarchy and reverse mathematics. In [6], pages 109–127, 2010. 2, 3

[21] Stephen G. Simpson and Rick L. Smith. Factorization of polynomials and Σ_{1}^{0} induction. Annals of Pure and Applied Logic, 31:289–306, 1986. 3, 6, 7, 11, 12

[22] Jouko Väänänen. Second order logic or set theory? Bulletin of Symbolic Logic, 18(1):91–121, 2012. 3

[23] Keita Yokoyama. On the strength of Ramsey’s Theorem without Σ_{1}- induction. Mathematical Logic Quarterly, 59:108–111, 2013. 14