Gaisi Takeuti - Proof Theory

PROOF THEORY

SECOND EDITION

Gaisi Takeuti

Professor Emeritus of Mathematics

The University of Illinois at Urbana-Champaign

Dover Publications, Inc.
Mineola, New York

Copyright

Copyright 1975, 1987 by Gaisi Takeuti

All rights reserved.

Bibliographical Note

This Dover edition, first published in 2013, is an unabridged republication of the work originally published in 1987 by North-Holland, Amsterdam, as Volume 81 in the series Studies in Logic and the Foundations of Mathematics. The first edition was published in 1975.

Library of Congress Cataloging-in-Publication Data

Takeuti, Gaisi, 1926

Proof theory / Gaisi Takeuti. Dover edition.

pages cm. (Dover books on mathematics)

Summary: This comprehensive monograph is a cornerstone in the area of mathematical logic and related fields. Focusing on Gentzen-type proof theory, the book presents a detailed overview of creative works by the author and other 20th-century logicians that includes applications of proof theory to logic as well as other areas of mathematics. 1975 edition Provided by publisher.

Includes bibliographical references and index.

eISBN-13: 978-0-486-32067-0

1. Proof theory. I. Title.

QA9.54.T34 2013

511.36dc23

2012030734

Manufactured in the United States by Courier Corporation
49073401
www.doverpublications.com

PREFACE

This book is based on a series of lectures that I gave at the Symposium on Intuitionism and Proof Theory held at Buffalo in the summer of 1968. Lecture notes, distributed at the Buffalo symposium, were prepared with the help of Professor John Myhill and Akiko Kino. Mariko Yasugi assisted me in revising and extending the original notes. This revision was completed in the summer of 1971. At this point Jeffery Zucker read the first three chapters, made improvements, especially in .

To all who contributed, including our departmental secretaries, who typed versions of the material for use in my classes. I express my deep appreciation.

Gaisi Takeuti

Urbana, March 1975

PREFACE TO THE SECOND EDITION

In addition to the corrections of misprints and minor gaps, this edition includes the following new material.

In , I have added RasiowaSikorskis Completeness Theorem for intuitionistic predicate calculus using Heyting algebras. The relationship between Kripke semantics and Heyting valued models is discussed. In the authors opinion, the present form of the Completeness theorems for intuitionistic predicate calculus is much weaker than the counterpart for classical logic. The author believes that the investigation of stronger completeness theorems for intuitionistic logic is a very attractive new area of investigation.

In , Wainers theory on the Hardy class, KirbyParis work on Goodstein sequences, KetonenSolovayQuinseys result on ParisHar ringtons theorem and a weak form of Friedmans work on Kruskals theorem are discussed as applications of Gentzens consistency-proof.

In , I have made the material more readable and added a proof theoretic form of Borel determinacy. It is an interesting open problem to prove Borel determinacy by means of cut elimination.

In , I have simplified the accessibility proof of ordinal diagrams and included Arais improvement of my consistency-proof and cut elimination theorem using ordinal diagrams. The theory of quasi-ordinal diagrams are developed as a generalization of ordinal diagrams.

As a postscript, I have added references which are not mentioned in the course of the book.

Included as an Appendix are Kreisels article on his work, Pohlers article on the work of Schtte school, Simpsons article on reverse mathematics, and Fefermans article on his approach to proof theory. The order of these articles is the order of the date when I received the manuscripts. These articles will give the reader a good idea of many different aspects of proof theory. I am very grateful to Professors Georg Kreisel, Wolfram Pohlers, Stephen G. Simpson and Solomon Feferman for their contributions.

Many people helped me with this edition. I would especially like to mention, with my deep appreciation, Nobuyoshi Motohashi for his help on the postscript, Toshiyasu Arai for his help on and also for proof-reading, and Mitsuhiro Okada and Noriko Honda for proof-reading.

Gaisi Takeuti

Urbana, August 1986

CONTENTS

INTRODUCTION

Mathematics is a collection of proofs. This is true no matter what standpoint one assumes about mathematicsplatonism, anti-platonism, intuitionism, formalism, nominalism, etc. Therefore, in investigating mathematics, a fruitful method is to formalize the proofs of mathematics and investigate the structure of these proofs. This is what proof theory is concerned with.

Proof theory was initiated by D. Hilbert in his attempt to prove the consistency of mathematics. Hilberts approach was later developed by the brilliant work of G. Gentzen. This textbook is devoted to the proof theory inspired by Gentzens work: so-called Gentzen-type proof theory.

deals with the first order predicate calculus; Gentzens cut-elimination theorem plays a major role here. There are many consequences of this theorem as for example the various interpolation theorems.

We prove the completeness of the classical predicate calculus, by the use of reduction trees (following Schtte), and then we prove the completeness of the intuitionistic predicate calculus, by adapting this method to Kripke semantics.

deals with the theory of natural numbers; the main topics are Gdels incompleteness theorem and Gentzens consistency proof. Since the author believes that the true significance of Gentzens consistency proof has not been well understood so far, a philosophical discussion is also presented in this chapter. The author believes that the Hilbert-Gentzen finitary standpoint, with Gedankenexperimenten involving finite (and concrete) operations on (sequences of) concretely given figures, is most important in the foundations of mathematics.

for systems with heterogeneous quantifiers. Here we propose a basic system of heterogeneous quantifiers which seems reasonable and for which so-called weak completeness holds. It seems, however, that our system is far from complete. A system which is obtained from ours by a slight modification is closely related to the axiom of determinateness (AD). Therefore the problem of how to extend our system to a (sound and) complete system is related to the justification of the axiom of determinateness.

Let M be a transitive model of ZF + DC (the axiom of dependent choices) which contains P(). It has been shown that the following two statements are equivalent: (1) AD holds in M; and (2) the cut-elimination theorem holds for any M-definable determinate logic. This suggests an interesting direction for the study of infinitary languages.

is devoted to consistency proofs for stronger systems on which the author has worked.

We have tried to avoid overlapping of material with other textbooks. Thus, for example, we do not present the material in K. Schttes Beweistheorie, although much of it is Gentzen-type proof theory. Those who wish to learn other approaches to proof theory are advised to consult G. Kreisels Survey of Proof Theory I and II, Journal of Symbolic Logic (1968), and Proceedings of the Second Scandinavian Logic Symposium, ed. J. E. Fenstad (North-Holland, Amsterdam, 1971), respectively. We have made special efforts to clarify our position on foundational issues. Indeed, it is our view that in the study of the foundations of mathematics (which is not restricted to consistency problems), it is philosophically important to study and clarify the structures of mathematical proofs.

Concerning the impact of foundational studies on mathematics itself, we remark that while set theory, for example, has already contributed essentially to the development of modern mathematics, it remains to be seen what influence proof theory will have on mathematics.