## Applied Proof Theory: Proof Interpretations and their Use in MathematicsThis is the first treatment in book format of proof-theoretic transformations - known as proof interpretations - that focuses on applications to ordinary mathematics. It covers both the necessary logical machinery behind the proof interpretations that are used in recent applications as well as – via extended case studies – carrying out some of these applications in full detail. This subject has historical roots in the 1950s. This book for the first time tells the whole story. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

1 | |

12 | |

Intuitionistic and classical arithmetic in all finite types | 41 |

Representation of Polish metric spaces | 77 |

Modified realizability | 97 |

Majorizability and the fan rule | 108 |

Semiintuitionistic systems and monotone modified realizability | 115 |

Gödels functional Dialectica interpretation | 125 |

Elimination of monotone Skolem functions | 243 |

The Friedman Atranslation | 273 |

general metatheorems I | 278 |

Uniqueness proofs in approximation theory | 297 |

general metatheorems II | 377 |

Applications to the fixed point theory of nonexpansive mappings | 454 |

Final comments | 503 |

507 | |

Semiintuitionistic systems and monotone functional interpretation | 141 |

Systems based on classical logic and functional interpretation | 163 |

Functional interpretation of full classical analysis | 198 |

A nonstandard principle of uniform boundedness | 223 |

List of formal systems and term classes | 524 |

525 | |

529 | |

### Other editions - View all

Applied Proof Theory: Proof Interpretations and their Use in Mathematics Ulrich Kohlenbach No preview available - 2010 |

Applied Proof Theory: Proof Interpretations and their Use in Mathematics Ulrich Kohlenbach No preview available - 2008 |

### Common terms and phrases

analysis applied arbitrary arithmetic assume assumption axioms bar recursion bounded metric space Cauchy Cauchy sequence chapter Chebycheff closed term compact metric space computable constant construct convergence corollary define deﬁned deﬁnition denote E-HA equivalent existence extensionality extract fact ﬁnite ﬁrst ﬁxed point formula free variables functions f G¨odel Hence hyperbolic space implies induction intuitionistic Kohlenbach lemma logical majorizable metatheorems modiﬁed realizability modulus of uniform modulus of uniqueness modus ponens monotone functional interpretation negative translation no-counterexample interpretation nonempty nonexpansive mappings normal form normed spaces obtain parameters point theorem Polish space polynomial prenex normal form primitive recursive functionals proof of theorem proposition provable proved purely universal QF-AC quantifier-free quantiﬁers real numbers Remark representation resp s-maj satisfying schema sentence sequence Skolem normal form soundness theorem theory tuples uniform continuity uniformly convex uniqueness proof upper bound UWKL Vx'Vy WE-HA WE-HAffl yields

### Popular passages

Page 512 - A. Stachura, Uniform convexity of the hyperbolic metric and fixed points of holomorphic mappings in the Hilbert ball, Nonlinear Analysis 4 (1980), 1011-1021.

Page 12 - What more do we know if we have proved a theorem by restricted means than if we merely know that it is true?

Page 513 - Hardy, GH, Wright, EM: An Introduction to the Theory of Numbers, 5th ed.

Page 515 - Kirk, WA, Martinez- Yanez, C., Approximate fixed points for nonexpansive mappings in uniformly convex spaces.

Page 515 - Recursive functionals and quantifiers of finite types, I. Trans. Am. Math. Soc. 91, pp.

Page 513 - The faithfulness of the interpretation of arithmetic in the theory of constructions, J. Symbolic Logic 38:^53 (1973). 17. P. Howard, The formulae-as-types notation of construction, in; "To HB Curry. Essays on Logic, Lambda Calculus and Formalism," Academic Press, London (i960), U79-k90.

Page 509 - Bridges, DS, Richman, F., Julian, WH, Mines, R., Extensions and fixed points of contractive maps in R".

Page 523 - Weyl, H.: The Continuum: A Critical Examination of the Foundation of Analysis.