The Gödel Hierarchy and Reverse Mathematics
Stephen G. Simpson^{1}
Department of Mathematics
First draft: March 21, 2008
This draft: November 24, 2009
Pennsylvania State University
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.^{2}
 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 be any theory in the
predicate calculus satisfying certain wellknown mild conditions.
Then we have the following results:
 is incomplete (First Incompleteness Theorem, Gödel 1931).
 The statement `` is consistent'' is not a theorem of
(Second Incompleteness Theorem, Gödel 1931).
 The problem of deciding whether a given formula is a theorem of
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.^{3} 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.
Using the Second Incompleteness Theorem as our jumpingoff point, we
define an ordering of theories as follows. Let and be two
theories as above. We write
to mean that the statement `` is consistent'' is a theorem of
. One sometimes says that the consistency strength of
is less than that of . Often this goes handinhand with
saying that is interpretable in and not vice versa. We
may think of as meaning that is ``more abstract'' or
``harder to interpret'' or ``less concrete'' or ``less meaningful'' or
``less surely consistent'' than .
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 ,
, and
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 nonartificial 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 jumpingoff point
here is the First Incompleteness Theorem. Assuming that the language
of is part of the language of , let us write
to mean that the sentences which are theorems of form a proper
subset of the sentences in the language of which are theorems of
. We may think of
as meaning that is
``more powerful'' or ``stronger'' than . In many cases the
ordering and the ordering coincide. In Table 1
the lower theories are always below the higher theories with respect
to the 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
and
have been explored by Simpson [72, Remark I.11.7, Chapter
VIII].
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^{4} and ran it during the years 19972002 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?
Secondorder arithmetic, denoted , is a theory with two sorts
of variables. There are number variables intended
to range over the set of natural numbers
and
set variables intended to range over subsets of
. In addition the language of includes the predicates
and intended to denote addition and multiplication on
, as well as the membership predicate intended to denote
the membership relation
on
. Here is the powerset of , i.e.,
the set of all subsets of . In addition has the usual
apparatus of the predicate calculus including propositional
connectives
, number quantifiers
, and set quantifiers
.
The axioms of express basic properties of and .
Among the axioms are all instances of the full comprehension
scheme consisting of the universal closures of all formulas of the
form
where is any formula in which the set variable 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^{5} of rigorous core mathematics within . 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 , and in virtually all
cases these sentences are then provable as theorems of .
Later Kreisel [45] emphasized the importance of
subsystems of . By a subsystem of we mean any
theory in the language of which is
. For
example, if we restrict the comprehension scheme of to
formulas with a fixed finite number of set quantifiers, the
resulting theory is both and
. Thus we have
infinitely many different subsystems of . It can be shown that
itself is not finitely axiomatizable, but trivially each
theorem of is provable in some finitely axiomatizable
subsystem of obtained by discarding all but finitely many of
the axioms of . 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 in which they are provable. Thus subsystems of
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 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.^{6} Some interesting
subsystems of appear in Table 1:
,
,
,
, , .^{7} As an outcome of ongoing research, it is
now fair to say that subsystems of 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.
Given a mathematical theorem , let be the ``weakest
natural''^{8} subsystem of in which is provable. The
following widespread phenomena have been observed:
 Often it is possible to determine exactly. In other
words,
and there is no ``natural''
such that .
 In such cases it often turns out that and are
logically equivalent over a much weaker subsystem . In other
words,
for some
. (In
particular is finitely axiomatizable over .)
 Only a relatively small number of subsystems of tend to
arise repeatedly as 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 wellknown 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
over the much weaker system
. Thus we have
where is the Perfect Set
Theorem as formalized in the language of .
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
over
.
As a third example, define a countable bipartite graph to be a
set
. A matching is a set such that if and only if for all and
. A covering is a set
such that
for all at least one of belongs to . A
König covering consists of a matching and a covering
such that for all exactly one of belongs to .
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
over
.
Combining these three examples, we obtain the oddlooking result that
the Perfect Set Theorem, Lusin's Theorem, and the Podewski/Steffens
Theorem are pairwise logically equivalent (over
). Thus these
three theorems coming from completely different branches of
mathematics have been classified into precisely the same equivalence
class (modulo logical equivalence over
) 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 uptodate reference on Reverse Mathematics is
the 2005 volume [67] which includes papers by a number of
prominent researchers.
Table 2:
Mathematics in the Big Five.





 
analysis (separable): 





differential equations 





continuous functions 





completeness, etc. 





Banach spaces 





open and closed sets 





Borel and analytic sets 





algebra (countable): 





countable fields 





commutative rings 





vector spaces 





Abelian groups 





miscellaneous: 





mathematical logic 





countable ordinals 





infinite matchings 





the Ramsey property 





infinite games 






The five most important subsystems of for Reverse Mathematics
are:

(Recursive Comprehension Axiom). This is a kind of
formalized recursive or computable mathematics. The models
of
are precisely the nonempty subsets of which are
closed under Turing reducibility. The smallest model of
is
is recursive.

(Weak König's Lemma). This consists of
plus a
compactness principle: every infinite subtree of the full binary
tree has an infinite path. The models of
are
precisely the Scott systems [63].
is not an model of
, but it is the
intersection of all such models.

(Arithmetical Comprehension Axiom). This consists of
plus the comprehension scheme restricted to formulas
with no set quantifiers. The models of
are the nonempty subsets of which are closed under Turing
reducibility and the Turing jump operator. The smallest
model of
is
where is the th Turing jump of
.

(Arithmetical Transfinite Recursion). This consists of
plus an axiom saying that the Turing jump operator, or
equivalently arithmetical comprehension, can be iterated along any
countable wellordering. Each model of
is closed
under relative hyperarithmeticity. The model
is hyperarithmetical is not itself an model of
, but it is the intersection of all such models. In fact,
is the intersection of all models of
(Simpson [72, VII.2.7 and VIII.6.11]).
  ( Comprehension Axiom). This consists
of
plus the comprehension scheme restricted to formulas
with exactly one set quantifier. The smallest
model of  is
where is the th hyperjump of .
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 . Each
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
, and the most useful benchmark systems have been
,
,
and . We shall now list some of
these results. References for these results may be found in
[72].
is equivalent over
to each of the following
mathematical theorems:
 The Heine/Borel Covering Lemma: Every covering of by a
sequence of open intervals has a finite subcovering.
 Every covering of a compact metric space by a sequence of open
sets has a finite subcovering.
 Every continuous realvalued function on (or on any
compact metric space) is bounded (uniformly continuous, Riemann
integrable).
 The Maximum Principle: Every continuous realvalued function on
(or on any compact metric space) has (or attains) a
supremum.
 The local existence theorem for solutions of (finite systems of)
ordinary differential equations.
 Gödel's Completeness Theorem: every consistent finite (or
countable) set of sentences in the predicate calculus has a
countable model.
 Gödel's Compactness Theorem: a countable set of sentences in
the predicate calculus is satisfiable if and only if it is finitely
satisfiable.
 Every countable commutative ring has a prime ideal.
 Every countable field (of characteristic ) has a unique
algebraic closure.
 Every countable formally real field is orderable.
 Every countable formally real field has a (unique) real closure.
 Brouwer's Fixed Point Theorem: Every (uniformly) continuous
function
has a fixed point.
 The Separable Hahn/Banach Theorem: If is a bounded linear
functional on a subspace of a separable Banach space, and if
, then has an extension to the whole
space such that
.
 Banach's Theorem: In a separable Banach space, given two
disjoint convex open sets and , there exists a closed
hyperplane such that is on one side of and is on the
other.
 The existence and uniqueness of Haar measure on separable,
locally compact groups.
 Every countable regular bipartite graph has a perfect
matching.
is equivalent over
to each of the following
mathematical theorems:
 Every bounded, or bounded increasing, sequence of real numbers
has a least upper bound.
 The Bolzano/Weierstraß Theorem: Every bounded sequence of
real numbers, or of points in , has a convergent subsequence.
 Every sequence of points in a compact metric space has a
convergent subsequence.
 The Ascoli Lemma: Every bounded equicontinuous sequence of
realvalued continuous functions on a bounded interval has a
uniformly convergent subsequence.
 Every countable commutative ring has a maximal ideal.
 Every countable vector space (over ) has a basis.
 Every countable field (of characteristic ) has a
transcendence basis.
 Every countable Abelian group has a unique divisible closure.
 König's Lemma: Every infinite, finitely branching tree has an
infinite path.
 Ramsey's Theorem for colorings of
(or of
for
any fixed ).
is equivalent over
to each of the following
mathematical theorems:
 Any two countable wellorderings are comparable.
 Ulm's Theorem: Any two countable reduced Abelian groups
which have the same Ulm invariants are isomorphic.
 The Perfect Set Theorem: Every uncountable closed, or analytic,
set has a perfect subset.
 Lusin's Separation Theorem: Any two disjoint analytic sets can
be separated by a Borel set.
 The domain of any singlevalued Borel set in the plane is a
Borel set.
 Every clopen (or open) game in
is determined.
 Every clopen (or open) subset of
has the Ramsey
property.
 Every countable bipartite graph admits a König covering.
 is equivalent over
to each of the following
mathematical theorems:
 Every tree has a largest perfect subtree.
 The Cantor/Bendixson Theorem: Every closed subset of (or
of any complete separable metric space) is the union of a countable
set and a perfect set.
 Every countable Abelian group is the direct sum of a divisible
group and a reduced group.
 Every difference of two open sets in the Baire space
is determined.
 Every
set in
has the Ramsey
property.
 Silver's Theorem: For every Borel (or coanalytic, or
) equivalence relation with uncountably many
equivalence classes, there exists a perfect set of inequivalent
elements.
 For every countable set in the dual of a separable
Banach space (or in ), there exists a smallest
weakclosed subspace of (or of respectively)
containing .
 For every normclosed subspace of , the
weakclosure of exists.
Reverse Mathematics and the Big Five have a number of implications for
the foundations of mathematics. We briefly mention some of these
implications.
In Reverse Mathematics, specific mathematical theorems are classified
according to the subsystems of 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.
As a byproduct of Reverse Mathematics, certain specific subsystems of
are identified as being mathematically natural, and the
naturalness is rigorously demonstrated.
Namely, a subsystem of is to be considered mathematically
natural if we can find one or more core mathematical theorems
such that
is provable over a weak base
theory.^{9} In particular, there is abundant evidence
(some of which has been presented above) that
,
,
, and  are mathematically natural in this
sense.
With the help of Reverse Mathematics, we can explore the consequences
of particular f.o.m. doctrines and programs, including:
 computable analysis (see Aberth [1],
PourEl/Richards [60]).
 finitistic reductionism (see Hilbert [33]).
 predicativity (see Weyl [87,88], Kreisel
[45], Feferman
[17,18,21]).
 predicative reductionism (see Feferman
[19], Simpson
[73], and Friedman/McAloon/Simpson
[26]).
 impredicative or 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 . Thus
certain subsystems of 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 .
We now discuss two examples: the Cinq Lettres Program
[3] and Hilbert's Program
[33].
Table 3:
Foundational programs and the Big Five.

computable mathematics 
PourEl/Richards 

finitistic reductionism 
Hilbert 

predicativity 
Weyl, Feferman 

predicative reductionism 
Feferman, Friedman,
Simpson 
 
impredicativity 
Buchholz et al. 

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 wellbehaved 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
. Moreover, it is known prooftheoretically (see
Friedman/McAloon/Simpson [26]) that
is
conservative over Feferman's systems of predicative
mathematics [17,18]. Thus all 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.
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:
 Tait [80] has argued that (Primitive Recursive
Arithmetic) embodies all of finitistic mathematics.
 Parsons [58] and Friedman (unpublished,
but see [72, Section IX.3])^{10} have shown
that
is conservative^{11} over for sentences. Moreover,
Tait's argument shows that this class of sentences includes all
finitistically meaningful sentences.
 A large portion of core mathematics, including many of the best
known nonconstructive theorems, can be carried out in
. A
sampling of these results is included in the above discussion of
Reverse Mathematics in
. See also Simpson [72, Chapter
IV].
 In addition to
there are other subsystems of
which are likewise conservative over 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].
In addition to the Big Five, a number of other subsystems of
have arisen in Reverse Mathematics.
The most striking recent discovery is the existence of Reverse
Mathematics at the level of comprehension,^{12} 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 be a partially ordered set. A
filter^{13} on is a set
such that (a) imply , and (b)
imply
. A
maximal filter on is a filter on which is not properly
included in any other filter on . Let be the topological
space whose points are the maximal filters on and whose basic open
sets are of the form
where . It
can be shown that all complete metric spaces and many nonmetrizable
topological spaces are homeomorphic to spaces of the form
where is a partially ordered set. Moreover, every complete
separable^{14} metric space is homeomorphic to for some countable
partially ordered set .
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 wellknown and easy to see that every metrizable
topological space is regular. Let be the following
metrization theorem:
Given a countable partially ordered set , the topological space
is completely metrizable if and only if it is regular.
It can be shown (see [55]) that is an easy
consequence of wellknown metrization theorems due to Urysohn and
Choquet. It is straightforward to formalize as a sentence in
the language of .
Mummert/Simpson [55] have shown that is equivalent to
 over . Thus we have a convincing
instance of Reverse Mathematics at the level of
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.
 Simpson/Smith [76] (see also [72, Section
X.4]) introduced a system
which is
and
. They showed that
induction
and that
can replace
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
over
.
 Yu [89] introduced a system
which arises
repeatedly in the Reverse Mathematics of measure theory. For
example,
is equivalent over
to a formal statement
of the Vitali Covering Theorem [8]. It turns out that
is strictly intermediate between
and
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].
 Cholak/Jockusch/Slaman [14] and Hirschfeldt/Shore
[35] have studied a number of Reverse Mathematics questions
centering around
Ramsey's Theorem for exponent 2.
A problem which remains open is to determine exactly the consistency
strength of
. It is also open whether
. It is known that not all
models of
satisfy
.
 Beginning with Dobrinen/Simpson [16] there has been an
explosion of activity in the Reverse Mathematics of
measuretheoretic regularity. This turns out to be closely related
to the study of lowforrandomness in the sense of
Kucera/Terwijn [48]. In addition to [16] see
also Binns et al. [4], Cholak/Greenberg/Miller
[13], KjosHanssen [42], Simpson
[74,75], and KjosHanssen/Miller/Solomon
[43].
 Simpson [69] has performed an axiomatic study of
socalled basis theorems for ideals in commutative and
noncommutative rings, leading to Reverse Mathematics at the levels
is wellordered
and
is wellordered
in the Gödel Hierarchy. It is known that these theories are
strictly intermediate between
and
with respect to
the and orderings, and incomparable with
with
respect to the ordering.
 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
is wellordered
where
is the Ackermann ordinal, a.k.a., the
small Veblen ordinal. It is known that this theory is strictly
intermediate between
and  with respect to
the ordering and incomparable with
and
with
respect to the ordering.
 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 which arise in this
way are strictly intermediate between  and
.
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.
 1

Oliver Aberth.
Computable Analysis.
McGrawHill, 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:257290, 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:261273, 1905.
Reprinted in [5, pp. 150160]. English translation in
[53, pp. 311320].
 4

Stephen Binns, Bjørn KjosHanssen, Manuel Lerman, and David Reed Solomon.
On a question of Dobrinen and Simpson concerning almost
everywhere domination.
Journal of Symbolic Logic, 71:119136, 2006.
 5

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

Stephen H. Brackin.
On Ramseytype 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:191206, 2002.
 9

Douglas K. Brown and Stephen G. Simpson.
Which set existence axioms are needed to prove the separable
HahnBanach theorem?
Annals of Pure and Applied Logic, 31:123144, 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:557578, 1993.
 11

Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg.
Iterated Inductive Definitions and Subsystems of
Analysis: Recent ProofTheoretical Studies.
Number 897 in Lecture Notes in Mathematics. SpringerVerlag,
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:10571072, 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:155, 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:914922, 2004.
 17

Solomon Feferman.
Systems of predicative analysis, I.
Journal of Symbolic Logic, 29:130, 1964.
 18

Solomon Feferman.
Systems of predicative analysis, II.
Journal of Symbolic Logic, 33:193220, 1968.
 19

Solomon Feferman.
Predicatively reducible systems of set theory.
In [40], pages 1132, 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 249283, 1998.
 22

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

Harvey Friedman.
Bar induction and .
Journal of Symbolic Logic, 34:353362, 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 235242. Canadian
Mathematical Congress, 1975.
 25

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

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

Harvey Friedman, Stephen G. Simpson, and Rick L. Smith.
Countable algebra and set existence axioms.
Annals of Pure and Applied Logic, 25:141181, 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:319320, 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:173198,
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:437479,
1902.
 33

David Hilbert.
Über das Unendliche.
Mathematische Annalen, 95:161190, 1926.
 34

David Hilbert and Paul Bernays.
Grundlagen der Mathematik.
Grundlehren der Mathematischen Wissenschaften. SpringerVerlag,
2nd edition, 19681970.
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:171206, 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:42314255, 1996.
 39

A. James Humphreys and Stephen G. Simpson.
Separation and weak König's lemma.
Journal of Symbolic Logic, 64:268278, 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.
NorthHolland, 1970.
VIII + 516 pages.
 42

Bjørn KjosHanssen.
Lowforrandom reals and positivemeasure domination.
Proceedings of the American Mathematical Society,
135:37033709, 2007.
 43

Bjørn KjosHanssen, 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:12391273, 1992.
 45

Georg Kreisel.
The axiom of choice and the class of hyperarithmetic functions.
Indagationes Mathematicae, 24:307319, 1962.
 46

Georg Kreisel.
A survey of proof theory.
Journal of Symbolic Logic, 33:321388, 1968.
 47

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

Antonín Kucera and Sebastiaan A. Terwijn.
Lowness for the class of random sets.
Journal of Symbolic Logic, 64:13961402, 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 MartinLöf.
The definition of random sequences.
Information and Control, 9:602619, 1966.
 51

MedYahya Ould MedSalem and Kazuyuki Tanaka.
determinacy, comprehension and induction.
Journal of Symbolic Logic, 72:452462, 2007.
 52

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

Gregory H. Moore.
Zermelo's Axiom of Choice.
Studies in the History of Mathematics and Physical Sciences.
SpringerVerlag, 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 comprehension.
Bulletin of Symbolic Logic, 11:526533, 2005.
 56

Takako Nemoto.
Determinacy of Wadge classes and subsystems of second order
arithmetic.
Mathematical Logic Quarterly, 55:154176, 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:226236, 2007.
 58

Charles Parsons.
On a numbertheoretic choice schema and its relation to induction.
In [41], pages 459473, 1970.
 59

KlausPeter Podewski and Karsten Steffens.
Injective choice functions for countable families.
Journal of Combinatorial Theory, Series B, 21:4046, 1976.
 60

Marian B. PourEl and J. Ian Richards.
Computability in Analysis and Physics.
Perspectives in Mathematical Logic. SpringerVerlag, 1988.
XI + 206 pages.
 61

Michael Rathjen and Andreas Weiermann.
Prooftheoretic investigations on Kruskal's theorem.
Annals of Pure and Applied Logic, 60:4988, 1993.
 62

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

Dana S. Scott.
Algebras of sets binumerable in complete extensions of arithmetic.
In [15], pages 117121, 1962.
 64

Naoki Shioji and Kazuyuki Tanaka.
Fixed point theory in weak secondorder arithmetic.
Annals of Pure and Applied Logic, 47:167188, 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:3371, 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:783802, 1984.
 69

Stephen G. Simpson.
Ordinal numbers and the Hilbert basis theorem.
Journal of Symbolic Logic, 53:961974, 1988.
 70

Stephen G. Simpson.
Partial realizations of Hilbert's program.
Journal of Symbolic Logic, 53:349363, 1988.
 71

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

Stephen G. Simpson.
Subsystems of Second Order Arithmetic.
Perspectives in Mathematical Logic. SpringerVerlag, 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 134140, 2002.
 74

Stephen G. Simpson.
Almost everywhere domination and superhighness.
Mathematical Logic Quarterly, 53:462482, 2007.
 75

Stephen G. Simpson.
Mass problems and measuretheoretic regularity.
Bulletin of Symbolic Logic, 15:385409, 2009.
 76

Stephen G. Simpson and Rick L. Smith.
Factorization of polynomials and induction.
Annals of Pure and Applied Logic, 31:289306, 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:4558, 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:524546, 1981.
 81

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

Kazuyuki Tanaka.
The GalvinPrikry theorem and set existence axioms.
Annals of Pure and Applied Logic, 42:81104, 1989.
 83

Kazuyuki Tanaka.
Weak axioms of determinacy and subsystems of analysis, I:
games.
Zeitschrift für Mathematische Logik und Grundlagen der
Mathematik, 36:481491, 1990.
 84

Kazuyuki Tanaka.
Weak axioms of determinacy and subsystems of analysis, II:
games.
Annals of Pure and Applied Logic, 52:181193, 1991.
 85

Kazuyuki Tanaka and Takeshi Yamazaki.
A nonstandard construction of Haar measure and
.
Journal of Symbolic Logic, 65:173186, 2000.
 86

Rüdiger Thiele.
Hilbert's twentyfourth problem.
American Mathematical Monthly, 110:124, 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.
The Gödel Hierarchy and Reverse Mathematics
This document was generated using the
LaTeX2HTML translator Version 200221 (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 20091124
Footnotes
 ... Simpson^{1}
 The author's research is supported
by the Grove Endowment, the Templeton Foundation, and NSF Grants
DMS0600823 and DMS0652637. 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 57, 2001 at the University of Pisa.
 ...
logic.^{2}
 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 socalled 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.^{3}
 Another line of research which reveals a
great deal of structure is Gentzenstyle proof theory as carried on
by many researchers including Schütte [62] and Takeuti
[81].
 ... 1997^{4}
 During 19971999 I received
much advice, help, and encouragement concerning the FOM list from
Harvey Friedman.
 ... majority^{5}
 Of course we must make exceptions
for extremely abstract branches of mathematics such as
settheoretical topology and the arithmetic of uncountable cardinal
numbers.
 ...
students.^{6}
 Among the Ph.D. theses supervised by Simpson on
subsystems of 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
and Reverse Mathematics is Simpson [72].
 ....^{7}
 These
particular subsystems of and many others were first
introduced by Friedman [25]. The subscript
denotes restricted induction, i.e., the systems in question
assume induction only for a restricted class of formulas. For
and
this class consists of the
formulas, while for stronger systems it consists of the
quantifierfree 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''^{8}
 Later in this paper we shall propose a rigorous
criterion of ``mathematical naturalness'' for subsystems of
.
 ...
theory.^{9}
 We regard this as a sufficient (and possibly also
necessary) condition for a subsystem of to be considered
mathematically natural.
 ...sosoa)^{10}
 See also Sieg
[66] and Kohlenbach [44].
 ... conservative^{11}
 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,^{12}
 By
comprehension we mean , i.e., with
the comprehension scheme restricted to formulas with
exactly two set quantifiers.
 ...filter^{13}
 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^{14}
 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.
Stephen G Simpson
20091124