Proof Theory
- PDF / 22,359,499 Bytes
- 309 Pages / 482 x 692 pts Page_size
- 28 Downloads / 310 Views
Editors S. S. Chern J. L. Doob J. Douglas, jr. A. Grothendieck E. Heinz F. Hirzebruch E. Hopf S. Mac Lane W. Magnus M. M. Postnikov W. Schmidt D. S. Scott K. Stein J. Tits B. L. van der Waerden Managing Editors B. Eckmann J. K. Moser
Kurt Schutte
Proof Theory Translation from the German by J. N. Crossley
Springer-Verlag Berlin Heidelberg New York 1977
Kurt Schutte Mathematisches Institut, Ludwig-Maximilians-Universitat, 8000 Munchen 2/Germany
Translator:
J. N. Crossley Department of Mathematics, Monash University, Clayton, Victoria 3168/Australia
Translation of the revised version of "Beweistheorie", 1st edition, 1960; Grundlehren der mathematischen Wissenschaften, Band 103
AMS Subject Classification (1970): 02B 10, 02B99, 02C 15, 02Dxx, 02E99, ION99
ISBN-13: 978-3-642-66475-5 DOl: 10.1007/978-3-642-66473-1
e-ISBN-13: 978-3-642-66473-1
Library of Congress Cataloging in Publication Data. Schutte, KUTt. Proof theory. (Grundlehren def mathematischen Wissenschaften; 225). Translation of Beweistheorie. Bibliography: p. Includes index. I. Proof theory. I. Title. II. Series: Die Grundlehren dec mathematischen Wissenschaften in Einzeldarstellungen; 225. QA9.54.S3813. 511'.3. 76-45768. This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically those of translation. reprinting, re-use of illustrations, broadcasting, reproduction by photocopying machine or similar means, and storage in data banks. Under §54 of the German Copyright Law where copies are made for other than private use, a fee is payable to the publisher, the amount of the fee to be determined by agreement with the publisher.
©
by Springer-Verlag Berlin Heidelberg 1977. Softcover reprint of the hardcover 1st edition 1977
2141/314()-543210
Preface
This book was originally intended to be the second edition of the book "Beweistheorie" (Grundlehren der mathematischen Wissenschaften, Band 103, Springer 1960), but in fact has been completely rewritten. As well as classical predicate logic we also treat intuitionistic predicate logic. The sentential calculus properties of classical formal and semiformal systems are treated using positive and negative parts of formulas as in the book "Beweistheorie". In a similar way we use right and left parts of formulas for intuitionistic predicate logic. We introduce the theory of functionals of finite types in order to present the Gi:idel interpretation of pure number theory. Instead of ramified type theory, type-free logic and the associated formalization of parts of analysis which we treated in the book "Beweistheorie", we have developed simple classical type theory and predicative analysis in a systematic way. Finally we have given consistency proofs for systems of lI~-analysis following the work of G. Takeuti. In order to do this we have introduced a constni'ctive system of notation for ordinals which goes far beyond the notation system in "Beweistheorie". My hearty thanks are due to Professor J. N. Crossley for his translation of my German