University of Calgary

# Kohlenbach's Applied Proof Theory is Out!

## This website has moved!

You are looking at an archived page. The website has moved to richardzach.org.

Submitted by Richard Zach on Mon, 06/02/2008 - 5:41pm

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

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^?

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

5 Modified realizability
5.1 The soundness and program extraction theorems
5.2 Remarks on fragments of E-HA^?

6 Majorizability and the fan rule
6.1 A syntactic treatment of majorization and the fan rule

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

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

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

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

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

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^?

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

14 The Friedman A-translation
14.1 The A-translation

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^?

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

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^? [. . .]

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