Preface |
|
vii | |
Acknowledgments |
|
xi | |
|
|
1 | (14) |
|
1.1 What is reverse mathematics? |
|
|
1 | (2) |
|
|
3 | (3) |
|
1.3 Considerations about coding |
|
|
6 | (2) |
|
1.4 Philosophical implications |
|
|
8 | (2) |
|
1.5 Conventions and notation |
|
|
10 | (5) |
|
Part I Computable mathematics |
|
|
|
|
15 | (36) |
|
2.1 The informal idea of computability |
|
|
15 | (2) |
|
2.2 Primitive recursive functions |
|
|
17 | (6) |
|
2.2.1 Some primitive recursive functions |
|
|
19 | (1) |
|
2.2.2 Bounded quantification |
|
|
20 | (2) |
|
2.2.3 Coding sequences with primitive recursion |
|
|
22 | (1) |
|
|
23 | (3) |
|
|
26 | (5) |
|
2.5 Computably enumerable sets and the halting problem |
|
|
31 | (2) |
|
2.6 The arithmetical hierarchy and Post's theorem |
|
|
33 | (3) |
|
2.7 Relativization and oracles |
|
|
36 | (1) |
|
|
37 | (11) |
|
|
39 | (4) |
|
|
43 | (3) |
|
|
46 | (2) |
|
|
48 | (3) |
|
3 Instance-solution problems |
|
|
51 | (26) |
|
|
51 | (2) |
|
|
53 | (3) |
|
3.3 Multiple problem forms |
|
|
56 | (3) |
|
|
59 | (2) |
|
|
61 | (2) |
|
|
63 | (5) |
|
|
68 | (2) |
|
|
70 | (4) |
|
|
74 | (3) |
|
|
77 | (30) |
|
4.1 Subproblems and identity reducibility |
|
|
78 | (3) |
|
4.2 Computable reducibility |
|
|
81 | (3) |
|
4.3 Weihrauch reducibility |
|
|
84 | (4) |
|
|
88 | (3) |
|
4.5 Multiple applications |
|
|
91 | (4) |
|
|
95 | (5) |
|
4.7 Hirschfeldt-Jockusch games |
|
|
100 | (3) |
|
|
103 | (4) |
|
Part II Formalization and syntax |
|
|
|
5 Second order arithmetic |
|
|
107 | (46) |
|
|
107 | (4) |
|
5.2 Hierarchies of formulas |
|
|
111 | (2) |
|
5.2.1 Arithmetical formulas |
|
|
111 | (2) |
|
5.2.2 Analytical formulas |
|
|
113 | (1) |
|
|
113 | (4) |
|
5.3.1 First order arithmetic |
|
|
113 | (2) |
|
5.3.2 Second order arithmetic |
|
|
115 | (2) |
|
5.4 Formalization, and on ω and N |
|
|
117 | (1) |
|
|
118 | (5) |
|
|
118 | (1) |
|
|
119 | (3) |
|
5.5.3 Formalizing computability theory |
|
|
122 | (1) |
|
5.6 The subsystems ACA0 and WKL0 |
|
|
123 | (6) |
|
|
124 | (3) |
|
|
127 | (2) |
|
5.7 Equivalences between mathematical principles |
|
|
129 | (3) |
|
5.8 The subsystems πl-CA0 and ATR0 |
|
|
132 | (9) |
|
5.8.1 The subsystem π1-CA0 |
|
|
132 | (4) |
|
|
136 | (5) |
|
|
141 | (2) |
|
5.10 First order parts of theories |
|
|
143 | (1) |
|
5.11 Comparing reducibility notions |
|
|
144 | (2) |
|
5.12 Full second order semantics |
|
|
146 | (2) |
|
|
148 | (5) |
|
|
153 | (22) |
|
6.1 Induction, bounding, and least number principles |
|
|
153 | (5) |
|
6.2 Finiteness, cuts, and all that |
|
|
158 | (4) |
|
6.3 The Kirby-Paris hierarchy |
|
|
162 | (4) |
|
6.4 Reverse recursion theory |
|
|
166 | (2) |
|
6.5 Hirst's theorem and B2Σ02 |
|
|
168 | (4) |
|
6.6 So, why Σ01 induction? |
|
|
172 | (2) |
|
|
174 | (1) |
|
|
175 | (28) |
|
|
175 | (2) |
|
|
177 | (5) |
|
7.3 Density and genericity |
|
|
182 | (4) |
|
|
186 | (3) |
|
|
189 | (5) |
|
|
194 | (2) |
|
7.7 Harrington's theorem and conservation |
|
|
196 | (3) |
|
|
199 | (4) |
|
|
|
|
203 | (56) |
|
|
204 | (5) |
|
|
209 | (3) |
|
|
212 | (4) |
|
8.4 Stability and cohesiveness |
|
|
216 | (7) |
|
|
217 | (4) |
|
|
221 | (2) |
|
8.5 The Cholak-Jockusch-Slaman decomposition |
|
|
223 | (8) |
|
8.5.1 A different proof of Seetapun's theorem |
|
|
225 | (3) |
|
|
228 | (3) |
|
|
231 | (7) |
|
|
232 | (2) |
|
8.6.2 Proof of Lemma 8.6.6 |
|
|
234 | (1) |
|
8.6.3 Proof of Lemma 8.6.7 |
|
|
234 | (4) |
|
8.7 The first order part of RT |
|
|
238 | (13) |
|
8.7.1 Two versus arbitrarily many colors |
|
|
238 | (3) |
|
8.7.2 Proof of Proposition 8.7.4 |
|
|
241 | (4) |
|
8.7.3 Proof of Proposition 8.7.5 |
|
|
245 | (4) |
|
8.7.4 What else is known? |
|
|
249 | (2) |
|
8.8 The SRT; vs. COH problem |
|
|
251 | (5) |
|
8.9 Summary: Ramsey's theorem and the "big five" |
|
|
256 | (1) |
|
|
257 | (2) |
|
9 Other combinatorial principles |
|
|
259 | (104) |
|
9.1 Finer results about RT |
|
|
259 | (12) |
|
9.1.1 Ramsey's theorem for singletons |
|
|
259 | (6) |
|
9.1.2 Ramsey's theorem for higher exponents |
|
|
265 | (5) |
|
9.1.3 Homogeneity vs. limit homogeneity |
|
|
270 | (1) |
|
9.2 Partial and linear orders |
|
|
271 | (20) |
|
9.2.1 Equivalences and bounds |
|
|
272 | (3) |
|
9.2.2 Stable partial and linear orders |
|
|
275 | (4) |
|
9.2.3 Separations over RCA0 |
|
|
279 | (7) |
|
9.2.4 Variants under finer reducibilities |
|
|
286 | (5) |
|
9.3 Polarized Ramsey's theorem |
|
|
291 | (3) |
|
9.4 Rainbow Ramsey's theorem |
|
|
294 | (9) |
|
|
303 | (2) |
|
9.6 The Chubb-Hirst-McNicholl tree theorem |
|
|
305 | (4) |
|
9.7 Milliken's tree theorem |
|
|
309 | (3) |
|
9.8 Thin set and free set theorems |
|
|
312 | (5) |
|
|
317 | (21) |
|
9.9.1 Apartness, gaps, and finite unions |
|
|
319 | (4) |
|
9.9.2 Towsner's simple proof |
|
|
323 | (6) |
|
9.9.3 Variants with bounded sums |
|
|
329 | (7) |
|
9.9.4 Applications of the Lovasz local lemma |
|
|
336 | (2) |
|
9.10 Model theoretic and set theoretic principles |
|
|
338 | (11) |
|
9.10.1 Languages, theories, and models |
|
|
338 | (2) |
|
9.10.2 The atomic model theorem |
|
|
340 | (5) |
|
9.10.3 The finite intersection principle |
|
|
345 | (4) |
|
9.11 Weak weak Konig's lemma |
|
|
349 | (5) |
|
9.12 The reverse mathematics zoo |
|
|
354 | (1) |
|
|
355 | (8) |
|
|
|
|
363 | (38) |
|
10.1 Formalizations of the real line |
|
|
364 | (2) |
|
10.2 Sequences and convergence |
|
|
366 | (2) |
|
10.3 Sets and continuous functions |
|
|
368 | (3) |
|
|
368 | (1) |
|
10.3.2 Continuous functions |
|
|
369 | (2) |
|
10.4 The intermediate value theorem |
|
|
371 | (2) |
|
10.5 Closed sets and compactness |
|
|
373 | (7) |
|
10.5.1 Separably closed sets |
|
|
376 | (3) |
|
10.5.2 Uniform continuity and boundedness |
|
|
379 | (1) |
|
10.6 Topological dynamics and ergodic theory |
|
|
380 | (8) |
|
10.6.1 BirkhofFs recurrence theorem |
|
|
381 | (4) |
|
10.6.2 The Auslander-Ellis theorem and iterated Hindman's theorem |
|
|
385 | (3) |
|
10.6.3 Measure theory and the mean ergodic theorem |
|
|
388 | (1) |
|
10.7 Additional results in real analysis |
|
|
388 | (2) |
|
10.8 Topology, MF spaces, CSC spaces |
|
|
390 | (7) |
|
10.8.1 Countable, second countable spaces |
|
|
390 | (3) |
|
|
393 | (2) |
|
10.8.3 Reverse mathematics of MF spaces |
|
|
395 | (2) |
|
|
397 | (4) |
|
|
401 | (26) |
|
11.1 Groups, rings, and other structures |
|
|
401 | (2) |
|
11.2 Vector spaces and bases |
|
|
403 | (3) |
|
11.3 The complexity of ideals |
|
|
406 | (4) |
|
|
410 | (5) |
|
11.5 The Nielsen-Schreier theorem |
|
|
415 | (5) |
|
|
420 | (3) |
|
|
423 | (4) |
|
|
427 | (32) |
|
12.1 Well orderings and ordinals |
|
|
427 | (12) |
|
12.1.1 The Zj separation principle |
|
|
428 | (3) |
|
12.1.2 Comparability of well orderings |
|
|
431 | (4) |
|
12.1.3 Proof of Proposition 12.1.12 |
|
|
435 | (4) |
|
12.2 Descriptive set theory |
|
|
439 | (4) |
|
|
443 | (9) |
|
12.3.1 Gale-Stewart games |
|
|
443 | (2) |
|
12.3.2 Clopen and open determinacy |
|
|
445 | (3) |
|
12.3.3 Godel's constructible universe |
|
|
448 | (1) |
|
12.3.4 Friedman's theorem |
|
|
449 | (3) |
|
12.4 Higher order reverse mathematics |
|
|
452 | (5) |
|
|
457 | (2) |
References |
|
459 | (14) |
Index |
|
473 | |