Proof Theory

  • PDF / 22,359,499 Bytes
  • 309 Pages / 482 x 692 pts Page_size
  • 28 Downloads / 264 Views

DOWNLOAD

REPORT


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