Applied Proof Theory: Proof Interpretations and their Use in Mathematics

AvUlrich Kohlenbach

Häftad, Engelska, 2010

Del i serien Springer Monographs in Mathematics

1 378 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt över 249 kr.

Fler format och utgåvor

Inbunden

1 378 kr

Beskrivning

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.

Produktinformation

Utgivningsdatum:2010-10-21
Mått:155 x 235 x 30 mm
Vikt:832 g
Format:Häftad
Språk:Engelska
Serie:Springer Monographs in Mathematics
Antal sidor:536
Förlag:Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
ISBN:9783642096273

Utforska kategorier

Mer om författaren

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".

Recensioner i media

From the reviews: "This book covers ... from proof theory to a rich set of applications in areas quite distinct from mathematical logic: approximation theory and fixed point theory of nonexpansive mappings. ... Almost every chapter has a detailed ... informative final section with exercises, historical comments and references to related work. ... In summary, this book is a very welcome addition to the proof theory literature." (H. Schwichtenberg, Mathematical Reviews, Issue 2009 k)

Innehållsförteckning

Unwinding proofs (‘Proof Mining’).- Intuitionistic and classical arithmetic in all finite types.- Representation of Polish metric spaces.- Modified realizability.- Majorizability and the fan rule.- Semi-intuitionistic systems and monotone modified realizability.- Gödel’s functional (‘Dialectica’) interpretation.- Semi-intuitionistic systems and monotone functional interpretation.- Systems based on classical logic and functional interpretation.- Functional interpretation of full classical analysis.- A non-standard principle of uniform boundedness.- Elimination of monotone Skolem functions.- The Friedman A-translation.- Applications to analysis: general metatheorems I.- Case study I: Uniqueness proofs in approximation theory.- Applications to analysis: general metatheorems II.- Case study II: Applications to the fixed point theory of nonexpansive mappings.- Final comments.