Proof theory. 2nd ed (Q1086559)

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 problem: to give a new proof of this result of Martin by proving a corresponding cut elimination theorem. One of the main contributions of the author was the ordinal analysis of subsystems of second-order arithmetic by means of special systems of ordinal notation which the author introduced and called ordinal diagrams (o.d.). The proof of well-foundedness for o.d. is complicated both combinatorially and in proof-theoretic respect. In this edition this proof is changed. The schema of ordinal analysis is also changed: instead of normalising derivations of existential theorems in subsystems of second-order arithmetic, derivations of arbitrary theorems in the corresponding system of second-order logic are now normalised, and then the translation of arithmetic into logic is used. This makes the proof more elegant, but to obtain the best possible ordinal estimate the author has to use the more involved treatment due to Arai dealing with arithmetic systems. Ordinal diagrams turn out to be convenient for the treatment of the generalised Kruskal's theorem introduced by Friedman including the proof of its independence from a system of \(\Pi^ 1_ 1\)- analysis. An unusual feature is the appendix (about 100 pages) consisting of contributions of four authors (\textit{G. Kreisel}, \textit{W. Pohlers}, \textit{S. G. Simpson} and \textit{S. Feferman}) reflecting their view of proof theory and partially compensating for the author's reluctance to investigate connections of some of his notions (especially ordinal diagrams) with the notions used by other authors. The appendices help the reader to form an even more complete picture of the modern state of proof theory. The 11-page postscript by the author lists some references used in the text and provides information on further developments. This book is a very useful addition to the literature on proof theory.