Applied Proof Theory: Proof Interpretations and Their Use in Mathematics

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. Gödel’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 II: Applications to the fixed point theory of nonexpansive mappings

19. Final comments

DRM-restrictions

Printing: not available
Clipboard copying: not available

Keywords: MATHEMATICS / General MAT000000