This book presents reverse mathematics to a general mathematical audience for the first time. Reverse mathematics is a new field that answers some old questions. In the two thousand years that mathematicians have been deriving theorems from axioms, it has often been asked: which axioms are needed to prove a given theorem? Only in the last two hundred years have some of these questions been answered, and only in the last forty years has a systematic approach been developed. In Reverse Mathematics, John Stillwell gives a representative view of this field, emphasizing basic analysis-finding the "right axioms" to prove fundamental theorems-and giving a novel approach to logic.Stillwell introduces reverse mathematics historically, describing the two developments that made reverse mathematics possible, both involving the idea of arithmetization. The first was the nineteenth-century project of arithmetizing analysis, which aimed to define all concepts of analysis in terms of natural numbers and sets of natural numbers. The second was the twentieth-century arithmetization of logic and computation. Thus arithmetic in some sense underlies analysis, logic, and computation. Reverse mathematics exploits this insight by viewing analysis as arithmetic extended by axioms about the existence of infinite sets. Remarkably, only a small number of axioms are needed for reverse mathematics, and, for each basic theorem of analysis, Stillwell finds the "right axiom" to prove it.By using a minimum of mathematical logic in a well-motivated way, Reverse Mathematics will engage advanced undergraduates and all mathematicians interested in the foundations of mathematics.

Preface xi1 Historical Introduction 1
1.1 Euclid and the Parallel Axiom 2
1.2 Spherical and Non-Euclidean Geometry 5
1.3 Vector Geometry 10
1.4 Hilbert's Axioms 14
1.5 Well-ordering and the Axiom of Choice 19
1.6 Logic and Computability 23
2 Classical Arithmetization 26
2.1 From Natural to Rational Numbers 27
2.2 From Rationals to Reals 29
2.3 Completeness Properties of R 32
2.4 Functions and Sets 35
2.5 Continuous Functions 37
2.6 The Peano Axioms 39
2.7 The Language of PA 43
2.8 Arithmetically Definable Sets 45
2.9 Limits of Arithmetization 48
3 Classical Analysis 51
3.1 Limits 51
3.2 Algebraic Properties of Limits 53
3.3 Continuity and Intermediate Values 55
3.4 The Bolzano-Weierstrass Theorem 57
3.5 The Heine-Borel Theorem 59
3.6 The Extreme Value Theorem 60
3.7 Uniform Continuity 61
3.8 The Cantor Set 64
3.9 Trees in Analysis 66
4 Computability 70
4.1 Computability and Church's Thesis 71
4.2 The Halting Problem 73
4.3 Computably Enumerable Sets 74
4.4 Computable Sequences in Analysis 77
4.5 Computable Tree with No Computable Path 78
4.6 Computability and Incompleteness 80
4.7 Computability and Analysis 81
5 Arithmetization of Computation 85
5.1 Formal Systems 86
5.2 Smullyan's Elementary Formal Systems 87
5.3 Notations for Positive Integers 89
5.4 Turing's Analysis of Computation 91
5.5 Operations on EFS-Generated Sets 93
5.6 Generating Sets 96
5.7 EFS for Relations 98
5.8 Arithmetizing Elementary Formal Systems 100
5.9 Arithmetizing Computable Enumeration 103
5.10 Arithmetizing Computable Analysis 106
6 Arithmetical Comprehension 109
6.1 The Axiom System ACA0 110
6.2 _ and Arithmetical Comprehension 111
6.3 Completeness Properties in ACA0 113
6.4 Arithmetization of Trees 116
6.5 The Konig Infinity Lemma 118
6.6 Ramsey Theory 121
6.7 Some Results from Logic 124
6.8 Peano Arithmetic in ACA0 127
7 Recursive Comprehension 130
7.1 The Axiom System RCA0 131
7.2 Real Numbers and Continuous Functions 132
7.3 The Intermediate Value Theorem 134
7.4 The Cantor Set Revisited 136
7.5 From Heine-Borel toWeak Konig Lemma 137
7.6 From Weak Konig Lemma to Heine-Borel 140
7.7 Uniform Continuity 141
7.8 FromWeak Konig to Extreme Value 143
7.9 Theorems of WKL0 146
7.10 WKL0, ACA0, and Beyond 149
8 A Bigger Picture 154
8.1 Constructive Mathematics 155
8.2 Predicate Logic 156
8.3 Varieties of Incompleteness 159
8.4 Computability 162
8.5 Set Theory 164
8.6 Concepts of "Depth" 166
Bibliography 168
Index 173