Proof Theory and Intuitionistic Systems

  • PDF / 15,849,818 Bytes
  • 298 Pages / 504 x 720 pts Page_size
  • 47 Downloads / 245 Views

DOWNLOAD

REPORT


212 Bruno Scarpellini Universitat Basel, Basel/Schweiz

Proof Theory and Intuitionistic Systems

Springer-Verlag Berlin· Heidelberg· NewYork 1971

AMS Subject Classifications (1970): Primary: 02D 99, 02E 05. Secondary: 02C 15

ISBN 3-540-05541-X Springer-Verlag Berlin' Heidelberg· New York ISBN 0-387-05541-X Springer-Verlag New York· Heidelberg· Berlin

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 1971. Library of Congress Catalog Card Number 78-169705. Printed in Germany.

Offsetdruck:Julius Beltz, Hemsbach IBergstr.

PREFACE

The aim of this monograph is to show

that the methods used by Gent-

zen in his second consistency proof for number theory can be extended and used in order to exhibit properties of mathematical interest of certain intuitionistic systems of analysis. The monograph has its root in a paper

[8]

in which familiar properties of number theory

have been derived with the aid of Gentzen methods. An outline of the material contained in chapter IV has been presented at the Buffalo conference on intuitionism and proof theory

(1968) [9J '

while other

parts have been discussed in seminaries on mathematical logic at the university of Basel. A detailed introduction, containing a review of the content of the monograph,

is given at the beginning of chapter I.

The author would like to express his gratitude to the Swiss national foundations whose financial support made this work possible. Thanks are also due to the Freiweillige Akademische Gesellschaft Basel which supplied the major part of the typing costs.

CONTENTS

CHAPTER I: Introduction and preliminaries 1.1.

Introductory remarks •

1.2.

Preliminaries and notation

1

5

1. 3.

Languages, Syntax

10

1. 4.

Some basic systems

16

1. 5.

Some systems of analysis

25

CHAPTER II: A review of

second consistency proof

34

2.1.

Some preliminary notions

2.2.

The reduction steps

39

2.3.

Properties of reduction steps

48

2.4.

Assignement of ordinals to proofs

50

2.5.

A generalization.

53

CHAPTER III: The intuitionistic system of number theory 3.1.

Elimination of forks in intuitionistic proofs

70

3.2.

A basic lemma

74

CHAPTER IV: A formally intuitionistic system as strong as classical analysis 4.1.

A conservative extension of

4.2.

Reduction steps

4.3. 4.4. 4.5. 4.6.

ZT/II

N

91 . 94

Ordinals The system

ZTEi/II

Applications • The system

79 • 85

N

.105

ZTi/II

and its conservative extension

.121

ZTEi/II . Some remarks on the proof theoretic treatment of ZTEi/II

N

and

ZTEi/II.

.133

VI CHAPTER V: Transfinite induction with respect to recursive we