• PDF / 6,272,709 Bytes
• 539 Pages / 439.37 x 666.142 pts Page_size
• 79 Downloads / 232 Views

DOWNLOAD

REPORT

---

U. Kohlenbach

Applied Proof Theory: Proof Interpretations and Their Use in Mathematics

Ulrich Kohlenbach Technische Universität Darmstadt FB Mathematik Schloßgartenstr. 7 64289 Darmstadt Germany [email protected]

ISBN 978-3-540-77532-4

e-ISBN 978-3-540-77533-1

DOI 10.1007/978-3-540-77533-1 Springer Monographs in Mathematics ISSN 1439-7382 Library of Congress Control Number: 2008920614 Mathematics Subject Classification (2000): 03F03, 03F10, 03B30, 41A10, 41A52, 47H9, 47H10 c 2008 Springer-Verlag Berlin Heidelberg  This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilm or in any other way, and storage in data banks. Duplication of this publication or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965, in its current version, and permission for use must always be obtained from Springer. Violations are liable to prosecution under the German Copyright Law. The use of general descriptive names, registered names, trademarks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. Cover design: WMXDesign GmbH, Heidelberg Printed on acid-free paper 9 8 7 6 5 4 3 2 1 springer.com

For Gabriele and Katharina

Preface

This book gives an introduction to so-called proof interpretations, more specifically various forms of realizability and functional interpretations, and their use in mathematics. Whereas earlier treatments of these techniques (e.g. [366, 266, 122, 369, 7]) emphasize foundational and logical issues the focus of this book is on applications of the methods to extract new effective information such as computable uniform bounds from given (typically ineffective) proofs. This line of research, which has its roots in G. Kreisel’s pioneering work on ‘unwinding of proofs’ from the 50’s, has in more recent years developed into a field of mathematical logic which has been called (suggested by D. Scott) ‘proof mining’. The areas where proof mining based on proof interpretations has been applied most systematically are numerical analysis and functional analysis and so the book concentrates on those. There are also some extractions of effective information from proofs (guided by logic) in number theory (G. Kreisel, H. Luckhardt, see e.g. [249, 268, 267, 122]) and algebra (G. Kreisel, C. Delzell, H. Lombardi, T. Coquand and others, see e.g. [252, 84, 77, 74, 76]). However, here mainly methods from structural proof theory such as Herbrand’s theorem, ε -substitution and cut-elimination are used and we will refer to the literature for more information on these results. In this book two kinds of systems play an important role: those with full induction and variants with induction for purely existential formulas (whose centra