Review: Stephen G. Simpson (1999) Subsystems of Second-Order Arithmetic (Springer)

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 ( Z2), five important subsystems, and explains the main ideas behind RM. Chapter II contains a detailed discussion of the base theory'' RCA0 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 Z2. The Appendix contains some additional results.

Simpson treats second-order arithmetic as a first-order axiomatic theory Z2, formulated in a (two-sorted) first-order language L2 (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 L2 in which X does not occur freely.

The strong deductive power of Z2 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 nsuch 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 Z2.

The five main subsystems of Z2 studied are, in increasing logical strength, RCA0 (recursive comprehension axiom), WKL0 (Weak König's Lemma), ACA0 ( arithmetical comprehension axiom), ATR0 ( arithmetic transfinite recursion) and -CA0 ( comprehension axiom). Each of the three subsystems RCA0, ACA0 and -CA0of Z2 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). WKL0 is RCA0 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 ATR0 is ACA0 plus an axiom scheme which permits transfinite recursion on well-ordered sequences. (It turns out that these systems WKL0 and ATR0 are equivalent (over RCA0) 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 RCA0. As Simpson explains, RCA0 ... 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:

System Motivation Associated with
RCA0 Constructivism Bishop
WKL0 Finitistic reductionism Hilbert
ACA0 Predicativism Weyl, Feferman
ATR0 Predicative reductionism Friedman, Simpson
-CA0 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 Z2), (2) a sequence S1,S2,..., 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) Si can be deduced from the theorem (modulo B, of course). It then follows that (modulo B) the axiom Si is the weakest such from which the theorem can be proved. Throughout the bulk of Simpson's book, the base theory chosen is RCA0. Chapter III develops in detail the main known reversals for ACA0. 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 ACA0 over RCA0. 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 Z2. 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 Z2. For example, (a) ACA0 is conservative over PA for L1sentences; (b) RCA0 is conservative over -PA (PA with restricted induction), (c) WKL0is conservative over RCA0 for sentences; (d) WKL0 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 Z2are conservative over PRA for sentences? ...'' (p. 382). He concludes:

Theorem IX.3.16 shows that WKL0 is conservative over PRA for sentences (in fact sentences). This conservation result, together with the results of Chapter II and IV concerning the development of mathematics within WKL0 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].