# zbMATH — the first resource for mathematics

##### Examples
 Geometry Search for the term Geometry in any field. Queries are case-independent. Funct* Wildcard queries are specified by * (e.g. functions, functorial, etc.). Otherwise the search is exact. "Topological group" Phrases (multi-words) should be set in "straight quotation marks". au: Bourbaki & ti: Algebra Search for author and title. The and-operator & is default and can be omitted. Chebyshev | Tschebyscheff The or-operator | allows to search for Chebyshev or Tschebyscheff. "Quasi* map*" py: 1989 The resulting documents have publication year 1989. so: Eur* J* Mat* Soc* cc: 14 Search for publications in a particular source with a Mathematics Subject Classification code (cc) in 14. "Partial diff* eq*" ! elliptic The not-operator ! eliminates all results containing the word elliptic. dt: b & au: Hilbert The document type is set to books; alternatively: j for journal articles, a for book articles. py: 2000-2015 cc: (94A | 11T) Number ranges are accepted. Terms can be grouped within (parentheses). la: chinese Find documents in a given language. ISO 639-1 language codes can also be used.

##### Operators
 a & b logic and a | b logic or !ab logic not abc* right wildcard "ab c" phrase (ab c) parentheses
##### Fields
 any anywhere an internal document identifier au author, editor ai internal author identifier ti title la language so source ab review, abstract py publication year rv reviewer cc MSC code ut uncontrolled term dt document type (j: journal article; b: book; a: book article)
Proof theory. 2nd ed. (English) Zbl 0609.03019
Studies in Logic and the Foundations of Mathematics, Vol. 81. Amsterdam etc.: North-Holland. X, 490 p. {$} 90.00; Dfl. 250.00 (1987). 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\sb 0$-recursive functions is constructed using the detailed structure of fundamental sequences for ordinals$<\epsilon\sb 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\sp 1\sb 1\$- analysis. An unusual feature is the appendix (about 100 pages) consisting of contributions of four authors ({\it G. Kreisel}, {\it W. Pohlers}, {\it S. G. Simpson} and {\it 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.
Reviewer: G.Mints

##### MSC:
 03F05 Cut-elimination; normal-form theorems 03F15 Recursive ordinals; ordinal notations 03-02 Research monographs (mathematical logic) 03F35 Second- and higher-order arithmetic and fragments 03F30 First-order arithmetic and fragments 03F55 Intuitionistic mathematics 03B10 First-order logic 03B15 Higher-order logic; type theory 03B20 Subsystems of classical logic