Review of


Stephen G. Simpson:
Subsystems of Second Order Arithmetic

Michael Möllerfeld

Simpson's 'Subsystems of Second Order Arithmetic' is a long awaited textbook on reverse mathematics, a branch of foundational mathematics. Circulated in part for many years and even as a preprint it has become a standard reference for the reductive proof theory of subsystems of second order arithmetic.

Reverse mathematics, introduced and substantially driven forward by Harvey Friedman and Stephen G. Simpson, mainly focuses on the questions 'What are the appropriate axioms for mathematics?', or more precisely, 'Which set existence axioms are needed to prove specific theorems of ordinary non set-theoretical mathematics?'. The aim is to find the somehow weakest axioms which allow one to prove a certain theorem. Thence, if a theorem has been proven from the right (set existence) axioms, the axioms themselves can be proven from the theorem. Hence the theorem and the axioms used to prove it are equivalent (over a weak base theory).

According to the author, ordinary mathematics mainly deals with countable or separable objects, therefore he chose the system of second order arithmetic as a framework for the reverse mathematics presented in his book. Second order arithmetic was introduced by Hilbert and Bernays in Grundlagen der Mathematik (English translation: Foundations of Mathematics).

Reverse mathematics reduces many parts of ordinary mathematics to systems based on a (generalized) finitistic standpoint, hence it can be considered as a partial solution to Hilbert's Program (according to Gödel's incompleteness theorem, this is the best one can expect).

Beside an extensive introduction and an appendix which hints to recent research done in reverse mathematics, Simpson's book splits up in two parts. We will mainly focus on the first part, because it is of formidable interest even for mathematicians who are non-logicians, but interested in the foundations of mathematics.

In the first part the author develops a large amount of ordinary mathematics within subsystems of second order arithmetic. Surprisingly there are five subsystems which naturally arise and turn out to be equivalent to many theorems proved within them. These systems are based on some elementary arithmetic with an induction axiom stating that the set of natural numbers is the least inductive set with respect to inclusion. They are enriched by certain set existence axioms, so called comprehension schemes stating that certain definable classes of natural numbers are sets, and a first order choice principle, known as weak König's lemma. It states that every binary infinite tree has an infinite branch.

Ordered in increasing strength, these systems are as follows: recursive comprehension ( $\ensuremath{\ensuremath{\sf RCA}_0}$), weak König's Lemma ( $\ensuremath{\ensuremath{\sf WKL}_0}$), arithmetical comprehension ( $\ensuremath{\ensuremath{\sf ACA}_0}$), autonomously iterated transfinite recursion ( $\ensuremath{\ensuremath{\sf ATR}_0}$), and $\Pi^1_1$-comprehension ( $\ensuremath{\Pi^1_{1}\text{-}{\sf CA}_0}$).

Each of the five systems can also be considered as a formal framework for a generalized finitistic standpoint. $\ensuremath{\ensuremath{\sf RCA}_0}$ reflects the pure finitistic or constructive standpoint. Hence it could be considered as a formal framework for Bishop style mathematics. $\ensuremath{\ensuremath{\sf WKL}_0}$ is an extension of $\ensuremath{\ensuremath{\sf RCA}_0}$ by a weak non-constructive principle, which allows us to prove 'many of the best-known non-constructive theorems'. Being partially conservative over $\ensuremath{\ensuremath{\sf RCA}_0}$, $\ensuremath{\ensuremath{\sf WKL}_0}$is a formal framework for Hilbert's finitistic reductionism. According to the author, $\ensuremath{\ensuremath{\sf ACA}_0}$ can be considered as the framework for predicativism, whereas $\ensuremath{\ensuremath{\sf ATR}_0}$ is the framework for predicative reductionism. (Due to the limited closure properties of the arithmetical hierarchy I disbelieve that $\ensuremath{\ensuremath{\sf ACA}_0}$ is an appropriate framework for predicativism.) At the very end $\ensuremath{\Pi^1_{1}\text{-}{\sf CA}_0}$ is the paradigm for a fully impredicative system.

Within these systems Simpson develops a large amount of classical mathematics from different fields including analysis, algebra, differential equations, combinatorics, mathematical logic, and descriptive set theory.

We will briefly summarize some of the theorems, which turn out to be equivalent to one of the five systems.

Recursive comprehension, $\ensuremath{\ensuremath{\sf RCA}_0}$, is equivalent for example to Baire's category theorem, the intermediate value theorem, the soundness theorem and a weak form of Gödel's incompleteness theorem, and the existence of the algebraic closure of a countable field.

Weak König's lemma, $\ensuremath{\ensuremath{\sf WKL}_0}$, is for example equivalent to Heine-Borel Covering, the boundedness of every continuous real-valued function on a compact metric space, the maximum principle for real-valued functions on compact metric spaces, the local existence theorem for solutions of ordinary differential equations, Gödel's completeness theorem for countable languages, the uniqueness of the algebraic closure of countable fields of characteristic 0, and the Hahn-Banach theorem.

Arithmetical comprehension, $\ensuremath{\ensuremath{\sf ACA}_0}$ turns out to be equivalent to the following theorems. Bolzano-Weierstraß, every sequence in a compact metric space has a convergent subsequence, the Ascoli-lemma, every countable commutative ring has a maximal ideal, every countable vector space over a countable field has a basis, full König's Lemma, and a Ramsey theorem for colorings.

$\ensuremath{\sf ATR} _0$ is for example equivalent to the comparability of countable well orderings, Ulm's theorem, the perfect set theorem, Lusin separation, and open (and even clopen) determinacy in the Baire space.

$\Pi^1_1$-comprehension, $\ensuremath{\Pi^1_{1}\text{-}{\sf CA}_0}$, is equivalent to each of the following theorems. Every tree has a largest perfect subtree, Cantor-Bendixson, every countable abelian group is the direct sum of a divisible and a reduced one, the determinacy of differences of open sets in the Baire space, and Silver's theorem.

In the second part Simpson develops the model theory of and within our five systems, he also considers much more subsystems of second order arithmetic, which are too much to mention here. They are for example based on collection principles, like the $\Sigma^1_1$ axiom of choice, depended choice principles and bar induction principles. Simpson also gives a set-theoretic interpretation of $\ensuremath{\ensuremath{\sf ATR}_0}$and $\ensuremath{\Pi^1_{1}\text{-}{\sf CA}_0}$. He proves Shoenfield absoluteness within a set-theoretic version of the latter theory. Simpson gives a nice treatment of the theory of $\beta$-models, $\omega$-models and arbitrary models of various subsystems of second order arithmetic. He very briefly describes relations to ordinal informative proof theory.

Simpson's book is an almost self-contained and systematic introduction to reverse mathematics and reductive proof theory of subsystems of second order arithmetic. It consists of many results which are not published elsewhere. Simpson carefully dedicates these results to their origins. The exercises are well deliberated and interesting. They are moderate in difficulty and salutary for the reader.

The whole book is very well and extremely carefully written. The proofs are worked out in very detail.

Simpson's book is highly recommended to mathematicians and philosophers who are interested in this branch of foundational mathematics. The systematical treatment is striking. It would be nice to have more of such accurate treatments in the wide field of proof theory.

Although it has been developed over a long time it is in no way out of fashion.

There is some criticism which is is a matter of taste and therefore it may be obsolete.

Although there are both historical and foundational arguments one might ask why Simpson choosed the language of second order arithmetic as a framework for his book. Some notions might look artificial due to the limited expressiveness of a second order language in contrast to a language consisting of variables for all finite types

The part on ordinal informative proof theory is very brief and therefore of little use.

The author did not focus much on reverse mathematics beyond $\Pi^1_1$-comprehension. On my account there could be more on systems of (generalized) inductive definitions, as these are omnipresent in mathematics. More connections between determinacy and subsystems of second order arithmetic would have been of interest, too. Simpson only mentioned the relation of $\Sigma^1_1$ (monotone) inductive definitions and $\Sigma^0_2$-determinacy. But maybe this would be beyond the scope of this book.

Due to its important role in generalized recursion and computability theory it would also be nice to have a treatment of the notion of admissibility and its relation to $\Pi^1_1$-comprehension.

It's a pity that there is no collection of theorems of ordinary mathematics which are not (known to be) provable within $\Pi^1_1$-comprehension.

All in all Simpson's book is a very highlight in the area of proof theory, both in accuracy and in its systematical and uniform treatment of the results. It is also very useful as a reference book.

Simpson runs a web page on subsystems of second order arithmetic under the URL http://www.personal.psu.edu/t20/sosoa/. Along with some further reviews and a list of recent research and open problems in reverse mathematics it also contains a downloadable version of the extensive introduction of Simpson's book.

About this document ...

Review of


Stephen G. Simpson:
Subsystems of Second Order Arithmetic

This document was generated using the LaTeX2HTML translator Version 98.1p1 release (March 2nd, 1998)

Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, Computer Based Learning Unit, University of Leeds.

The command line arguments were:
latex2html -split 0 moellerfeld.tex.

The translation was initiated by Stephen G Simpson on 2001-01-18