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

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

(i) Induction Axiom:

$\forall X[(0\in X\wedge \forall n(n\in X\rightarrow n+1\in X))\rightarrow \forall n(n\in X)]$

(ii) Full 2nd Order Comprehension Scheme:

$\exists X\forall n(n\in X\leftrightarrow \varphi (n))$,

where $\varphi (n)$ is any formula of L₂ in which X does not occur freely.

The strong deductive power of Z₂ 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 $\varphi (n)$ holds. Note that the induction axiom (i) is distinct from (and sometimes weaker than) the full second-order induction scheme , $[\varphi (0)\wedge \forall n(\varphi (n)\rightarrow \varphi (n+1))]\rightarrow \forall n\varphi (n)$. However, this scheme is in fact provable in full Z₂.

The five main subsystems of Z₂ studied are, in increasing logical strength, RCA₀ (recursive comprehension axiom), WKL₀ (Weak König's Lemma), ACA₀ ( arithmetical comprehension axiom), ATR₀ ( arithmetic transfinite recursion) and $\Pi _{1}^{1}$-CA₀ ( $% \Pi _{1}^{1}$ comprehension axiom). Each of the three subsystems RCA₀, ACA₀ and $\Pi _{1}^{1}$-CA₀of Z₂ is defined by a specification of a restricted class of formulas which can go into either the comprehension or induction schemes (roughly, either $\Sigma _{k}^{n}$ formulas or $\Pi _{k}^{n}$ formulas or a combination. I lack the space to go into details). WKL₀ is RCA₀ 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₀ is ACA₀ plus an axiom scheme which permits transfinite recursion on well-ordered sequences. (It turns out that these systems WKL₀ and ATR₀ are equivalent (over RCA₀) to $\Sigma _{1}^{0}$ separation and $\Sigma _{1}^{1}$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₀. As Simpson explains, ``RCA₀ ... 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
$\Pi _{1}^{1}$-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 Z<sub>2</sub>), (2) a sequence S<sub>1</sub>,S<sub>2</sub>,..., of set-existence axioms of increasing strength, and (3) some (core mathematical) theorem $\varphi$. A ``reversal'' is then to establish a metatheorem of the form: $\mathbf{B}\vdash \varphi \leftrightarrow \mathbf{S}_{i}$. Results of this form establish not only that the theorem $\varphi$ can be proved in the system $\mathbf{B}\cup \mathbf{S}_{i}$, but also that the axiom (or each instance of the axiom scheme) S_i can be deduced from the theorem $\varphi$ (modulo B, of course). It then follows that (modulo B) the axiom S_i is the weakest such from which the theorem $\varphi$ can be proved. Throughout the bulk of Simpson's book, the base theory chosen is RCA₀. Chapter III develops in detail the main known reversals for ACA₀. Consider the Bolzano/Weierstrass Theorem, BW : ``Every bounded sequence of real numbers, or of points in $\mathbb{R} ^{n}$, has a convergent subsequence''. Theorem III.2.2 (pp. 106-7) shows that BW is equivalent to ACA₀ over RCA₀. That is, RCA $_{0}\vdash \mathbf{BW}\leftrightarrow \mathbf{ACA}_{0}$. 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₂. 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-$\omega$-Models'') are model-theoretic, but are mainly geared up to proving conservation theorems. A theory $\mathbf{% T}^{\ast }$ in $\mathbf{L}^{\ast }$ is a conservative extension of another theory T in L just in case $\mathbf{L}% \subseteq \mathbf{L}^{\ast }$, $\mathbf{T}\subseteq \mathbf{T}^{\ast }$ and any L-theorem $\varphi$ of the extended theory $\mathbf{T}^{\ast }$is already a theorem of T. Chapter IX contains several conservativeness results for subsystems of Z<sub>2</sub>. For example, (a) ACA<sub>0</sub> is conservative over PA for L<sub>1</sub>sentences; (b) RCA<sub>0</sub> is conservative over $\Sigma _{1}^{0}$ -PA (PA with restricted induction), (c) WKL<sub>0</sub>is conservative over RCA<sub>0</sub> for $\Pi _{1}^{1}$ sentences; (d) WKL<sub>0</sub> is conservative over PRA for $\Pi _{2}^{0}$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₂are conservative over PRA for $\Pi _{1}^{0}$ sentences? ...'' (p. 382). He concludes:

Theorem IX.3.16 shows that WKL₀ is conservative over PRA for $\Pi _{1}^{0}$ sentences (in fact $\Pi _{2}^{0}$ sentences). This conservation result, together with the results of Chapter II and IV concerning the development of mathematics within WKL₀ 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].