**Jeffrey Ketland,**

During the nineteenth century, and up until around 1939, many major
mathematicians were deeply interested in, and actively contributed to, the
*foundations of mathematics*.^{1}
Indeed, the period saw the development of several important new
branches of mathematics (set theory, model theory, computability theory and
proof theory). But since then interest by working ``core'' mathematicians in
such foundational (and philosophical) questions has declined. However,
foundations has been partially resuscitated since the early 1970s by the
pioneering work of Harvey Friedman, whose distinctive foundational program
is known as ``reverse mathematics'' (henceforth, **RM**). Stephen G.
Simpson's new book *Subsystems of Second-Order Arithmetic* is the
first monograph on **RM**. Why, you ask, concentrate on *
second-order arithmetic*? The reason is that very much *ordinary* (or ``
*core*'') mathematical knowledge can be *formalized* within
second-order arithmetic (or some subsystem). Simpson writes in the preface:

Almost all of the problems studied in this book are motivated by an overriding foundational question: what are the appropriate axioms for mathematics? We undertake a series of case studies to discover which are the appropriate axioms for proving particular theorems in core mathematical areas such as algebra, analysis and topology. We focus on the language of second order arithmetic, because that language is the weakest one that is rich enough to express and develop the bulk of core mathematics. (pp. vii-viii).

After Chapter I (Introduction), the book is broken into Parts A and B, and
an Appendix. Chapter I describes *axiomatic second-order arithmetic* (
**Z**_{2}), five important *subsystems*, and explains the main
ideas behind **RM**. Chapter II contains a detailed discussion of the
``base theory'' **RCA**_{0} and Chapters III-VI of Part A develop
**RM** for the four remaining subsystems. Chapters VII-IX of Part B
discusses the model theory for the subsystems of **Z**_{2}. The
Appendix contains some additional results.

Simpson treats second-order arithmetic as a *first-order* axiomatic
theory **Z**_{2}, formulated in a (two-sorted) *first-order*
language **L**_{2} (an extension of the usual first-order language of
arithmetic, obtained by adding atomic formulas of the form ,
where
*n* is a number variable and *X* is a set variable). The axioms of **Z**
_{2} are the usual first-order axioms of Peano Arithmetic plus,

(i)Induction Axiom:

(ii)

Full 2nd Order Comprehension Scheme:,

where is any formula of

L_{2}in whichXdoes not occur freely.

The strong deductive power of **Z**_{2} derives from the full
comprehension scheme (ii), whose instances are *set-existence axioms*:
the scheme (ii) asserts the existence of a *set* *X* of numbers *n*such that
holds. Note that the induction axiom (i) is distinct
from (and sometimes weaker than) the *full second-order induction scheme
*,
.
However, this scheme is in fact
provable in full **Z**_{2}.

The five main subsystems of **Z**_{2} studied are, in increasing
logical strength, **RCA**_{0} (*recursive comprehension axiom*),
**WKL**_{0} (*Weak König's Lemma*), **ACA**_{0} (
*arithmetical comprehension axiom*), **ATR**_{0} (*
arithmetic transfinite recursion*) and
-**CA**_{0} (
*comprehension axiom*). Each of the three subsystems
**RCA**_{0}, **ACA**_{0} and
-**CA**_{0}of **Z**_{2} is defined by a specification of a restricted class of
formulas which can go into either the comprehension or induction schemes
(roughly, either
formulas or
formulas or a
combination. I lack the space to go into details). **WKL**_{0} is
**RCA**_{0} plus the axiom ``every infinite tree of binary sequences
has an infinite path'' (i.e., a version of König's Lemma, the theorem we
use in proving Gödel's completeness theorem for first-order logic) and
**ATR**_{0} is **ACA**_{0} plus an axiom scheme which permits
transfinite recursion on well-ordered sequences. (It turns out that these
systems **WKL**_{0} and **ATR**_{0} are equivalent (over
**RCA**_{0}) to
separation and
separation, respectively: see p. 40).

In general, it is possible (via devious coding mechanisms) to *express*
many basic theorems of core mathematics (analysis, algebra, topology) within
the language of second-order arithmetic. Chapter II of Simpson's book
contains the development of many theorems of core mathematics within **
RCA**_{0}. As Simpson explains, ``**RCA**_{0} ... is seen to embody
a kind of formalized computable or constructive mathematics'' (p. 41).
Further, Simpson notes that each of the chosen subsystems corresponds
(perhaps loosely) with some important foundational position. The following
is based on Simpson's table on p. 42:

SystemMotivationAssociated withRCA_{0}Constructivism Bishop WKL_{0}Finitistic reductionism Hilbert ACA_{0}Predicativism Weyl, Feferman ATR_{0}Predicative reductionism Friedman, Simpson - CA_{0}Impredicativity Feferman, et al.

On a standard account, mathematics involves proving theorems from axioms (be
they ``self-evidently true'', ``grounded in intuition'', merely
``stipulative'', or whatever). **RM** involves deducing *axioms*
from *theorems*. The methodology (and some of the main results) of
**RM** is introduced in Chapter I, and involves three main ingredients:
(1) A *base theory* **B** (some subsystem of **Z**_{2}),
(2) a sequence
**S**_{1},**S**_{2},..., of *set-existence
axioms* of increasing strength, and (3) some (core mathematical) *
theorem* .
A ``reversal'' is then to establish a metatheorem of
the form:
.
Results
of this form establish not only that the theorem
can be proved in
the system
,
but also that the *axiom*
(or each instance of the axiom scheme)
**S**_{i} can be deduced from
the *theorem*
(modulo **B**, of course). It then
follows that (modulo **B**) the axiom
**S**_{i} is the *
weakest* such from which the theorem
can be proved. Throughout
the bulk of Simpson's book, the base theory chosen is **RCA**_{0}.
Chapter III develops in detail the main known reversals for **ACA**_{0}. Consider the Bolzano/Weierstrass Theorem, **BW **: ``Every bounded
sequence of real numbers, or of points in
,
has a convergent
subsequence''. Theorem III.2.2 (pp. 106-7) shows that **BW** is
equivalent to **ACA**_{0} over **RCA**_{0}. That is, **
RCA**
.
Simpson
remarks:

The point here is that the Bolzano/Weierstrass theorem (an ordinary mathematical statement) implies arithmetical comprehension (a set existence axiom). Thus no set existence axiom weaker than arithmetical comprehension will suffice to prove the Bolzano/Weierstrass theorem. (p. 107).

The remaining Chapters IV-VI of Part A develop similar detailed reverse
mathematics results for the other three main subsystems of **Z**_{2}.
In general, by demonstrating that certain set-existence axioms are required
to develop a part of core mathematics, one establishes rather precise limits
on the reconstructive powers of the various reductive philosophical
programmes mentioned in the table above.

The techniques of Chapter IX (``Non--Models'') are model-theoretic,
but are mainly geared up to proving conservation theorems. A theory
in
is a *conservative extension* of
another theory
**T** in
**L** just in case
,
and
any **L**-theorem
of the extended theory
is *already* a theorem of
**T**. Chapter IX contains several
conservativeness results for subsystems of **Z**_{2}. For example,
(a) **ACA**_{0} is conservative over **PA** for **L**_{1}sentences; (b) **RCA**_{0} is conservative over
**-PA** (**PA** with restricted induction), (c) **WKL**_{0}is conservative over **RCA**_{0} for
sentences; (d)
**WKL**_{0} is conservative over **PRA** for
sentences (**PRA** is *primitive recursive arithmetic*). As
mentioned, the proofs of these results use *model-theoretic*
techniques. In another review of Simpson's book, John Burgess asked the
important question whether these model-theoretic proofs of conservativeness
could be converted to *proof-theoretic* (or ``syntactic'', or
``finitistic'') proofs. Harvey Friedman has replied (on the moderated
internet discussion list FOM: see below) that, in fact, all of them can be
given proof-theoretic proofs. The *philosophical significance* of such
conservativeness results is related to various forms of *reductionism*.
Simpson discusses these topics in Chapter IX (Sections 3 and 4), where he
argues that such results yield ``partial realizations of Hilbert's
program''. Simpson introduces finitism as ``that part of mathematics which
rejects completed infinite totalities and [which] is indispensable for all
scientific reasoning. ... [I]t is generally agreed that **PRA**
captures this notion.'' (p. 381). Simpson explains that Gödel's
incompleteness theorems block a wholesale realization of Hilbert's programme
and comments that ``it is of interest to ask what part of Hilbert's program
can be carried out. .... Which interesting subsystems of **Z**_{2}are conservative over **PRA** for
sentences? ...'' (p.
382). He concludes:

Theorem IX.3.16 shows thatWKL_{0}is conservative overPRAfor sentences (in fact sentences). This conservation result, together with the results of Chapter II and IV concerning the development of mathematics withinWKL_{0}implies that a significant part of mathematics is finistically reducible, in the precise sense envisioned by Hilbert. (p. 382).

These results are certainly interesting. But it might well be argued that,
*despite* such partial successes for reductionism, Gödel's
incompleteness results themselves in general point in the opposite
direction: towards *non-finitism* and *irreducibility* (i.e., the
indispensability of abstract set existence axioms). In fact, it is possible
to speculate that research in **RM** might tie in (somehow) with some
recent debates in the philosophical literature about the indispensability of
mathematics for *empirical science* (especially theoretical physics).
If certain parts of substantial mathematics are indispensable for science,
then (as Quine was perhaps the first to point out) we thereby obtain a
``holistic'' (Putnam says ``quasi-empirical'') scientific justification for
abstract mathematics (even for mathematical realism).

This review cannot do full justice to the comprehensive *tour de force*
treatment of **RM** in Simpson's book. It is clear that **RM**
contains results of significance for numerous topics in the foundations and
philosophy of mathematics. Gödel speculated that we might require higher
and higher levels of *abstraction* (in particular, abstract set
existence axioms) in order to generate proofs of (and understanding of)
certain truths of arithmetic which remain unprovable in weaker axiom
systems. What **RM** achieves is, in a sense, an elaboration of the
*fine structure* of such Gödelian phenomena. There is no question
that the **RM** program initiated by Friedman, and further developed by
Simpson and others, significantly profits our understanding of philosophical
and foundational problems concerning mathematics. Anyone interested in the
foundations of (and philosophy of) mathematics needs to know about this
work. Simpson's book, despite its highly technical nature, is an excellent
and comprehensive introduction to this developing field.

[Stephen G. Simpson runs a moderated discussion group called ``Foundations of Mathematics''. The web page is at: www.personal.psu.edu/t20/fom].