Book Description

"This long awaited book ... fills essential gaps in monographic literature on proof theory and prepares readers for volume 2 (to be published soon) containing an exposition of the author's new approach to proof theory for higher order logic. Even in traditional topics, like Gödel's completeness and incompleteness theorems, and cut elemination, accents are different compared to books by Kleene, Schütte, or Takeuti, which are strongly influenced by Hilbert's aim: to make mathematical theories (number theory, analysis etc.) more reliable by transformations of formalized proofs. The author is much closer to the approach of G. Kreisel (to whom this book is dedicated): Hilbert's program needs drastic rethinking and one of the main tasks is in finding mathematical applications of the results obtained in proof theory. Possibly, it is not a pure chance that the system of second order functionals developed by the author in his normalization proof for second order logic (was rediscovered and) became a tool in computer science. The book under review presents not only this material, but also other results by the author which became a part of modern proof theory including analysis of cut-free provability in terms of 3-valued logic. The material which was not previously covered (at least in such detail) in proof-theoretic monographs includes strong normalizability proofs (after Tait and Gandy), applications of reflection principles, recursive ordinals, operations on local correct (but not necessarily well-founded) omega-derivations, no-counterexample interpretation, using proof theory to extract combinatory estimates with a detailed treatment of van der Waerden's theorem. This is a difficult, but rewarding postgraduate-level textbook. The author does not avoid philosophical questions, and such discussion supported by theorems is certainly fruitful, although the reviewer would not agree with all author's conclusions"-- description of volume 1.