Proof Theory and Intuitionistic Systems
- PDF / 15,849,818 Bytes
- 298 Pages / 504 x 720 pts Page_size
- 47 Downloads / 246 Views
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
Data Loading...
