Applied Proof Theory: Proof Interpretations and their Use in Mathematics

2008
ISBN: 978-3-540-77532-4
Verlag: Springer Berlin Heidelberg

Buch, Englisch, 536 Seiten, Format (B × H): 160 mm x 241 mm, Gewicht: 2100 g

Reihe: Springer Monographs in Mathematics

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.

Zielgruppe

Research

Autoren/Hrsg.

Kohlenbach, Ulrich

Fachgebiete

• Mathematik | Informatik Mathematik Numerik und Wissenschaftliches Rechnen Angewandte Mathematik, Mathematische Modelle
• Mathematik | Informatik Mathematik Mathematik Allgemein Mathematische Logik

Inhaltsverzeichnis

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.

Über Autor(innen)

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