| Preface | p. vii |
| Acknowledgements | p. xi |
| Common Notations and Terminology | p. xvii |
| Introduction | p. 1 |
| Unwinding proofs ('Proof Mining') | p. 13 |
| Introductory remark | p. 13 |
| Informal treatment of ineffective proofs | p. 13 |
| Herbrand's theorem and the no-counterexample interpretation | p. 22 |
| Exercises, historical comments and suggested further reading | p. 38 |
| Intuitionistic and classical arithmetic in all finite types | p. 41 |
| Intuitionistic and classical predicate logic | p. 41 |
| Intuitionistic ('Heyting') arithmetic HA and Peano arithmetic PA | p. 44 |
| Extensional intuitionistic ('Heyting') and classical ('Peano') arithmetic in all finite types | p. 46 |
| Fragments of (W)E-HA[omega] and (W)E-PA[omega] | p. 52 |
| Fragments corresponding to the Grzegorczyk hierarchy | p. 54 |
| Models of E-PA[omega] | p. 67 |
| Exercises, historical comments and suggested further reading | p. 73 |
| Representation of Polish metric spaces | p. 77 |
| Representation of real numbers | p. 77 |
| Representation of complete separable metric ('Polish') spaces | p. 81 |
| Special representation of compact metric spaces | p. 88 |
| Fragments, exercises, historical comments and suggested further reading | p. 94 |
| Modified realizability | p. 97 |
| The soundness and program extraction theorems | p. 97 |
| Remarks on fragments of E-HA[omega] | p. 105 |
| Exercises, historical comments and suggested further reading | p. 107 |
| Majorizability and the fan rule | p. 109 |
| A syntactic treatment of majorization and the fan rule | p. 109 |
| Exercises, historical comments and suggested further reading | p. 114 |
| Semi-intuitionistic systems and monotone modified realizability | p. 115 |
| The soundness and bound extraction theorems | p. 115 |
| Fragments, exercises, historical comments and suggested further reading | p. 123 |
| Godel's functional ('Dialectica') interpretation | p. 125 |
| Introduction | p. 125 |
| The soundness and program extraction theorems | p. 129 |
| Fragments, exercises, historical comments and suggested further reading | p. 138 |
| Semi-intuitionistic systems and monotone functional interpretation | p. 141 |
| The soundness and bound extraction theorems | p. 141 |
| Applications of monotone functional interpretation | p. 146 |
| Examples of axioms [Delta]: Weak Konig's lemma WKL | p. 149 |
| WKL as a universal sentence [Delta] | p. 156 |
| Fragments, exercises, historical comments and suggested further reading | p. 160 |
| Systems based on classical logic and functional interpretation | p. 163 |
| The negative translation | p. 163 |
| Combination of negative translation and functional interpretation | p. 165 |
| Application: Uniform weak Konig's lemma UWKL | p. 178 |
| Elimination of extensionality | p. 180 |
| Fragments of (W)E-PA[omega] | p. 188 |
| The computational strength of full extensionality | p. 191 |
| Exercises, historical comments and suggested further reading | p. 195 |
| Functional interpretation of full classical analysis | p. 199 |
| Functional interpretation of full comprehension | p. 199 |
| Functional interpretation of dependent choice | p. 206 |
| Functional interpretation of arithmetical comprehension | p. 209 |
| Functional interpretation of (IPP) by finite bar recursion | p. 213 |
| Models of bar recursion | p. 214 |
| Exercises, historical comments and suggested further reading | p. 219 |
| A non-standard principle of uniform boundedness | p. 223 |
| The [Sigma superscript 0 subscript 1]-boundedness principle | p. 223 |
| Applications of [Sigma superscript 0 subscript 1]-boundedness | p. 232 |
| Remarks on the fragments E-G[subscript n]A[omega] | p. 238 |
| Exercises, historical comments and suggested further reading | p. 241 |
| Elimination of monotone Skolem functions | p. 243 |
| Skolem functions of type degree 1 in fragments of finite type arithmetic | p. 243 |
| Elimination of Skolem functions for monotone formulas | p. 247 |
| The principle of convergence for bounded monotone sequences of real numbers (PCM) | p. 262 |
| [Pi superscript 0 subscript 1]-CA and [Pi superscript 0 subscript 1]-AC | p. 265 |
| The Bolzano-Weierstrass property for bounded sequences in R[superscript d] | p. 269 |
| Exercises, historical comments and suggested further reading | p. 272 |
| The Friedman A-translation | p. 273 |
| The A-translation | p. 273 |
| Historical comments and suggested further reading | p. 277 |
| Applications to analysis: general metatheorems I | p. 279 |
| A general metatheorem for Polish spaces | p. 279 |
| Applications to uniqueness proofs | p. 284 |
| Applications to monotone convergence theorems | p. 291 |
| Applications to proofs of contractivity | p. 292 |
| Remarks on fragments of J[omega] | p. 293 |
| Historical comments and suggested further reading | p. 295 |
| Case study I: Uniqueness proofs in approximation theory | p. 297 |
| Uniqueness proofs in best approximation theory | p. 297 |
| Best Chebycheff approximation I | p. 303 |
| Best Chebycheff approximation II | p. 328 |
| Best L[subscript 1]-approximation | p. 348 |
| Exercises, historical comments and suggested further reading | p. 376 |
| Applications to analysis: general metatheorems II | p. 377 |
| Introduction | p. 377 |
| Main results in the metric and hyperbolic case | p. 391 |
| The case of normed spaces | p. 410 |
| Proofs of theorems 17.35, 17.52 and 17.69 | p. 420 |
| Further variations | p. 431 |
| Treatment of several metric or normed spaces X[subscript 1] ..., X[subscript n] simultaneously | p. 435 |
| A generalized uniform boundedness principle [exist]-UB[superscript X] | p. 436 |
| Applications of [exist]-UB[superscript X] | p. 441 |
| Fragments of A[omega] [...] | p. 450 |
| Exercises, historical comments and suggested further reading | p. 452 |
| Case study II: Applications to the fixed point theory of nonexpansive mappings | p. 455 |
| General facts | p. 455 |
| Applications of the metatheorems from chapter 17 | p. 461 |
| Logical analysis of the proof of the Borwein-Reich-Shafrir theorem | p. 468 |
| Asymptotically nonexpansive mappings | p. 496 |
| Applications of proof mining in ergodic theory | p. 499 |
| Exercises, historical comments and suggested further reading | p. 501 |
| Final comments | p. 503 |
| References | p. 507 |
| List of formal systems and term classes | p. 525 |
| List of axioms and rules | p. 527 |
| Index | p. 529 |
| Table of Contents provided by Ingram. All Rights Reserved. |
