Reverse Mathematics

Preface xi
1 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