SIAM News Blog
SIAM News

A New Mathematical Field Answers Old Questions

Reverse Mathematics: Proofs from the Inside Out. By John Stillwell. Courtesy of Princeton University Press.
Reverse Mathematics: Proofs from the Inside Out. By John Stillwell. Princeton University Press, Princeton, NJ, January 2018. 200 pages, \$24.95.

It distresses John Stillwell that foundational questions, long in the mainstream of mathematical research, amount to little more than a backwater today. His latest book, Reverse Mathematics, is intended to acquaint colleagues with recent progress in the field and convince them that exciting discoveries remain to be made. He notes in passing that the same foundations underlie not only the several branches of mathematics, but physics and computer science as well.

While mathematicians ordinarily deduce theorems from axioms, reverse mathematicians seek to identify the axioms that establish key theorems like the Bolzano-Weierstrass, Heine-Borel, intermediate value, extreme value, uniform continuity, and Riemann integrability theorems. This approach enables Stillwell to attach a precise meaning to the notion of mathematical “depth.” He argues that one proposition is deeper than another if its proof requires stronger axioms. Time will tell if his suggestion “catches on.”

The early chapters of Reverse Mathematics summarize 19th-century efforts to place mathematics on a firm foundation, beginning with David Hilbert’s elimination of the gaps in Euclid and including the axiomatic treatment of algebra and arithmetic by Richard Dedekind, Giuseppe Peano, and others. Gottlob Frege believed for a time that he had answered all remaining questions on the basis of Georg Cantor’s set theory. But Russell’s paradox derailed that approach (before Frege’s book even published) by showing that the seemingly simple concept of a set is in fact elusive.

Students of reverse mathematics focus on three recently-identified axiom systems—designated $$RCA_0 \subset WKL_0 \subset ACA_0$$—that differ only in the sets they presume to classify. The symbol $$\subset$$ indicates that each system includes all sets recognized by the preceding system, in addition to others. An effort is underway to devise a “constructible mathematics” (particularly an analysis) that recognizes only computable numbers and functions that are computable in the sense that $$f(x)$$ is computable for any computable $$x.$$

Alan Turing was apparently the first (in 1936) to define the term “computable number” and demonstrate that some numbers are not computable. By the time he did so, Alonzo Church had already introduced a somewhat different notion of computability—without employing the term—that turned out to be equivalent to Turing’s explanation. Furthermore, Emil Post had proposed yet another definition several years earlier (in 1924) but refrained from publishing it for fear of having failed to capture the full meaning of the computability concept. It was not until the 1940s that the trio reached agreement and fairly distinguished that which is computable from that which is not.

$$RCA_0, WKL_0$$, and $$ACA_0$$ all consist of the Zermelo-Fraenkel (ZF) axioms of set theory, augmented by a single set existence axiom. Thus, writes Stillwell, the ZF axioms form a base foundational system that may be augmented in multiple ways. The situation is similar to one prevalent in geometry, where the axioms of absolute geometry (those of Euclidean geometry minus the parallel axiom) form a base system. One can enhance this system with different approaches to yield the various Euclidean and non-Euclidean geometries. The base system suffices to demonstrate the logical equivalence of various propositions of Euclidean geometry—such as the Pythagorean theorem, the existence of similar triangles and triangles of arbitrarily large area, and so on—without proof. It is likewise similar to the situation in set theory, where the ZF system can prove Zorn’s lemma, the Hausdorff maximal principle, the well-ordering principle, and the axiom of choice equivalent to one another in the sense that either all are true or all are false, without being able to decide which.

Reverse mathematics, which is largely the work of Stephen Simpson and Harvey Friedman, is often concerned with finding the “right axioms” for proving a given theorem, i.e., the weakest system from which one can deduce the theorem in question. Stillwell quotes Friedman to the effect that, “when a theorem is proved from the right axioms, the axioms can [as in the foregoing examples] be proved from the theorem.”

The set existence axiom for $$RCA_0$$ is nothing but the set of Turing-computable numbers, together with subsets thereof. But that is not rich enough to prove Bolzano-Weierstrass, Heine-Borel, and other fundamental theorems of analysis, which require more sets for proof.

Reverse mathematics makes essential use of a lemma proven in 1927 by Dénes König, the strong form of which asserts that a finitely branching rooted tree with infinitely many vertices contains an infinite path. The proof is almost immediate in that if, for some natural number $$n$$, all of the sub-trees separated from the root by a path of exactly $$n$$ edges contained only finitely many vertices, then the tree itself would contain only finitely many vertices. The weak form of König’s lemma is merely restriction of the strong form to binary trees. The set existence axiom for $$WKL_0$$ expands the notion of “computable number” to include any real number contained in a convergent sequence of nested intervals with Turing-computable end points.

The focus on nested intervals is important because bounded sets of $$WKL_0$$-computable numbers need not have $$WKL_0$$-computable upper bounds. Indeed, Stillwell exhibits a bounded and increasing sequence of such numbers with no $$WKL_0$$-computable upper bound. A useful consequence of the preceding definition is the ability—given $$WKL_0$$-computable $$a$$, $$b$$,  and $$f$$, such that $$f(a)f(b)<0$$—to solve the equation $$f(x)=0$$ by the bisection method for a $$WKL_0$$-computable $$x$$. Needless to say, such a computation charts an infinite path through the complete (unpruned) binary tree.

One can deduce most of the basic theorems of analysis from the $$WKL_0$$ axioms, with the possibly surprising exception (given its similarity to Heine-Borel) of Bolzano-Weierstrass. That theorem requires the strong form of König’s lemma, which follows from the set existence axiom for $$ACA_0$$ namely

$\exists X (n \in X \Leftrightarrow \varphi(n)),$

$$\varphi$$ being any formula from a specified class of formulae constructed from the following:

$variables: x,y,z,...,X,Y,Z,...$

$constants: a, b, c,...$

$function symbols: f, g, h, ...$

$predicate symbols: P, Q, R, ...$

$logic symbols: \vee, \wedge, \sim, \Rightarrow, \Leftrightarrow, \forall, \exists,$

together with commas and parentheses, and subject to certain restrictions on the use of quantifiers $$\forall$$ and $$\exists$$. Several such proofs are carried out in tutorial detail in the latter chapters of Reverse Mathematics. According to Stillwell, logicians currently recognize the “big five” axiom systems, of which $$RCA_0 \subset WKL_0 \subset ACA_0$$ are merely the simplest three. He primarily confines his exposition to these three because they appear to cover most of what concerns working mathematicians.

All in all, Stillwell has written a very readable book on a little-known subject of at least peripheral interest to every mathematician. It would be interesting to know what further developments he foresees.

James Case writes from Baltimore, Maryland.