Applied Proof Theory: Proof Interpretations and their Use in Mathematics (eBook)

Ulrich Kohlenbach has been Professor of Mathematics at the Technische Universität Darmstadt since 2004. He is a managing editor of the "Annals of Pure and Applied Logic". 

Preface 6
Acknowledgements 10
Common Notations and Terminology 16
Introduction 19
Unwinding proofs (`Proof Mining') 30
Introductory remark 30
Informal treatment of ineffective proofs 30
Herbrand's theorem and the no-counterexample interpretation 39
Exercises, historical comments and suggested further reading 55
Intuitionistic and classical arithmetic in all finite types 58
Intuitionistic and classical predicate logic 58
Intuitionistic (`Heyting') arithmetic HA and Peano arithmetic PA 61
Extensional intuitionistic (`Heyting') and classical (`Peano') arithmetic in all finite types 63
Fragments of (W)E-HA and (W)E-PA 69
Fragments corresponding to the Grzegorczyk hierarchy 71
Models of E-PA 84
Exercises, historical comments and suggested further reading 90
Representation of Polish metric spaces 94
Representation of real numbers 94
Representation of complete separable metric (`Polish') spaces 98
Special representation of compact metric spaces 105
Fragments, exercises, historical comments and suggested further reading 111
Modified realizability 113
The soundness and program extraction theorems 113
Remarks on fragments of E-HA 121
Exercises, historical comments and suggested further reading 123
Majorizability and the fan rule 124
A syntactic treatment of majorization and the fan rule 124
Exercises, historical comments and suggested further reading 129
Semi-intuitionistic systems and monotone modified realizability 130
The soundness and bound extraction theorems 130
Fragments, exercises, historical comments and suggested further reading 138
Gödel's functional (`Dialectica') interpretation 140
Introduction 140
The soundness and program extraction theorems 144
Fragments, exercises, historical comments and suggested further reading 153
Semi-intuitionistic systems and monotone functional interpretation 156
The soundness and bound extraction theorems 156
Applications of monotone functional interpretation 161
Examples of axioms : Weak König's lemma WKL 164
WKL as a universal sentence 171
Fragments, exercises, historical comments and suggested further reading 175
Systems based on classical logic and functional interpretation 177
The negative translation 177
Combination of negative translation and functional interpretation 179
Application: Uniform weak König's lemma UWKL 192
Elimination of extensionality 194
Fragments of (W)E-PA 202
The computational strength of full extensionality 205
Exercises, historical comments and suggested further reading 209
Functional interpretation of full classical analysis 212
Functional interpretation of full comprehension 212
Functional interpretation of dependent choice 219
Functional interpretation of arithmetical comprehension 222
Functional interpretation of (IPP) by finite bar recursion 226
Models of bar recursion 227
Exercises, historical comments and suggested further reading 232
A non-standard principle of uniform boundedness 235
The 01-boundedness principle 235
Applications of 01-boundedness 244
Remarks on the fragments E-GnA 250
Exercises, historical comments and suggested further reading 253
Elimination of monotone Skolem functions 255
Skolem functions of type degree 1 in fragments of finite type arithmetic 255
Elimination of Skolem functions for monotone formulas 259
The principle of convergence for bounded monotone sequences of real numbers (PCM) 274
01-CA and 01-AC 277
The Bolzano-Weierstraß property for bounded sequences in Rd 281
Exercises, historical comments and suggested further reading 284
The Friedman A-translation 285
The A-translation 285
Historical comments and suggested further reading 289
Applications to analysis: general metatheorems I 290
A general metatheorem for Polish spaces 290
Applications to uniqueness proofs 295
Applications to monotone convergence theorems 302
Applications to proofs of contractivity 303
Remarks on fragments of T 304
Historical comments and suggested further reading 306
Case study I: Uniqueness proofs in approximation theory 307
Uniqueness proofs in best approximation theory 307
Best Chebycheff approximation I 313
Best Chebycheff approximation II 338
Best L1-approximation 358
Exercises, historical comments and suggested further reading 386
Applications to analysis: general metatheorems II 387
Introduction 387
Main results in the metric and hyperbolic case 401
The case of normed spaces 420
Proofs of theorems 17.35, 17.52 and 17.69 430
Further variations 441
Treatment of several metric or normed spaces X1…,Xn simultaneously 445
A generalized uniform boundedness principle -UBX 446
Applications of -UBX 451
Fragments of A[…] 460
Exercises, historical comments and suggested further reading 462
Case study II: Applications to the fixed point theory of nonexpansive mappings 464
General facts 464
Applications of the metatheorems from chapter 17 470
Logical analysis of the proof of the Borwein-Reich-Shafrir theorem 477
Asymptotically nonexpansive mappings 505
Applications of proof mining in ergodic theory 508
Exercises, historical comments and suggested further reading 510
Final comments 512
References 516
List of formal systems and term classes 533
List of axioms and rules 534
Index 536