The Gödel Hierarchy and Reverse Mathematics

Stephen G. Simpson¹

Department of Mathematics

First draft: March 21, 2008
This draft: November 24, 2009

Pennsylvania State University

The Hilbert problems and Hilbert's Program

In 1900 the great mathematician David Hilbert laid down a list of 23 mathematical problems [32] which exercised a great influence on subsequent mathematical research. From the perspective of foundational studies, it is noteworthy that Hilbert's Problems 1 and 2 are squarely in the area of foundations of mathematics, while Problems 10 and 17 turned out to be closely related to mathematical logic.²

1.

Cantor's Problem of the Cardinal Number of the Continuum.

2.

Compatibility of the Arithmetical Axioms.

...

10.

Determination of the Solvability of a Diophantine Equation.

...

17.

Expression of Definite Forms by Squares.

...

Our starting point here is Problem 2, the consistency (= ``compatibility'') of the arithmetical axioms. In a later paper [33] published in 1926, Hilbert further elaborated his ideas on the importance of consistency proofs. Hilbert's Program [33] asks for a finitistic consistency proof for all of mathematics. Although we are not concerned with consistency proofs in Hilbert's sense, we are interested in certain logical structures which grew out of Hilbert's original concerns.

In answer to Hilbert's Problem 2 [32] and Hilbert's Program [33], Gödel [30] proved the famous Incompleteness Theorems. Let $T$ be any theory in the predicate calculus satisfying certain well-known mild conditions. Then we have the following results:

• $T$ is incomplete (First Incompleteness Theorem, Gödel 1931).
• The statement ``$T$ is consistent'' is not a theorem of $T$
  (Second Incompleteness Theorem, Gödel 1931).
• The problem of deciding whether a given formula is a theorem of $T$ is algorithmically unsolvable (Gödel, Turing, Rosser, Church, Tarski, ...).

Some commentators have asserted that the Incompleteness Theorems mark the end of the axiomatic method. However, I would argue that this view fails to take account of developments in the foundations of mathematics subsequent to 1931. The purpose of this paper is to call attention to some relatively recent research which reveals a large amount of logical regularity and structure arising from the Incompleteness Theorems and from the axiomatic approach to foundations of mathematics.³ We shall comment on the following topics:

• The Gödel Hierarchy.
• Reverse Mathematics.
• Foundational consequences of Reverse Mathematics.
• A partial realization of Hilbert's Program.

The Gödel Hierarchy

Using the Second Incompleteness Theorem as our jumping-off point, we define an ordering of theories as follows. Let $T_1$ and $T_2$ be two theories as above. We write

$$T_1 < T_2$$

to mean that the statement ``$T_1$ is consistent'' is a theorem of $T_2$. One sometimes says that the consistency strength of $T_1$ is less than that of $T_2$. Often this goes hand-in-hand with saying that $T_1$ is interpretable in $T_2$ and not vice versa. We may think of $T_2>T_1$ as meaning that $T_2$ is ``more abstract'' or ``harder to interpret'' or ``less concrete'' or ``less meaningful'' or ``less surely consistent'' than $T_1$.

It is known that the $<$ ordering gives rise to a hierarchy of foundationally significant theories, ordered by consistency strength. We dub this the Gödel Hierarchy, because it seems to us that the possibility of such a hierarchy became apparent through the work of Gödel. In any case, the Gödel Hierarchy has been a central object of study in foundations of mathematics subsequent to 1931. It turns out that the Gödel Hierarchy exhibits a number of remarkable regularities, including a kind of linearity.

Table 1: Some benchmarks in the Gödel Hierarchy.

A schematic representation of the Gödel Hierarchy is in Table 1. Each of the theories in Table 1 is of considerable significance for the foundations of mathematics. Generally speaking, the idea of Table 1 is that the lower theories are below the higher theories with respect to the $<$ ordering. The exception is that $\mathsf{PRA}$, $\mathsf{RCA}_0$, and $\mathsf{WKL}_0$ are all of the same consistency strength. A number of these theories will be described below in connection with Reverse Mathematics.

It is striking that a great many foundational theories are linearly ordered by $<$. Of course it is possible to construct pairs of artificial theories which are incomparable under $<$. However, this is not the case for the ``natural'' or non-artificial theories which are usually regarded as significant in the foundations of mathematics. The problem of explaining this observed regularity is a challenge for future foundational research.

As an alternative to the $<$ ordering, one may consider a somewhat different ordering, the inclusion ordering. Our jumping-off point here is the First Incompleteness Theorem. Assuming that the language of $T_1$ is part of the language of $T_2$, let us write

$$T_1 \subset T_2$$

to mean that the sentences which are theorems of $T_1$ form a proper subset of the sentences in the language of $T_1$ which are theorems of $T_2$. We may think of $T_2\supset T_1$ as meaning that $T_2$ is ``more powerful'' or ``stronger'' than $T_1$. In many cases the $<$ ordering and the $\subset$ ordering coincide. In Table 1 the lower theories are always below the higher theories with respect to the $\subset$ ordering.

In addition to the observed linearity noted above, another kind of observed regularity is the existence of repeating patterns at various levels of the Gödel Hierarchy. For example, the foundationally significant analogies

$$\frac{\mathsf{RCA}_0}{\mathsf{WKL}_0}\quad=\quad\frac{\Delta^1_1\hbox{-}\mathsf{CA}_0}{\mathsf{ATR}_0}$$

and

$$\frac{\mathsf{WKL}_0}{\mathsf{ACA}_0}\quad=\quad\frac{\mathsf{ATR}_0}{\Pi^1_1\hbox{-}\mathsf{CA}_0}$$

have been explored by Simpson [72, Remark I.11.7, Chapter VIII].

Foundations of mathematics

Foundations of mathematics (f.o.m.) is the study of the most basic concepts and logical structure of mathematics as a whole. Among the most basic mathematical concepts are: number, shape, set, function, algorithm, computability, randomness, mathematical proof, mathematical definition, mathematical axiom, mathematical theorem.

I set up the FOM list in 1997⁴ and ran it during the years 1997-2002 as an electronic forum for lively discussion of issues and programs in f.o.m. Currently the FOM list resides at http://www.cs.nyu.edu/mailman/listinfo/fom/ and is moderated by Martin Davis with the help of an editorial board. Both the FOM list and my book Subsystems of Second Order Arithmetic [72] were developed in order to promote a sometimes controversial idea:

Mathematical logic is or ought to be driven by f.o.m. considerations.

A crucially important f.o.m. question which we shall study below is:

What axioms are needed in order to prove particular mathematical theorems?

Subsystems of second-order arithmetic

Second-order arithmetic, denoted $\mathsf{Z}_2$, is a theory with two sorts of variables. There are number variables $m,n,\ldots$ intended to range over the set of natural numbers $\mathbb{N}=\{0,1,2,\ldots\}$ and set variables $X,Y,\ldots$ intended to range over subsets of $\mathbb{N}$. In addition the language of $\mathsf{Z}_2$ includes the predicates $+$ and $\times$ intended to denote addition and multiplication on $\mathbb{N}$, as well as the membership predicate $\in$ intended to denote the membership relation

$${\in}\quad=\quad\{(n,X)\mid n\in X\}\quad\subseteq\quad\mathbb{N}\times P(\mathbb{N})$$

on $\mathbb{N}\times P(\mathbb{N})$. Here $P(\mathbb{N})$ is the powerset of $\mathbb{N}$, i.e., the set of all subsets of $\mathbb{N}$. In addition $\mathsf{Z}_2$ has the usual apparatus of the predicate calculus including propositional connectives $\lnot ,\land,\lor,\Rightarrow ,\Leftrightarrow$, number quantifiers $\forall n,\exists n$, and set quantifiers $\forall X,\exists X$.

The axioms of $\mathsf{Z}_2$ express basic properties of $\mathbb{N}$ and $P(\mathbb{N})$. Among the axioms are all instances of the full comprehension scheme consisting of the universal closures of all formulas of the form

$$\exists X \forall n (n\in X\Leftrightarrow \Phi(n))$$

where $\Phi(n)$ is any formula in which the set variable $X$ does not occur freely.

A basic foundational discovery essentially due to Hilbert/Bernays [34, Supplement IV] is that it is possible to formalize the vast majority⁵ of rigorous core mathematics within $\mathsf{Z}_2$. Virtually every theorem of rigorous core mathematics (including the key theorems of analysis, algebra, geometry, combinatorics, etc.) can be formalized as a sentence in the language of of $\mathsf{Z}_2$, and in virtually all cases these sentences are then provable as theorems of $\mathsf{Z}_2$.

Later Kreisel [45] emphasized the importance of subsystems of $\mathsf{Z}_2$. By a subsystem of $\mathsf{Z}_2$ we mean any theory in the language of $\mathsf{Z}_2$ which is $\subset\mathsf{Z}_2$. For example, if we restrict the comprehension scheme of $\mathsf{Z}_2$ to formulas $\Phi(n)$ with a fixed finite number of set quantifiers, the resulting theory is both $<\mathsf{Z}_2$ and $\subset\mathsf{Z}_2$. Thus we have infinitely many different subsystems of $\mathsf{Z}_2$. It can be shown that $\mathsf{Z}_2$ itself is not finitely axiomatizable, but trivially each theorem of $\mathsf{Z}_2$ is provable in some finitely axiomatizable subsystem of $\mathsf{Z}_2$ obtained by discarding all but finitely many of the axioms of $\mathsf{Z}_2$. Therefore, in view of Hilbert/Bernays [34, Supplement IV], it becomes interesting to try to correlate particular theorems of rigorous mathematics with the subsystems of $\mathsf{Z}_2$ in which they are provable. Thus subsystems of $\mathsf{Z}_2$ emerge as benchmarks for the classification of rigorous mathematical theorems according to their ``logical strength.'' This kind of calibration was apparently first pioneered by Kreisel.

Subsequently subsystems of $\mathsf{Z}_2$ were investigated by a number of researchers including Kreisel [45,46], Feferman [17,18], Friedman [23,24,25], Simpson (numerous publications including [72]) and Simpson's Ph.D. students.⁶ Some interesting subsystems of $\mathsf{Z}_2$ appear in Table 1: $\mathsf{RCA}_0$, $\mathsf{WKL}_0$, $\mathsf{ACA}_0$, $\mathsf{ATR}_0$, $\Pi^1_1$-$\mathsf{CA}_0$, $\Pi^1_2$-$\mathsf{CA}_0$.⁷ As an outcome of ongoing research, it is now fair to say that subsystems of $\mathsf{Z}_2$ are basic for our current understanding of the logical structure of contemporary rigorous mathematics. An important component of this understanding is Reverse Mathematics, as we shall now explain.

Reverse Mathematics

Given a mathematical theorem $\tau$, let $S_\tau$ be the ``weakest natural''⁸ subsystem of $\mathsf{Z}_2$ in which $\tau$ is provable. The following widespread phenomena have been observed:

• Often it is possible to determine $S_\tau$ exactly. In other words, $S_\tau\vdash\tau$ and there is no ``natural'' $S\subset S_\tau$ such that $S\vdash\tau$.
• In such cases it often turns out that $S_\tau$ and $\tau$ are logically equivalent over a much weaker subsystem $S$. In other words, $S\vdash S_\tau\Leftrightarrow \tau$ for some $S\subset S_\tau$. (In particular $S_\tau$ is finitely axiomatizable over $S$.)
• Only a relatively small number of subsystems of $\mathsf{Z}_2$ tend to arise repeatedly as $S_\tau$ in this context.

Thus we obtain an illuminating classification of mathematical theorems up to logical equivalence over weak base theories in which the theorems in question are not provable.

As an example, consider the well-known Perfect Set Theorem: every uncountable closed set in Euclidean space includes a perfect set. It has been shown (see [72, Theorem V.5.5]) that the Perfect Set Theorem is logically equivalent to $\mathsf{ATR}_0$ over the much weaker system $\mathsf{RCA}_0$. Thus we have $S_\tau=\mathsf{ATR}_0$ where $\tau$ is the Perfect Set Theorem as formalized in the language of $\mathsf{Z}_2$.

As a second example, consider the Lusin Separation Theorem in descriptive set theory: any disjoint pair of analytic sets is separated by a Borel set. The Reverse Mathematics investigations of Simpson [72, Sections V.3 and V.5] have shown that Lusin's Theorem, like the Perfect Set Theorem, is logically equivalent to $\mathsf{ATR}_0$ over $\mathsf{RCA}_0$.

As a third example, define a countable bipartite graph to be a set $E\subseteq\mathbb{N}\times\mathbb{N}$. A matching is a set $M\subseteq E$ such that $i=m$ if and only if $j=n$ for all $(i,j)\in M$ and $(m,n)\in M$. A covering is a set $C\subseteq\mathbb{N}$ such that for all $(i,j)\in E$ at least one of $i,j$ belongs to $C$. A König covering consists of a matching $M$ and a covering $C$ such that for all $(i,j)\in M$ exactly one of $i,j$ belongs to $C$. The Podewski/Steffens Theorem [59] asserts that every countable bipartite graph has a König covering. The Reverse Mathematics investigations of Aharoni/Magidor/Shore [2] and Simpson [71] have shown that the Podewski/Steffens Theorem, like the Perfect Set Theorem and Lusin's Theorem, is logically equivalent to $\mathsf{ATR}_0$ over $\mathsf{RCA}_0$.

Combining these three examples, we obtain the odd-looking result that the Perfect Set Theorem, Lusin's Theorem, and the Podewski/Steffens Theorem are pairwise logically equivalent (over $\mathsf{RCA}_0$). Thus these three theorems coming from completely different branches of mathematics have been classified into precisely the same equivalence class (modulo logical equivalence over $\mathsf{RCA}_0$) and calibrated at precisely the same level of consistency strength in the Gödel Hierarchy.

Remarkably, a series of case studies of this kind has revealed a clear pattern which is documented in my book [72]. Namely, a large number of mathematical theorems (several hundreds at least) fall into a small number of equivalence classes (five).

This completes our broad outline of the ongoing program of Reverse Mathematics as developed in [72, Part A] and in many research papers. The foundational significance of this program will be discussed below.

The basic reference on Reverse Mathematics is Part A of my 1999 book [72]. A more up-to-date reference on Reverse Mathematics is the 2005 volume [67] which includes papers by a number of prominent researchers.

The Big Five

Table 2: Mathematics in the Big Five.

	$\mathsf{RCA}_0$	$\mathsf{WKL}_0$	$\mathsf{ACA}_0$	$\mathsf{ATR}_0$	$\Pi^1_1$-$\mathsf{CA}_0$
analysis (separable):
differential equations	$\times$	$\times$
continuous functions	$\times$	$\times$	$\times$
completeness, etc.	$\times$	$\times$	$\times$
Banach spaces	$\times$	$\times$	$\times$		$\times$
open and closed sets	$\times$	$\times$		$\times$	$\times$
Borel and analytic sets	$\times$			$\times$	$\times$
algebra (countable):
countable fields	$\times$	$\times$	$\times$
commutative rings	$\times$	$\times$	$\times$
vector spaces	$\times$		$\times$
Abelian groups	$\times$		$\times$	$\times$	$\times$
miscellaneous:
mathematical logic	$\times$	$\times$
countable ordinals	$\times$		$\times$	$\times$
infinite matchings		$\times$	$\times$	$\times$
the Ramsey property			$\times$	$\times$	$\times$
infinite games			$\times$	$\times$	$\times$

The five most important subsystems of $\mathsf{Z}_2$ for Reverse Mathematics are:

1. $\mathsf{RCA}_0$ (Recursive Comprehension Axiom). This is a kind of formalized recursive or computable mathematics. The $\omega$-models of $\mathsf{RCA}_0$ are precisely the nonempty subsets of $P(\mathbb{N})$ which are closed under Turing reducibility. The smallest $\omega$-model of $\mathsf{RCA}_0$ is $\mathrm{REC}=\{X\mid X$ is recursive$\}$.
2. $\mathsf{WKL}_0$ (Weak König's Lemma). This consists of $\mathsf{RCA}_0$ plus a compactness principle: every infinite subtree of the full binary tree has an infinite path. The $\omega$-models of $\mathsf{WKL}_0$ are precisely the Scott systems [63]. $\mathrm{REC}$ is not an $\omega$-model of $\mathsf{WKL}_0$, but it is the intersection of all such models.
3. $\mathsf{ACA}_0$ (Arithmetical Comprehension Axiom). This consists of $\mathsf{RCA}_0$ plus the comprehension scheme restricted to formulas $\Phi(n)$ with no set quantifiers. The $\omega$-models of $\mathsf{ACA}_0$ are the nonempty subsets of $P(\mathbb{N})$ which are closed under Turing reducibility and the Turing jump operator. The smallest $\omega$-model of $\mathsf{ACA}_0$ is $\mathrm{ARITH}=\{X\mid\exists n (X\le_T0^{(n)})\}$ where $0^{(n)}$ is the $n$th Turing jump of $0$.
4. $\mathsf{ATR}_0$ (Arithmetical Transfinite Recursion). This consists of $\mathsf{RCA}_0$ plus an axiom saying that the Turing jump operator, or equivalently arithmetical comprehension, can be iterated along any countable well-ordering. Each $\omega$-model of $\mathsf{ATR}_0$ is closed under relative hyperarithmeticity. The $\omega$-model $\mathrm{HYP}=\{X\mid X$ is hyperarithmetical$\}$ is not itself an $\omega$-model of $\mathsf{ATR}_0$, but it is the intersection of all such models. In fact, $\mathrm{HYP}$ is the intersection of all $\beta$-models of $\mathsf{ATR}_0$ (Simpson [72, VII.2.7 and VIII.6.11]).
5. $\Pi^1_1$-$\mathsf{CA}_0$ ($\Pi^1_1$ Comprehension Axiom). This consists of $\mathsf{RCA}_0$ plus the comprehension scheme restricted to formulas $\Phi(n)$ with exactly one set quantifier. The smallest $\beta$-model of $\Pi^1_1$-$\mathsf{CA}_0$ is $\{X\mid\exists n (X\le_T0^{(n)})\}$ where $0^{(n)}$ is the $n$th hyperjump of $0$.

These five systems correspond to Chapters II through VI of my book [72] and are colloquially known as ``the Big Five.'' Table 2 gives a rough indication of which kinds of mathematical theorems are provable in which of these subsystems of $\mathsf{Z}_2$. Each $\times$ in the table indicates that there are some theorems in the given branch of mathematics which fall at the given level of the Gödel Hierarchy. Some of these results are listed below.

In Reverse Mathematics to date, the most useful base theory has been $\mathsf{RCA}_0$, and the most useful benchmark systems have been $\mathsf{WKL}_0$, $\mathsf{ACA}_0$, $\mathsf{ATR}_0$ and $\Pi^1_1$-$\mathsf{CA}_0$. We shall now list some of these results. References for these results may be found in [72].

Reverse Mathematics for $\mathsf{WKL}_0$

$\mathsf{WKL}_0$ is equivalent over $\mathsf{RCA}_0$ to each of the following mathematical theorems:

1. The Heine/Borel Covering Lemma: Every covering of $[0,1]$ by a sequence of open intervals has a finite subcovering.
2. Every covering of a compact metric space by a sequence of open sets has a finite subcovering.
3. Every continuous real-valued function on $[0,1]$ (or on any compact metric space) is bounded (uniformly continuous, Riemann integrable).
4. The Maximum Principle: Every continuous real-valued function on $[0,1]$ (or on any compact metric space) has (or attains) a supremum.
5. The local existence theorem for solutions of (finite systems of) ordinary differential equations.
6. Gödel's Completeness Theorem: every consistent finite (or countable) set of sentences in the predicate calculus has a countable model.
7. Gödel's Compactness Theorem: a countable set of sentences in the predicate calculus is satisfiable if and only if it is finitely satisfiable.
8. Every countable commutative ring has a prime ideal.
9. Every countable field (of characteristic $0$) has a unique algebraic closure.
10. Every countable formally real field is orderable.
11. Every countable formally real field has a (unique) real closure.
12. Brouwer's Fixed Point Theorem: Every (uniformly) continuous function $\phi:[0,1]^n\to[0,1]^n$ has a fixed point.
13. The Separable Hahn/Banach Theorem: If $f$ is a bounded linear functional on a subspace of a separable Banach space, and if $\Vert f\Vert\le1$, then $f$ has an extension $\widetilde{f}$ to the whole space such that $\Vert\widetilde{f}\Vert\le1$.
14. Banach's Theorem: In a separable Banach space, given two disjoint convex open sets $A$ and $B$, there exists a closed hyperplane $H$ such that $A$ is on one side of $H$ and $B$ is on the other.
15. The existence and uniqueness of Haar measure on separable, locally compact groups.
16. Every countable $k$-regular bipartite graph has a perfect matching.

Reverse Mathematics for $\mathsf{ACA}_0$

$\mathsf{ACA}_0$ is equivalent over $\mathsf{RCA}_0$ to each of the following mathematical theorems:

1. Every bounded, or bounded increasing, sequence of real numbers has a least upper bound.
2. The Bolzano/Weierstraß Theorem: Every bounded sequence of real numbers, or of points in $\mathbb{R}^n$, has a convergent subsequence.
3. Every sequence of points in a compact metric space has a convergent subsequence.
4. The Ascoli Lemma: Every bounded equicontinuous sequence of real-valued continuous functions on a bounded interval has a uniformly convergent subsequence.
5. Every countable commutative ring has a maximal ideal.
6. Every countable vector space (over $\mathbb{Q}$) has a basis.
7. Every countable field (of characteristic $0$) has a transcendence basis.
8. Every countable Abelian group has a unique divisible closure.
9. König's Lemma: Every infinite, finitely branching tree has an infinite path.
10. Ramsey's Theorem for colorings of $[\mathbb{N}]^3$ (or of $[\mathbb{N}]^k$ for any fixed $k\ge3$).

Reverse Mathematics for $\mathsf{ATR}_0$

$\mathsf{ATR}_0$ is equivalent over $\mathsf{RCA}_0$ to each of the following mathematical theorems:

1. Any two countable well-orderings are comparable.
2. Ulm's Theorem: Any two countable reduced Abelian $p$-groups which have the same Ulm invariants are isomorphic.
3. The Perfect Set Theorem: Every uncountable closed, or analytic, set has a perfect subset.
4. Lusin's Separation Theorem: Any two disjoint analytic sets can be separated by a Borel set.
5. The domain of any single-valued Borel set in the plane is a Borel set.
6. Every clopen (or open) game in $\mathbb{N}^\mathbb{N}$ is determined.
7. Every clopen (or open) subset of $[\mathbb{N}]^\mathbb{N}$ has the Ramsey property.
8. Every countable bipartite graph admits a König covering.

Reverse Mathematics for $\Pi^1_1$-$\mathsf{CA}_0$

$\Pi^1_1$-$\mathsf{CA}_0$ is equivalent over $\mathsf{RCA}_0$ to each of the following mathematical theorems:

1. Every tree has a largest perfect subtree.
2. The Cantor/Bendixson Theorem: Every closed subset of $\mathbb{R}$ (or of any complete separable metric space) is the union of a countable set and a perfect set.
3. Every countable Abelian group is the direct sum of a divisible group and a reduced group.
4. Every difference of two open sets in the Baire space $\mathbb{N}^\mathbb{N}$ is determined.
5. Every $\mathrm{G}_\delta$ set in $[\mathbb{N}]^\mathbb{N}$ has the Ramsey property.
6. Silver's Theorem: For every Borel (or coanalytic, or $\mathrm{F}_\sigma$) equivalence relation with uncountably many equivalence classes, there exists a perfect set of inequivalent elements.
7. For every countable set $S$ in the dual $X^*$ of a separable Banach space $X$ (or in $l_1=c_0^*$), there exists a smallest weak-$*$-closed subspace of $X^*$ (or of $l_1$ respectively) containing $S$.
8. For every norm-closed subspace $Y$ of $l_1=c_0^*$, the weak-$*$-closure of $Y$ exists.

Foundational implications

Reverse Mathematics and the Big Five have a number of implications for the foundations of mathematics. We briefly mention some of these implications.

Formalization

In Reverse Mathematics, specific mathematical theorems are classified according to the subsystems of $\mathsf{Z}_2$ in which they are formally provable. This kind of classification provides data which are of obvious interest from the viewpoint of the Russell/Whitehead formalization program.

Mathematical naturalness

As a byproduct of Reverse Mathematics, certain specific subsystems of $\mathsf{Z}_2$ are identified as being mathematically natural, and the naturalness is rigorously demonstrated.

Namely, a subsystem $S$ of $\mathsf{Z}_2$ is to be considered mathematically natural if we can find one or more core mathematical theorems $\tau$ such that $S\Leftrightarrow \tau$ is provable over a weak base theory.⁹ In particular, there is abundant evidence (some of which has been presented above) that $\mathsf{WKL}_0$, $\mathsf{ACA}_0$, $\mathsf{ATR}_0$, and $\Pi^1_1$-$\mathsf{CA}_0$ are mathematically natural in this sense.

Consequences of foundational programs

With the help of Reverse Mathematics, we can explore the consequences of particular f.o.m. doctrines and programs, including:

1. computable analysis (see Aberth [1], Pour-El/Richards [60]).
2. finitistic reductionism (see Hilbert [33]).
3. predicativity (see Weyl [87,88], Kreisel [45], Feferman [17,18,21]).
4. predicative reductionism (see Feferman [19], Simpson [73], and Friedman/McAloon/Simpson [26]).
5. impredicative or $\Pi^1_1$ analysis (see Buchholz et al. [11]).

From the foundational viewpoint, it is desirable to understand what each of these programs would mean in terms of their consequences for mathematical practice. Reverse Mathematics provides data which can be of great importance for such understanding.

Note first that each of the above programs focuses on a certain restricted portion of mathematics which is asserted to be of special foundational significance. Moreover, in each case, the portion of mathematics in question is at least roughly identifiable as that which can be developed within a particular subsystem of $\mathsf{Z}_2$. Thus certain subsystems of $\mathsf{Z}_2$ are seen to be of foundational interest. See Table 3. The question then arises, which mathematical theorems would be ``lost'' by such a restriction? Reverse Mathematics provides rigorous answers to such questions, by telling us which mathematical theorems are and are not provable in which subsystems of $\mathsf{Z}_2$.

We now discuss two examples: the Cinq Lettres Program [3] and Hilbert's Program [33].

Table 3: Foundational programs and the Big Five.

$\mathsf{RCA}_0$	computable mathematics	Pour-El/Richards
$\mathsf{WKL}_0$	finitistic reductionism	Hilbert
$\mathsf{ACA}_0$	predicativity	Weyl, Feferman
$\mathsf{ATR}_0$	predicative reductionism	Feferman, Friedman, Simpson
$\Pi^1_1$-$\mathsf{CA}_0$	impredicativity	Buchholz et al.

The Cinq Lettres Program

An interesting exchange of letters among Baire, Borel, Hadamard and Lebesgue concerning the foundations of set theory has been preserved in [3]. These great mathematicians were horrified by the existence of arbitrary or pathological sets of points in Euclidean space. To remedy this difficulty, they proposed to restrict attention to well-behaved sets, such as Lebesgue measurable sets or Borel sets.

As a result of relatively recent research in Reverse Mathematics [72, Section V.3], it is now known that the basic theory of Borel and analytic sets (the Lusin Separation Theorem, etc.) can be developed in $\mathsf{ATR}_0$. Moreover, it is known proof-theoretically (see Friedman/McAloon/Simpson [26]) that $\mathsf{ATR}_0$ is $\Pi^1_1$-conservative over Feferman's systems of predicative mathematics [17,18]. Thus all $\Pi^1_1$ or arithmetical theorems of Borel mathematics are predicatively provable, and it becomes possible to argue that restricted mathematics in the Cinq Lettres style is predicatively reducible in this sense.

A partial realization of Hilbert's Program

Hilbert's Program [33] calls for all of mathematics to be reduced to finitism. Namely, each finitistically meaningful theorem is to be given a finitistic proof. The Second Incompleteness Theorem of Gödel [30] implies that Hilbert's Program cannot be completely realized. For instance, the statement ``finitism is consistent'' (assuming a precise formal analysis of finitism) is finitistically meaningful yet not finitistically provable.

Nevertheless, a significant partial realization of Hilbert's Program has been obtained:

1. Tait [80] has argued that $\mathsf{PRA}$ (Primitive Recursive Arithmetic) embodies all of finitistic mathematics.
2. Parsons [58] and Friedman (unpublished, but see [72, Section IX.3])¹⁰ have shown that $\mathsf{WKL}_0$ is conservative¹¹ over $\mathsf{PRA}$ for $\Pi^0_2$ sentences. Moreover, Tait's argument shows that this class of sentences includes all finitistically meaningful sentences.
3. A large portion of core mathematics, including many of the best known nonconstructive theorems, can be carried out in $\mathsf{WKL}_0$. A sampling of these results is included in the above discussion of Reverse Mathematics in $\mathsf{WKL}_0$. See also Simpson [72, Chapter IV].
4. In addition to $\mathsf{WKL}_0$ there are other subsystems of $\mathsf{Z}_2$ which are likewise $\Pi^0_2$-conservative over $\mathsf{PRA}$ and which suffice to prove even more core mathematical theorems concerning measure theory and Baire category theory. See for instance Brown/Simpson [10] and Brown/Giusto/Simpson [8].

Thus we see that a large portion of rigorous core mathematics is finitistically reducible. The general intellectual significance of this partial realization of Hilbert's Program has been argued vigorously in Simpson [70].

Beyond the Big Five

In addition to the Big Five, a number of other subsystems of $\mathsf{Z}_2$ have arisen in Reverse Mathematics.

The most striking recent discovery is the existence of Reverse Mathematics at the level of $\Pi^1_2$ comprehension,¹² thus going far beyond the Big Five as measured by the Gödel Hierarchy. We now describe this result briefly.

Mummert [54] and Mummert/Simpson [55] have initiated the Reverse Mathematics of general topology. The relevant definitions are as follows. Let $P$ be a partially ordered set. A filter¹³ on $P$ is a set $F\subseteq P$ such that (a) $p\in F,p\le q$ imply $q\in F$, and (b) $p\in F,q\in F$ imply $\exists r (r\in F,r\le p,r\le q)$. A maximal filter on $P$ is a filter on $P$ which is not properly included in any other filter on $P$. Let $\MF (P)$ be the topological space whose points are the maximal filters on $P$ and whose basic open sets are of the form $\{F\in\MF (P)\mid p\in F\}$ where $p\in P$. It can be shown that all complete metric spaces and many nonmetrizable topological spaces are homeomorphic to spaces of the form $\MF (P)$ where $P$ is a partially ordered set. Moreover, every complete separable¹⁴ metric space is homeomorphic to $\MF (P)$ for some countable partially ordered set $P$.

A topological space is said to be completely metrizable if it is homeomorphic to a complete metric space. A topological space is said to be regular if its topology has a base consisting of closed sets. It is well-known and easy to see that every metrizable topological space is regular. Let $\mathrm{MFMT}$ be the following metrization theorem:

Given a countable partially ordered set $P$, the topological space $\MF (P)$ is completely metrizable if and only if it is regular.

It can be shown (see [55]) that $\mathrm{MFMT}$ is an easy consequence of well-known metrization theorems due to Urysohn and Choquet. It is straightforward to formalize $\mathrm{MFMT}$ as a sentence in the language of $\mathsf{Z}_2$.

Mummert/Simpson [55] have shown that $\mathrm{MFMT}$ is equivalent to $\Pi^1_2$-$\mathsf{CA}_0$ over $\Pi^1_1$-$\mathsf{CA}_0$. Thus we have a convincing instance of Reverse Mathematics at the level of $\Pi^1_2$ comprehension.

In addition to Mummert/Simpson [55], a number of researchers have discovered Reverse Mathematics at other levels of the Gödel Hierarchy. We now list and describe these developments in order of increasing consistency strength.

1. Simpson/Smith [76] (see also [72, Section X.4]) introduced a system $\mathsf{RCA}_0^*$ which is $<\mathsf{RCA}_0$ and $\subset\mathsf{RCA}_0$. They showed that
   $\mathsf{RCA}_0\quad=\quad\mathsf{RCA}_0^* + \Sigma^0_1$ induction
   and that $\mathsf{RCA}_0^*$ can replace $\mathsf{RCA}_0$ as the base theory in much of Reverse Mathematics. Moreover, a number of core mathematical theorems (e.g., the fact that every polynomial can be factored into irreducible polynomials) are equivalent to $\mathsf{RCA}_0$ over $\mathsf{RCA}_0^*$.
2. Yu [89] introduced a system $\mathsf{WWKL}_0$ which arises repeatedly in the Reverse Mathematics of measure theory. For example, $\mathsf{WWKL}_0$ is equivalent over $\mathsf{RCA}_0$ to a formal statement of the Vitali Covering Theorem [8]. It turns out that $\mathsf{WWKL}_0$ is strictly intermediate between $\mathsf{RCA}_0$ and $\mathsf{WKL}_0$ and is closely related to algorithmic randomness in the sense of Martin/Löf [50]. See also Simpson [72, Section X.1] and Brown/Giusto/Simpson [8].
3. Cholak/Jockusch/Slaman [14] and Hirschfeldt/Shore [35] have studied a number of Reverse Mathematics questions centering around
   $\mathrm{RT}(2) =$ Ramsey's Theorem for exponent 2.
   A problem which remains open is to determine exactly the consistency strength of $\mathsf{RCA}_0+\mathrm{RT}(2)$. It is also open whether $\mathsf{WKL}_0\subset\mathsf{RCA}_0+\mathrm{RT}(2)$. It is known that not all $\omega$-models of $\mathsf{WKL}_0$ satisfy $\mathrm{RT}(2)$.
4. Beginning with Dobrinen/Simpson [16] there has been an explosion of activity in the Reverse Mathematics of measure-theoretic regularity. This turns out to be closely related to the study of low-for-randomness in the sense of Kucera/Terwijn [48]. In addition to [16] see also Binns et al. [4], Cholak/Greenberg/Miller [13], Kjos-Hanssen [42], Simpson [74,75], and Kjos-Hanssen/Miller/Solomon [43].
5. Simpson [69] has performed an axiomatic study of so-called basis theorems for ideals in commutative and noncommutative rings, leading to Reverse Mathematics at the levels
   $\mathsf{RCA}_0 + \omega^\omega$ is well-ordered
   and
   $\mathsf{RCA}_0 + \omega^{\omega^\omega}$ is well-ordered
   in the Gödel Hierarchy. It is known that these theories are strictly intermediate between $\mathsf{RCA}_0$ and $\mathsf{ACA}_0$ with respect to the $<$ and $\subset$ orderings, and incomparable with $\mathsf{WKL}_0$ with respect to the $\subset$ ordering.
6. Rathjen/Weiermann [61] (building on unpublished work of H. Friedman) have performed an axiomatic study of Kruskal's Theorem in graph theory, leading to Reverse Mathematics at the level
   $\mathsf{RCA}_0 + \vartheta\Omega^\omega$ is well-ordered
   where $\vartheta\Omega^\omega$ is the Ackermann ordinal, a.k.a., the small Veblen ordinal. It is known that this theory is strictly intermediate between $\mathsf{ATR}_0$ and $\Pi^1_1$-$\mathsf{CA}_0$ with respect to the $<$ ordering and incomparable with $\mathsf{ACA}_0$ and $\mathsf{ATR}_0$ with respect to the $\subset$ ordering.
7. Tanaka [83,84] (see also [72, Section VI.7]) and his colleagues MedSalem and Nemoto (see [51,56,57]) have investigated the Reverse Mathematics of determinacy at various levels of the arithmetical hierarchy. Some of the subsystems of $\mathsf{Z}_2$ which arise in this way are strictly intermediate between $\Pi^1_1$-$\mathsf{CA}_0$ and $\Pi^1_2$-$\mathsf{CA}_0$.

Thus we see that the Gödel Hierarchy and Reverse Mathematics can be expected to persist as significant f.o.m. research areas for a long time to come.

Bibliography

1

Oliver Aberth.
Computable Analysis.
McGraw-Hill, 1980.
XI + 187 pages.

2

Ron Aharoni, Menachem Magidor, and Richard A. Shore.
On the strength of König's duality theorem for infinite bipartite graphs.
Journal of Combinatorial Theory, Series B, 54:257-290, 1992.

3

René Baire, Émile Borel, Jacques Hadamard, and Henri Lebesgue.
Cinq lettres sur la théorie des ensembles.
Bulletin de la Société Mathématique de France, 33:261-273, 1905.
Reprinted in [5, pp. 150-160]. English translation in [53, pp. 311-320].

4

Stephen Binns, Bjørn Kjos-Hanssen, Manuel Lerman, and David Reed Solomon.
On a question of Dobrinen and Simpson concerning almost everywhere domination.
Journal of Symbolic Logic, 71:119-136, 2006.

5

Émile Borel.
Leçons sur la Théorie des Fonctions.
Gauthier-Villars, Paris, 3nd edition, 1928.
XII + 293 pages.

6

Stephen H. Brackin.
On Ramsey-type Theorems and their Provability in Weak Formal Systems.
PhD thesis, Pennsylvania State University, 1984.

7

Douglas K. Brown.
Functional Analysis in Weak Subsystems of Second Order Arithmetic.
PhD thesis, The Pennsylvania State University, 1987.
VII + 150 pages.

8

Douglas K. Brown, Mariagnese Giusto, and Stephen G. Simpson.
Vitali's theorem and WWKL.
Archive for Mathematical Logic, 41:191-206, 2002.

9

Douglas K. Brown and Stephen G. Simpson.
Which set existence axioms are needed to prove the separable Hahn-Banach theorem?
Annals of Pure and Applied Logic, 31:123-144, 1986.

10

Douglas K. Brown and Stephen G. Simpson.
The Baire category theorem in weak subsystems of second order arithmetic.
Journal of Symbolic Logic, 58:557-578, 1993.

11

Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg.
Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies.
Number 897 in Lecture Notes in Mathematics. Springer-Verlag, 1981.
V + 383 pages.

12

John P. Burgess.
On the outside looking in: a caution about conservativeness.
In this volume.

13

Peter Cholak, Noam Greenberg, and Joseph S. Miller.
Uniform almost everywhere domination.
Journal of Symbolic Logic, 71:1057-1072, 2006.

14

Peter A. Cholak, Carl G. Jockusch, Jr., and Theodore A. Slaman.
On the strength of Ramsey's theorem for pairs.
Journal of Symbolic Logic, 66:1-55, 2001.

15

J. C. E. Dekker, editor.
Recursive Function Theory.
Proceedings of Symposia in Pure Mathematics. American Mathematical Society, 1962.
VII + 247 pages.

16

Natasha L. Dobrinen and Stephen G. Simpson.
Almost everywhere domination.
Journal of Symbolic Logic, 69:914-922, 2004.

17

Solomon Feferman.
Systems of predicative analysis, I.
Journal of Symbolic Logic, 29:1-30, 1964.

18

Solomon Feferman.
Systems of predicative analysis, II.
Journal of Symbolic Logic, 33:193-220, 1968.

19

Solomon Feferman.
Predicatively reducible systems of set theory.
In [40], pages 11-32, 1974.

20

Solomon Feferman.
In the Light of Logic.
Oxford University Press, 1998.
XII + 340 pages.

21

Solomon Feferman.
Weyl vindicated: Das Kontinuum seventy years later.
In [20], pages 249-283, 1998.

22

Fernando Ferreira.
Polynomial Time Computable Arithmetic and Conservative Extensions.
PhD thesis, Pennsylvania State University, 1988.

23

Harvey Friedman.
Bar induction and $\Pi^1_1$-$\mathsf{CA}$.
Journal of Symbolic Logic, 34:353-362, 1969.

24

Harvey Friedman.
Some systems of second order arithmetic and their use.
In Proceedings of the International Congress of Mathematicians, Vancouver 1974, volume 1, pages 235-242. Canadian Mathematical Congress, 1975.

25

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

26

Harvey Friedman, Kenneth McAloon, and Stephen G. Simpson.
A finite combinatorial principle which is equivalent to the 1-consistency of predicative analysis.
In [52], pages 197-230, 1982.

27

Harvey Friedman, Stephen G. Simpson, and Rick L. Smith.
Countable algebra and set existence axioms.
Annals of Pure and Applied Logic, 25:141-181, 1983.

28

Harvey Friedman, Stephen G. Simpson, and Rick L. Smith.
Addendum to ``Countable algebra and set existence axioms''.
Annals of Pure and Applied Logic, 27:319-320, 1985.

29

Mariagnese Giusto.
Topology, Analysis and Reverse Mathematics.
PhD thesis, Università di Torino, 1998.
VIII + 121 pages.

30

Kurt Gödel.
Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I.
Monatshefte für Mathematik und Physik, 38:173-198, 1931.

31

Kostas Hatzikiriakou.
Commutative Algebra in Subsystems of Second Order Arithmetic.
PhD thesis, Pennsylvania State University, 1989.
VII + 43 pages.

32

David Hilbert.
Mathematical problems.
Bulletin of the American Mathematical Society, 8:437-479, 1902.

33

David Hilbert.
Über das Unendliche.
Mathematische Annalen, 95:161-190, 1926.

34

David Hilbert and Paul Bernays.
Grundlagen der Mathematik.
Grundlehren der Mathematischen Wissenschaften. Springer-Verlag, 2nd edition, 1968-1970.
Volume I, XV + 475 pages, Volume II, XIV + 561 pages.

35

Denis R. Hirschfeldt and Richard A. Shore.
Combinatorial principles weaker than Ramsey's theorem for pairs.
Journal of Symbolic Logic, 72:171-206, 2007.

36

Jeffry L. Hirst.
Combinatorics in Subsystems of Second Order Arithmetic.
PhD thesis, Pennsylvania State University, 1987.
VII + 146 pages.

37

A. James Humphreys.
On the Necessary Use of Strong Set Existence Axioms in Analysis and Functional Analysis.
PhD thesis, Pennsylvania State University, 1996.
VIII + 83 pages.

38

A. James Humphreys and Stephen G. Simpson.
Separable Banach space theory needs strong set existence axioms.
Transactions of the American Mathematical Society, 348:4231-4255, 1996.

39

A. James Humphreys and Stephen G. Simpson.
Separation and weak König's lemma.
Journal of Symbolic Logic, 64:268-278, 1999.

40

T. J. Jech, editor.
Axiomatic Set Theory, Part 2.
Number XIII in Proceedings of Symposia in Pure Mathematics. American Mathematical Society, 1974.
VI + 222 pages.

41

A. Kino, J. Myhill, and R. E. Vesley, editors.
Intuitionism and Proof Theory.
Studies in Logic and the Foundations of Mathematics. North-Holland, 1970.
VIII + 516 pages.

42

Bjørn Kjos-Hanssen.
Low-for-random reals and positive-measure domination.
Proceedings of the American Mathematical Society, 135:3703-3709, 2007.

43

Bjørn Kjos-Hanssen, Joseph S. Miller, and David Reed Solomon.
Lowness notions, measure and domination.
May 2008.
Preprint, 20 pages, in preparation, to appear.

44

Ulrich Kohlenbach.
Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization.
Journal of Symbolic Logic, 57:1239-1273, 1992.

45

Georg Kreisel.
The axiom of choice and the class of hyperarithmetic functions.
Indagationes Mathematicae, 24:307-319, 1962.

46

Georg Kreisel.
A survey of proof theory.
Journal of Symbolic Logic, 33:321-388, 1968.

47

Kenneth Kunen.
Set Theory, an Introduction to Independence Proofs.
Studies in Logic and the Foundations of Mathematics. North-Holland, 1980.
XVI + 313 pages.

48

Antonín Kucera and Sebastiaan A. Terwijn.
Lowness for the class of random sets.
Journal of Symbolic Logic, 64:1396-1402, 1999.

49

Alberto Marcone.
Foundations of BQO Theory and Subsystems of Second Order Arithmetic.
PhD thesis, Pennsylvania State University, 1993.
V + 51 pages.

50

Per Martin-Löf.
The definition of random sequences.
Information and Control, 9:602-619, 1966.

51

MedYahya Ould MedSalem and Kazuyuki Tanaka.
$\Delta^0_3$-determinacy, comprehension and induction.
Journal of Symbolic Logic, 72:452-462, 2007.

52

G. Metakides, editor.
Patras Logic Symposion.
Studies in Logic and the Foundations of Mathematics. North-Holland, 1982.
IX + 391 pages.

53

Gregory H. Moore.
Zermelo's Axiom of Choice.
Studies in the History of Mathematics and Physical Sciences. Springer-Verlag, 1982.
XIV + 410 pages.

54

Carl Mummert.
On the Reverse Mathematics of General Topology.
PhD thesis, The Pennsylvania State University, 2005.
VI + 102 pages.

55

Carl Mummert and Stephen G. Simpson.
Reverse mathematics and $\Pi^1_2$ comprehension.
Bulletin of Symbolic Logic, 11:526-533, 2005.

56

Takako Nemoto.
Determinacy of Wadge classes and subsystems of second order arithmetic.
Mathematical Logic Quarterly, 55:154-176, 2009.

57

Takako Nemoto, MedYahya Ould MedSalem, and Kazuyuki Tanaka.
Infinite games in the Cantor space and subsystems of second order arithmetic.
Mathematical Logic Quarterly, 53:226-236, 2007.

58

Charles Parsons.
On a number-theoretic choice schema and its relation to induction.
In [41], pages 459-473, 1970.

59

Klaus-Peter Podewski and Karsten Steffens.
Injective choice functions for countable families.
Journal of Combinatorial Theory, Series B, 21:40-46, 1976.

60

Marian B. Pour-El and J. Ian Richards.
Computability in Analysis and Physics.
Perspectives in Mathematical Logic. Springer-Verlag, 1988.
XI + 206 pages.

61

Michael Rathjen and Andreas Weiermann.
Proof-theoretic investigations on Kruskal's theorem.
Annals of Pure and Applied Logic, 60:49-88, 1993.

62

Kurt Schütte.
Proof Theory.
Number 225 in Grundlehren der Mathematischen Wissenschaften. Springer-Verlag, 1977.
XII + 299 pages.

63

Dana S. Scott.
Algebras of sets binumerable in complete extensions of arithmetic.
In [15], pages 117-121, 1962.

64

Naoki Shioji and Kazuyuki Tanaka.
Fixed point theory in weak second-order arithmetic.
Annals of Pure and Applied Logic, 47:167-188, 1990.

65

W. Sieg, R. Sommer, and C. Talcott, editors.
Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, volume 15 of Lecture Notes in Logic.
Association for Symbolic Logic, 2001.
VIII + 444 pages.

66

Wilfried Sieg.
Fragments of arithmetic.
Annals of Pure and Applied Logic, 28:33-71, 1985.

67

S. G. Simpson, editor.
Reverse Mathematics 2001.
Number 21 in Lecture Notes in Logic. Association for Symbolic Logic, 2005.
X + 401 pages.

68

Stephen G. Simpson.
Which set existence axioms are needed to prove the Cauchy/Peano theorem for ordinary differential equations?
Journal of Symbolic Logic, 49:783-802, 1984.

69

Stephen G. Simpson.
Ordinal numbers and the Hilbert basis theorem.
Journal of Symbolic Logic, 53:961-974, 1988.

70

Stephen G. Simpson.
Partial realizations of Hilbert's program.
Journal of Symbolic Logic, 53:349-363, 1988.

71

Stephen G. Simpson.
On the strength of König's duality theorem for countable bipartite graphs.
Journal of Symbolic Logic, 59:113-123, 1994.

72

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.

73

Stephen G. Simpson.
Predicativity: the Outer Limits.
In [65], pages 134-140, 2002.

74

Stephen G. Simpson.
Almost everywhere domination and superhighness.
Mathematical Logic Quarterly, 53:462-482, 2007.

75

Stephen G. Simpson.
Mass problems and measure-theoretic regularity.
Bulletin of Symbolic Logic, 15:385-409, 2009.

76

Stephen G. Simpson and Rick L. Smith.
Factorization of polynomials and $\Sigma^0_1$ induction.
Annals of Pure and Applied Logic, 31:289-306, 1986.

77

Rick L. Smith.
Theory of Profinite Groups with Effective Presentations.
PhD thesis, Pennsylvania State University, 1979.

78

Reed Solomon.
Ordered groups: a case study in reverse mathematics.
Bulletin of Symbolic Logic, 5:45-58, 1999.

79

John R. Steel.
Determinateness and Subsystems of Analysis.
PhD thesis, University of California at Berkeley, 1976.
VI + 107 pages.

80

William W. Tait.
Finitism.
Journal of Philosophy, 78:524-546, 1981.

81

Gaisi Takeuti.
Proof Theory.
Studies in Logic and Foundations of Mathematics. North-Holland, 2nd edition, 1987.
X + 490 pages.

82

Kazuyuki Tanaka.
The Galvin-Prikry theorem and set existence axioms.
Annals of Pure and Applied Logic, 42:81-104, 1989.

83

Kazuyuki Tanaka.
Weak axioms of determinacy and subsystems of analysis, I: $\Delta^0_2$ games.
Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 36:481-491, 1990.

84

Kazuyuki Tanaka.
Weak axioms of determinacy and subsystems of analysis, II: $\Sigma^0_2$ games.
Annals of Pure and Applied Logic, 52:181-193, 1991.

85

Kazuyuki Tanaka and Takeshi Yamazaki.
A non-standard construction of Haar measure and $\mathsf{WKL}_0$.
Journal of Symbolic Logic, 65:173-186, 2000.

86

Rüdiger Thiele.
Hilbert's twenty-fourth problem.
American Mathematical Monthly, 110:1-24, 2003.

87

Hermann Weyl.
Das Kontinuum: Kritische Untersuchungen über die Grundlagen der Analysis.
Veit, Leipzig, 1918.
IV + 84 pages. Reprinted in: H. Weyl, E. Landau, and B. Riemann, Das Kontinuum und andere Monographien, Chelsea, 1960, 1973.

88

Hermann Weyl.
The Continuum: A Critical Examination of the Foundations of Analysis.
Thomas Jefferson University Press, 1987.
Translation of [87] by S. Pollard and T. Bole. XIII + 130 pages.

89

Xiaokang Yu.
Measure Theory in Weak Subsystems of Second Order Arithmetic.
PhD thesis, Pennsylvania State University, 1987.
VII + 73 pages.

About this document ...

The Gödel Hierarchy and Reverse Mathematics

This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.71)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -split 0 gh

The translation was initiated by Stephen G Simpson on 2009-11-24

Footnotes

... Simpson¹

The author's research is supported by the Grove Endowment, the Templeton Foundation, and NSF Grants DMS-0600823 and DMS-0652637. This paper is an expanded and updated version of a talk which the author gave as part of an international symposium, Hilbert's Problems Today, which was held April 5-7, 2001 at the University of Pisa.

... logic.²

Moreover Problems 3, 4, and 5 were an outgrowth of Hilbert's interest in the foundations of geometry. I learned this from Professor Bottazzini's talk at the symposium in Pisa. One should also mention the so-called 24th Hilbert Problem discovered by R. Thiele [86] in an unpublished manuscript of Hilbert. Certainly the 24th Problem is foundationally motivated, and I will argue in a future publication that it points to Reverse Mathematics.

... mathematics.³

Another line of research which reveals a great deal of structure is Gentzen-style proof theory as carried on by many researchers including Schütte [62] and Takeuti [81].

... 1997⁴

During 1997-1999 I received much advice, help, and encouragement concerning the FOM list from Harvey Friedman.

... majority⁵

Of course we must make exceptions for extremely abstract branches of mathematics such as set-theoretical topology and the arithmetic of uncountable cardinal numbers.

... students.⁶

Among the Ph.D. theses supervised by Simpson on subsystems of $\mathsf{Z}_2$ and Reverse Mathematics are Steel 1976 [79], Smith 1979 [77], Brackin 1984 [6], Brown 1987 [7], Hirst 1987 [36], Yu 1987 [89], Ferreira 1988 [22], Hatzikiriakou 1989 [31], Marcone 1993 [49], Humphreys 1996 [37], Giusto 1998 [29], and Mummert 2005 [54]. Some key papers in Reverse Mathematics are Simpson [68,71], Friedman/Simpson/Smith [27,28], Friedman/McAloon/Simpson [26], Brown/Simpson [9,10], Brown/Giusto/Simpson [8], Humphreys/Simpson [38,39], Mummert/Simpson [55], Shioji/Tanaka [64], Solomon [78], Tanaka [82,83,84], and Tanaka/Yamazaki [85]. The basic reference for subsystems of $\mathsf{Z}_2$ and Reverse Mathematics is Simpson [72].

....⁷

These particular subsystems of $\mathsf{Z}_2$ and many others were first introduced by Friedman [25]. The subscript $0$ denotes restricted induction, i.e., the systems in question assume induction only for a restricted class of formulas. For $\mathsf{RCA}_0$ and $\mathsf{WKL}_0$ this class consists of the $\Sigma^0_1$ formulas, while for stronger systems it consists of the quantifier-free formulas. The advantages of systems with restricted induction over the corresponding systems with full induction are: (a) the former are finitely axiomatizable while the latter are not, (b) the former are below the latter in the Gödel Hierarchy, (c) results in Reverse Mathematics for the former subsume corresponding results for the latter.

... natural''⁸

Later in this paper we shall propose a rigorous criterion of ``mathematical naturalness'' for subsystems of $\mathsf{Z}_2$.

... theory.⁹

We regard this as a sufficient (and possibly also necessary) condition for a subsystem of $\mathsf{Z}_2$ to be considered mathematically natural.

...sosoa)¹⁰

See also Sieg [66] and Kohlenbach [44].

... conservative¹¹

Note however that not all proofs of conservativity are of equal value. It is arguable that Hilbert's Program of finitistic reductionism requires conservativity proofs which are themselves finitistic. See for instance the careful discussion by Burgess [12] in this volume.

... comprehension,¹²

By $\Pi^1_2$ comprehension we mean $\Pi^1_2$-$\mathsf{CA}_0$, i.e., $\mathsf{Z}_2$ with the comprehension scheme restricted to formulas $\Phi(n)$ with exactly two set quantifiers.

...filter¹³

Note that this is just the usual notion of filter which figures prominently in forcing over models of axiomatic set theory. See for instance Kunen [47].

... separable¹⁴

A metric space is said to be separable if it has a countable dense subset. Most of the topological spaces occurring in core mathematics arise from complete separable metric spaces.