Subsystems of Second Order Arithmetic

Preface. V Acknowledgements. VII Table of Contents. IX Chapter I. Introduction. 1 Section I.1. The Main Question. 1 Section I.2. Subsystems of Z2. 2 Section I.3. The System ACA0. 6 Section I.4. Mathematics Within ACA0. 9 Section I.5. Pi11-CA0 and Stronger Systems. 15 Section I.6. Mathematics Within Pi11-CA0. 18 Section I.7. The System RCA0. 23 Section I.8. Mathematics Within RCA0. 26 Section I.9. Reverse Mathematics. 31 Section I.10. The System WKL0. 34 Section I.11. The System ATR0. 37 Section I.12. The Main Question, Revisited. 41 Section I.13. Outline of Chapters II Through X. 42 Section I.14. Conclusions. 59 Part A. Development of Mathematics Within Subsystems of Z2. 61 Chapter II. Recursive Comprehension. 63 Section II.1. The Formal System RCA0. 63 Section II.2. Finite Sequences. 65 Section II.3. Primitive Recursion. 69 Section II.4. The Number Systems. 73 Section II.5. Complete Separable Metric Spaces. 78 Section II.6. Continuous Functions. 84 Section II.7. More on Complete Separable Metric Spaces. 88 Section II.8. Mathematical Logic. 91 Section II.9. Countable Fields. 96 Section II.10. Separable Banach Spaces. 99 Section II.11. Conclusions. 103 Chapter III. Arithmetical Comprehension. 105 Section III.1. The Formal System ACA0. 105 Section III.2. Sequential Compactness. 106 Section III.3. Strong Algebraic Closure. 110 Section III.4. Countable Vector Spaces. 111 Section III.5. Maximal Ideals in Countable Commutative Rings. 115 Section III.6. Countable Abelian Groups. 117 Section III.7. K"onigs Lemma and Ramseys Theorem. 121 Section III.8. Conclusions. 125 Chapter IV. Weak K"onigs Lemma. 127 Section IV.1. The Heine/Borel Covering Lemma. 127 Section IV.2. Properties of Continuous Functions. 132 Section IV.3. The G"odel Completeness Theorem. 139 Section IV.4. Formally Real Fields. 141 Section IV.5. Uniqueness of Algebraic Closure. 144 Section IV.6. Prime Ideals in Countable Commutative Rings. 146 Section IV.7. Fixed Point Theorems. 148 Section IV.8. Ordinary Differential Equations. 153 Section IV.9. The Separable Hahn/Banach Theorem. 160 Section IV.10. Conclusions. 165 Chapter V. Arithmetical Transfinite Recursion. 167 Section V.1. Countable Well Orderings; Analytic Sets. 167 Section V.2. The Formal System ATR0. 173 Section V.3. Borel Sets. 178 Section V.4. Perfect Sets; Pseudohierarchies. 185 Section V.5. Reversals. 189 Section V.6. Comparability of Countable Well Orderings. 195 Section V.7. Countable Abelian Groups. 199 Section V.8. Sigma01 and Delta01 Determinacy. 203 Section V.9. The Sigma01 and Delta01 Ramsey Theorems. 210 Section V.10. Conclusions. 215 Chapter VI. Pi11 Comprehension. 217 Section VI.1. Perfect Kernels. 217 Section VI.2. Coanalytic Uniformization. 221 Section VI.3. Coanalytic Equivalence Relations. 226 Section VI.4. Countable Abelian Groups. 230 Section VI.5. Sigma01i01 Determinacy. 233 Section VI.6. The Delta02 Ramsey Theorem. 236 Section VI.7. Stronger Set Existence Axioms. 239 Section VI.8. Conclusions. 241 Part B. Models of Subsystems of Z2. 243 Chapter VII. Beta-Models. 245 Section VII.1. The Minimum Beta-Model of Pi11-CA0. 246 Section VII.2. Countable Coded Beta-Models. 250 Section VII.3. A Set-Theoretic Interpretation of ATR0. 260 Section VII.4. Constructible Sets and Absoluteness. 275 Section VII.5. Strong Comprehension Schemes. 289 Section VII.6. Strong Choice Schemes. 296 Section VII.7. Beta-Model Reflection. 306 Section VII.8. Conclusions. 310 Chapter VIII. Omega-Models. 313 Section VIII.1. Omega-Models of RCA0 and ACA0. 314 Section VIII.2. Countable Coded Omega-models of WKL0. 318 Section VIII.3. Hyperarithmetical Sets. 326 Section VIII.4. Omega-Models of Sigma11 Choice. 337 Section VIII.5. Omega-Model Reflection and Incompleteness. 347 Section VIII.6. Omega-Models of Strong Systems. 353 Section VIII.7. Conclusions. 361 Chapter IX. Non-Omega-Models. 363 Section IX.1. The First Order Parts of RCA0 and ACA0. 364 Section IX.2. The First Order Part of WKL0. 369 Section IX.3. A Conservation Result for Hilberts Program. 373 Section IX.4. Saturated Models. 383 Section IX.5. Gentzen-Style Proof Theory. 390 Section IX.6. Conclusions. 392 Appendix. 395 Chapter X. Additional Results. 395 Section X.1. Measure Theory. 395 Section X.2. Separable Banach Spaces. 401 Section X.3. Countable Combinatorics. 403 Section X.4. Reverse Mathematics for RCA0. 410 Section X.5. Conclusions. 411 Bibliography. 413 Index. 425 List of Tables. 445 ^