Applied proof theory: Proof interpretations and their use in mathematics

Ulrich Kohlenbach (auth.)3540775323, 9783540775324, 9783540775331

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 :
Front Matter….Pages i-xix
Introduction….Pages 1-11
Unwinding proofs (‘Proof Mining’)….Pages 13-40
Intuitionistic and classical arithmetic in all finite types….Pages 41-76
Representation of Polish metric spaces….Pages 77-95
Modified realizability….Pages 97-107
Majorizability and the fan rule….Pages 109-114
Semi-intuitionistic systems and monotone modified realizability….Pages 115-124
Gödel’s functional (‘Dialectica’) interpretation….Pages 125-140
Semi-intuitionistic systems and monotone functional interpretation….Pages 141-161
Systems based on classical logic and functional interpretation….Pages 163-197
Functional interpretation of full classical analysis….Pages 199-221
A non-standard principle of uniform boundedness….Pages 223-242
Elimination of monotone Skolem functions….Pages 243-272
The Friedman A -translation….Pages 273-277
Applications to analysis: general metatheorems I….Pages 279-295
Case study I: Uniqueness proofs in approximation theory….Pages 297-376
Applications to analysis: general metatheorems II….Pages 377-453
Case study II: Applications to the fixed point theory of nonexpansive mappings….Pages 455-502
Final comments….Pages 503-506
Back Matter….Pages 507-532