Proof Theory and Mathematics

Ulrich Kohlenbach, Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Springer, 2008.
Ulrich Kohlenbach presents an applied form of proof theory that has led in recent years to new results in number theory, approximation theory, nonlinear analysis, geodesic geometry and ergodic theory (among others). This applied approach is based on logical transformations (so-called proof interpretations) and concerns the extraction of effective data (such as bounds) from prima facie ineffective proofs as well as new qualitative results such as independence of solutions from certain parameters, generalizations of proofs by elimination of premises.

The book first develops the necessary logical machinery emphasizing novel forms of Gödel's famous functional ('Dialectica') interpretation. It then establishes general logical metatheorems that connect these techniques with concrete mathematics. Finally, two extended case studies (one in approximation theory and one in fixed point theory) show in detail how this machinery can be applied to concrete proofs in different areas of mathematics.


Table of contents:

1 Introduction

2 Unwinding proofs (‘Proof Mining’)
2.1 Introductory remark
2.2 Informal treatment of ineffective proofs
2.3 Herbrand’s theorem and the no-counterexample interpretation
2.4 Exercises, historical comments and suggested further reading

3 Intuitionistic and classical arithmetic in all finite types
3.1 Intuitionistic and classical predicate logic
3.2 Intuitionistic (‘Heyting’) arithmetic HA and Peano arithmetic PA
3.3 Extensional intuitionistic (‘Heyting’) and classical (‘Peano’)
arithmetic in all finite types
3.4 Fragments of (W)E-HA^ω and (W)E-PA^ω
3.5 Fragments corresponding to the Grzegorczyk hierarchy
3.6 Models of E-PA^ω
3.7 Exercises, historical comments and suggested further reading

4 Representation of Polish metric spaces
4.1 Representation of real numbers
4.2 Representation of complete separable metric (‘Polish’) spaces
4.3 Special representation of compact metric spaces
4.4 Fragments, exercises, historical comments and suggested further
reading

5 Modified realizability
5.1 The soundness and program extraction theorems
5.2 Remarks on fragments of E-HA^ω
5.3 Exercises, historical comments and suggested further reading

6 Majorizability and the fan rule
6.1 A syntactic treatment of majorization and the fan rule
6.2 Exercises, historical comments and suggested further reading

7 Semi-intuitionistic systems and monotone modified realizability
7.1 The soundness and bound extraction theorems
7.2 Fragments, exercises, historical comments and suggested further
reading

8 Gödel’s functional (‘Dialectica’) interpretation
8.1 Introduction
8.2 The soundness and program extraction theorems
8.3 Fragments, exercises, historical comments and suggested further
reading

9 Semi-intuitionistic systems and monotone functional interpretation
9.1 The soundness and bound extraction theorems
9.2 Applications of monotone functional interpretation
9.3 Examples of axioms Δ : Weak König’s lemmaWKL
9.4 WKL as a universal sentence Δ
9.5 Fragments, exercises, historical comments and suggested further
reading

10 Systems based on classical logic and functional interpretation
10.1 The negative translation
10.2 Combination of negative translation and functional interpretation
10.3 Application: Uniform weak König’s lemma UWKL
10.4 Elimination of extensionality
10.5 Fragments of (W)E-PA^ω
10.6 The computational strength of full extensionality
10.7 Exercises, historical comments and suggested further reading

11 Functional interpretation of full classical analysis
11.1 Functional interpretation of full comprehension
11.2 Functional interpretation of dependent choice
11.3 Functional interpretation of arithmetical comprehension
11.4 Functional interpretation of (IPP) by finite bar recursion
11.5 Models of bar recursion
11.6 Exercises, historical comments and suggested further reading

12 A non-standard principle of uniform boundedness
12.1 The Σ^0_1 -boundedness principle
12.2 Applications of Σ^0_1 -boundedness
12.3 Remarks on the fragments E-G_nA^ω
12.4 Exercises, historical comments and suggested further reading

13 Elimination of monotone Skolem functions
13.1 Skolem functions of type degree 1 in fragments of finite type
arithmetic
13.2 Elimination of Skolem functions for monotone formulas
13.3 The principle of convergence for bounded monotone sequences
of real numbers (PCM)
13.4 Π^0_1 -CA and Π^0_1 -AC
13.5 The Bolzano-Weierstraß property for bounded sequences in R^d
13.6 Exercises, historical comments and suggested further reading

14 The Friedman A-translation
14.1 The A-translation
14.2 Historical comments and suggested further reading

15 Applications to analysis: general metatheorems I
15.1 A general metatheorem for Polish spaces
15.2 Applications to uniqueness proofs
15.3 Applications to monotone convergence theorems
15.4 Applications to proofs of contractivity
15.5 Remarks on fragments of T^ω
15.6 Historical comments and suggested further reading

16 Case study I: Uniqueness proofs in approximation theory
16.1 Uniqueness proofs in best approximation theory
16.2 Best Chebycheff approximation I
16.3 Best Chebycheff approximation II
16.4 Best L_1-approximation
16.5 Exercises, historical comments and suggested further reading

17 Applications to analysis: general metatheorems II
17.1 Introduction
17.2 Main results in the metric and hyperbolic case
17.3 The case of normed spaces
17.4 Proofs of theorems 17.35, 17.52 and 17.69
17.5 Further variations
17.6 Treatment of several metric or normed spaces X_1 . . . , X_n
simultaneously
17.7 A generalized uniform boundedness principle ∃-UB^X
17.8 Applications of ∃-UB^X
17.9 Fragments of A^ω [. . .]
17.10 Exercises, historical comments and suggested further reading

18 Case study II: Applications to the fixed point theory of nonexpansive
mappings
18.1 General facts
18.2 Applications of the metatheorems from chapter 17
18.3 Logical analysis of the proof of the Borwein-Reich-Shafrir
theorem
18.4 Asymptotically nonexpansive mappings
18.5 Applications of proof mining in ergodic theory
18.6 Exercises, historical comments and suggested further reading

19 Final comments