Applied Proof Theory: Proof Interpretations and Their Use in Mathematics

Common Notations and Terminology 1. Introduction 2. Unwinding proofs ('Proof Mining') 3. Intuitionistic and classical arithmetic in all finite types 4. Representation of Polish metric spaces 5. Modified realizability 6. Majorizability and the fan rule 7. Semi-intuitionistic systems and monotone modified realizability 8. Godel's functional ('Dialectica') interpretation 9. Semi-intuitionistic systems and monotone functional interpretation 10. Systems based on classical logic and functional interpretation 11. Functional interpretation of full classical analysis 12. A non-standard principle of uniform boundedness 13. Elimination of monotone Skolem functions 14. The Friedman A-translation 15. Applications to analysis: general metatheorems I 16. Case study I: Uniqueness proofs in approximation theory 17. Applications to analysis: general metatheorems II 18. Case study 11: Applications to the fixed point theory of nonexpansive mappings 19. Final comments References List of Formal Systems and term Classes List of axioms and rules Index