Proof Theory An Introduction

Although this is an introductory text on proof theory, most of its contents is not found in a unified form elsewhere in the literature, except at a very advanced level. The heart of the book is the ordinal analysis of axiom systems, with particular emphas

  • PDF / 9,830,506 Bytes
  • 220 Pages / 439.32 x 666.12 pts Page_size
  • 63 Downloads / 296 Views

DOWNLOAD

REPORT


1407

Wolfram Pohlers

Proof Theory An Introduction

Springer-Verlag Berlin Heidelberg NewYork London Paris Tokyo Hong Kong Barcelona

Budapest

Author Wolfram Pohlers Institut fur Mathematische Logik und Grundlagenforschung WestfaIische Wilhelms-Universitat Einsteinstr. 62, D-48148 Munster, Gennany

1st edition 1989 2nd printing 1994

Mathematics Subject Classification (1980): 03F

ISBN 3-540-51842-8 Springer-Verlag Berlin Heidelberg New York ISBN 0-387-51842-8 Springer-Verlag New York 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, re-use of illustrations, recitation, broadcasting, reproduction on microfilms or in any other way, and storage in data banks. Duplication of this publication or parts thereof is pennined only under the provisions of the Gennan Copyright Law of September 9, 1965, in its current version, and pennission for use must always be obtained from Springer-Verlag. Violations are liable for prosecution under the Gennan Copyright Law. Springer-Verlag Berlin Heidelberg New York a member of BertelsmannSpringerScience+Business Media GmbH

© Springer-Verlag Berlin Heidelberg 1989 Printed in Gennany 46/3111-543'

- Printed on acid-free paper

This book contaiDs the somewhat extended lecture Dotes of an introductory course in proof theory ) gave duriDg the Winter term 1987/88 at the University of MUnster, FRG. The decision to publish these notes in the Springer series has grown out of the demand for an introductory text on proof theory. The booles by LSchiitte and G.Talceuti are commonly considered to be qUite advanced and J.Y.Girard·s brilliant book also. is too broad to serve as an introduction.

J tried, therefore. to write a boole: which needs no preVious knowledge of proof theory at all and only little knowledge in logic. This is of course impossible, so the boole runs on two levels - a very basic one, at which the book is self-coD~ and a more advanced one (chiefly in the exercises) With some cross-references to defiDability theory. The beginner in logic should neglect

these cross-references. In the· presentation I have tried Dot to use the 'cabal language' of proof theory but a language familiar to students in mathematical logic.

Since proof theory is a very inhomogeneous area of mathematical logic, a choice had to been made about the parts to be presented here. I have decided to opt for what I consider to be the heart of proof theory - the ordiDal aDa1ysis of axiom systems. Emphasis is given to the ordiDal analysis of the axiom system of the impredicative theory of elementary inductive definitions OD the Datura) numbers. A rough sketch of the 'constructive' consequences of ordiDal aDa1ysLs is given in the epilogue. Many people helped me to write this book. i.Columbus suggested and checked nearly all the exercises. A.WeiermalUl made a lot of valuable suggestioDS especially .in the section about alternative interpretations for Q. A.Scbliiter did the proof-rea