Applied Proof Theory: Proof Interpretations and their Use in Mathematics

Front Cover
Springer Science & Business Media, May 23, 2008 - Mathematics - 536 pages
0 Reviews

This 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

Introduction
1
Unwinding proofs Proof Mining
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
References
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
List of axioms and rules
525
Index
529
Copyright

Other editions - View all

Common terms and phrases

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.

About the author (2008)

Ulrich Kohlenbach has been Professor of Mathematics at the Technische Universität Darmstadt since 2004. He is a managing editor of the "Annals of Pure and Applied Logic". 

Bibliographic information