Tableau Systems for First Order Number Theory and Certain Higher Order Theories
- PDF / 11,681,738 Bytes
- 342 Pages / 439.37 x 666.14 pts Page_size
- 32 Downloads / 208 Views
447 Sue Toledo
Tableau Systems for First Order Number Theory and Certain Higher Order Theories
Springer-Verlag Berlin· Heidelberg· New York 1975
Dr. Sue Toledo Dept. of Mathematical Statistics Columbia University in the City of New York New York, NY 10027/USA
Library or Congress Cataloging in Publication Data Toledo, Sue Ann, 1940Tablea u systems for first order number theory and
certain higher order theories.
(Lecture notes in mathematics ; 447)
Bibliography: p. Includes index.
1.
Proof theory. 2. Numbers, theory of.
3. Predicate calculus. I. Title. II. Series : Lec-
ture notes in mathematics (Berlin) ; 447. QA3.L28 no. 447 [QA9.54] 510'.8s [511'.3]
75-6738
AMS Subject Classifications (1970): 02-02, 02A05, 02B15, 02D99, 02H15 ISBN 3-540-07149-0 Springer-Verlag Berlin ·Heidelberg ·New York ISBN 0-387-07149-0 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 th e publisher, the amount of the fee to be determined by agreement with the publisher. © by Springer-Verlag Berlin · Heidelberg 1975. Printed in Germany.
Offsetdruck: Julius Beltz, Hemsbach/Bergstr.
TABLE OF CONTENTS
31
Introduction
31
Chapter I. First Order Number Theory I. The Finitary System f
31
2. A Constructive Consistency Proof for '!'
54
3. The Infini tary System st ;
'!'
as a Subsystem of
4. A Constructive Consistency Proof for
n
n
5. The Incompleteness of '!' (Missing Provable Ordinals) Chapter II. Second Order Logic
77
99 110
153
I. Two Formulations of Second Order Logic;
Translation Procedures
154
2. Second Order Models and Truth Sets
176
3. Consistency and Completeness Proofs
185
4. Logical Frameworks f or Higher Order Logic and Type Theory - The Henkin Completeness Theorem Chapter III. Other Higher Order Systems Due to Schutte
205 215
I. The System 1\ of Type-Free Logic
215
2. The System T of Ramified Type Theory
240
3. Systems of Analysis in Ramified Type Theory: r and r*
251
4. Transfinite Induction l.n r and r*
273
5. The Interpretation of Analysis
288
Appendix I. Cut Elimination in First Order Logic as Repetition Introduction
290
Appendix 2. A Translation Procedure between Tableau Systems and Schutte Systems with Positive and Negative Parts
308
Appendix 3. Applications of Gentzen's (Second) Consistency Proof to Intuitionistic Number Theory and Analysis Bibliography
322 335
INTRODUCTION Hilbert's Program.
In 1925 and 1927, in his papers "On the Infinite"
[1) and "The Foundations of Mathematics" [2), Hilbert gave a comprehensive
presentation of his ideas regarding the foundations of mathematics.
Here
he started from the point of view that for logical inference (and thus science in general) to be rel
Data Loading...
