Recursive Comprehension

This chapter proves the equivalences between the weak König lemma and the Heine–Borel, extreme value, and uniform continuity theorems. It also discusses the equivalence of the weak König lemma with two famous theorems of topology: the Brouwer fixed point and the Jordan curve theorems. This latter collection of theorems, lying strictly between RCA0 and ACA0, establishes the importance of the system WKL0 whose set existence axiom is the weak König lemma. Between them, RCA0, WKL0, and ACA0 cover the basic theorems of analysis, and they sort them into three different levels of strength. Here, RCA0 can be viewed as an axiom system for “computable analysis.” Its set existence axiom, called recursive comprehension, states the existence of computable sets.

Arithmetical Comprehension

This chapter focuses on arithmetical comprehension. Arithmetical comprehension is the most obvious set existence axiom to use when developing analysis in a system based on Peano arithmetic (PA) with set variables. This axiom asserts the existence of a set X of natural numbers for each property φ‎ definable in the language of PA. More precisely, if φ‎(n) is a property defined in the language of PA plus set variables, but with no set quantifiers, then there is a set X whose members are the natural numbers n such that φ‎(n). Since all such formulas φ‎ are asserted for, the arithmetical comprehension axiom is really an axiom schema. The reason set variables are allowed in φ‎ is to enable sets to be defined in terms of “given” sets. The reason set quantifiers are disallowed in φ‎ is to avoid definitions in which a set is defined in terms of all sets of natural numbers (and hence in terms of itself). The system consisting of PA plus arithmetical comprehension is called ACA0. This system lies at a remarkable “sweet spot” among axiom systems for analysis.

Classical Analysis

This chapter explores the basic concepts that arise when real numbers and continuous functions are studied, particularly the limit concept and its use in proving properties of continuous functions. It gives proofs of the Bolzano–Weierstrass and Heine–Borel theorems, and the intermediate and extreme value theorems for continuous functions. Also, the chapter uses the Heine–Borel theorem to prove uniform continuity of continuous functions on closed intervals, and its consequence that any continuous function is Riemann integrable on closed intervals. In several of these proofs there is a construction by “infinite bisection,” which can be recast as an argument about binary trees. Here, the chapter uses the role of trees to construct an object—the so-called Cantor set.

Classical Arithmetization

This chapter describes how one proceeds from natural to rational numbers, then to real and complex numbers, and to continuous functions—thus arithmetizing the foundations of analysis and geometry. The definitions of integers and rational numbers show why questions about them can, in principle, be reduced to questions about natural numbers and their addition and multiplication. This is what it means to say that the natural numbers are a foundation for the integer and rational numbers. But the next steps in the arithmetization project go beyond algebra. By admitting sets of rational numbers, one can enlarge the number system to one that admits certain infinite operations, such as forming infinite sums. This is crucial to building a foundation for analysis. As such, the chapter turns to the foundations of the natural numbers themselves, the “Peano axioms,” which gives a first glimpse of the logic underlying the arithmetization project.

Historical Introduction

This chapter prepares the reader's mind for reverse mathematics. As its name suggests, reverse mathematics seeks not theorems but the right axioms to prove theorems already known. Reverse mathematics began as a technical field of mathematical logic, but its main ideas have precedents in the ancient field of geometry and the early twentieth-century field of set theory. In geometry, the parallel axiom is the right axiom to prove many theorems of Euclidean geometry, such as the Pythagorean theorem. Set theory offers a more modern example: base theory called ZF, a theorem that ZF cannot prove (the well-ordering theorem) and the “right axiom” for proving it—the axiom of choice. From these and similar examples one can guess at a base theory for analysis, and the “right axioms” for proving some of its well-known theorems.

Computability

This chapter develops the basic results of computability theory, many of which are about noncomputable sequences and sets, with the goal of revealing the limits of computable analysis. Two of the key examples are a bounded computable sequence of rational numbers whose limit is not computable, and a computable tree with no computable infinite path. Computability is an unusual mathematical concept, because it is most easily used in an informal way. One often talks about it in terms of human activities, such as making lists, rather than by applying a precise definition. Nevertheless, there is a precise definition of computability, so this informal description of computations can be formalized.

A Bigger Picture

This chapter aims to pick up some of the ideas dropped from this book and set them in a bigger picture of logic and computability theory. It begins with a sketch of constructive mathematics. Originally developed by a minority of mathematicians opposed to using actual infinities, constructive mathematics contributed some useful techniques for computable mathematics in systems such as RCA0. This is followed by discussions on the completeness of logic and the incompleteness of Peano arithmetic (PA) and related systems. These results reveal mathematics as an arena where theorems cannot always be proved outright, but in which all of their logical equivalents can be found. This creates the possibility of reverse mathematics, where one seeks equivalents that are suitable as axioms. Next, the chapter explains how computability theory helps to distinguish the equivalence classes of theorems, and finally makes a few speculative remarks on the ordering of the equivalence classes, and how this throws light on the concept of mathematical depth.