What more do we know about a theorem if we have a proof (by restricted means) than merely that it is true? That’s an old question of Kreisel’s that motivated his “unwinding program”: extract additional information from proofs of theorems in constructive theories, such as bounds on y in theorems of the form ∀x∃y A(x, y).

Ulrich Kohlenbach has worked on problems like this more than anyone else, and his book Applied Proof Theory: Proof Interpretations and Their Use in Mathematics is now out from Springer.

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 Goedel’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.

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 RepresentationofPolish 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