Proof theory. 2nd ed
type: Item
instance of: scholarly article
title: Proof theory. 2nd ed
zbMATH Open document ID: 0609.03019
author: Gaisi Takeuti
published in: Studies in Logic and the Foundations of Mathematics
publication date: 1987-01-01T00:00:00Z
review text: The first edition of this book (1975; Zbl 0354.02027) which appeared more than 10 years ago quickly became one of the standard sources in proof theory. One can often see in a research paper a reference to details of proofs and constructions from the book. The general structure of the book is unchanged, but some additions are made reflecting new developments in proof theory. Let us list main changes. Exposition of the completeness theorem for intuitionistic predicate calculus using Heyting algebras (and their relation to Kripke models) is added, although topoi are not mentioned at all and only a couple of lines are devoted to Girard's categorical constructions. The importance of first-order model theory is stressed by paying attention to the axiomatization of particular Heyting algebras: a lot of place is devoted to the axiomatization of the segment [0,1]. The normalisation proof for arithmetic is slightly simplified. In chapter 2 even more attention than before is devoted to provably recursive functions of arithmetic. A version of the Löb-Wainer hierarchy (in terms of Hardy functions) for \(<\epsilon_ 0\)-recursive functions is constructed using the detailed structure of fundamental sequences for ordinals \(<\epsilon_ 0\). Acquaintance with this type of results is useful both in the subsequent proof of Ketonen-Solovay bounds for Paris-Harrington's version of the Ramsey theorem independent of arithmetic and in the discussion of ordinal diagrams. Two other independence results for combinatorial statements more closely connected to ordinals are presented: Kirby-Paris theorem on Goodstein sequences [but not their Hydra game] and Friedman's version of Kruskal's theorem. This additional material is included in place of the discussion of the interpolation theorems for weak subsystems of higher order logic. In chapter 4 (end of section 23) the general completeness theorem for infinitary logic is used to formulate a proof-theoretic equivalent of Borel determinacy and state a…
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F15
Mathematics Subject Classification ID: 03-02
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03F55
Mathematics Subject Classification ID: 03B10
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03B20
zbMATH DE Number: 3985205
zbMATH Keywords: Peano arithmetic
zbMATH Keywords: infinitary logic
zbMATH Keywords: consistency
zbMATH Keywords: proof theory
zbMATH Keywords: Heyting algebras
zbMATH Keywords: provably recursive functions of arithmetic
zbMATH Keywords: fundamental sequences
zbMATH Keywords: independence results
zbMATH Keywords: Borel determinacy
zbMATH Keywords: ordinal analysis of subsystems of second-order arithmetic
zbMATH Keywords: ordinal notation
zbMATH Keywords: ordinal diagrams
reviewed by: G. E. Mints
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 3985205