No label defined (Q4499084)

The book under review is the second edition of this almost encyclopaedic monograph on proof theory [for a review of the first edition (ibid. 1996) see Zbl 0868.03024], which was thoroughly revised and slightly extended. It treats structural proof theory in depth, and everybody interested in this subject should study it. However one should be aware that the authors chose deliberately to take only a first glimpse at mathematical proof theory (proof theory of axiom systems for formalizing fragments of mathematics), and that the reader interested in this topic should refer to standard text books on proof theory [\textit{K. Schütte}, Beweistheorie, Die Grundlehren der mathematischen Wissenschaften. 103. Berlin-Göttingen-Heidelberg: Springer-Verlag (1960; Zbl 0102.24704); \textit{K. Schütte}, Proof theory. Translation from the German by J. N. Crossley, Grundlehren der mathematischen Wissenschaften. 225. Berlin-Heidelberg-New York: Springer-Verlag (1977; Zbl 0367.02012); \textit{G. Takeuti}, Proof theory, Studies in Logic and the Foundations of Mathematics. 81. Amsterdam-Oxford: North-Holland Publishing Company; New York: American Elsevier Publishing Company, Inc. (1975; Zbl 0354.02027 and Zbl 0355.02023); Second edition: ibid., Amsterdam etc.: North-Holland Publishing Co. (1987; Zbl 0609.03019); \textit{J.-Y. Girard}, Proof theory and logical complexity. Volume I. Studies in Proof Theory. Monographs 1. Napoli: Bibliopolis. Edizioni di Filosofia e Scienze (1987; Zbl 0635.03052); \textit{W. Pohlers}, Proof theory. An introduction. Lecture Notes in Mathematics 1407. Berlin etc.: Springer-Verlag (1989; Zbl 0695.03024); \textit{G. Jaeger}, Theories for admissible sets. A unifying approach to proof theory. Studies in Proof Theory. Lecture Notes, 2. Napoli: Bibliopolis (1986; Zbl 0638.03052); \textit{W. Buchholz} and \textit{K. Schütte}, Proof theory of impredicative subsystems of analysis. Studies in Proof Theory, Monographs, 2. Napoli: Bibliopolis (1988; Zbl 0653.03039); \textit{S. R. Buss} (ed.), Handbook of proof theory. Studies in Logic and the Foundations of Mathematics. 137. Amsterdam: Elsevier (1998; Zbl 0898.03001)]. Apart from corrections of some unfortunate typos in the first edition -- it is recommended to use the second edition instead of the first one -- the following modifications have been carried out: in the overview 1.3 of the three types of formalisms (natural deduction, sequent calculus and Hilbert systems), natural deduction is now motivated via the BHK-interpretation and the sequent calculus is introduced as a way of constructing natural deduction derivations. This is helpful for the reader new to the subject. A chapter (2.1.10) on the representation of the complete discharge convention (CDC) in natural deduction with sequents has been added. The section on Kleene-style sequent calculus (3.5.11) has been extended and multi-succedent versions of the intuitionistic sequent calculus (3.5.10) together with a sketch of cut-elimination (4.1.10) have been added. A new section (3.4) with a general treatment of deduction systems with local rules has been introduced. The proof of the cut elimination theorem (4.1.5) has been revised (there are some tiny but misleading typos in this section, see the list of corrections mentioned below). Cut elimination results for extensions of the sequent calculus by rules (4.6), equality (4.7) and apartness (4.8) have been added. A result on the growth of size of proofs in propositional logic under cut elimination (5.2) has been included. Extensions of natural deduction systems with extra rules (6.4) are now treated and the section on E-logic (6.5) has been revised. The proof of strong normalization of system F (\(\lambda 2\)) makes now use of simplified techniques taken from [\textit{R. Matthes}, Extensions of system F by iteration and primitive recursion on monotone inductive types. München: Utz Verlag. München: LMU, Univ. München, Fakultät Mathematik/Informatik (1998; Zbl 0943.68086)]. Solutions to selected exercises have been added. A small criticism of the book might be that by treating sequents as multisets of formulas instead of sets, proofs become more involved, and therefore the reader might get the impression that cut elimination for the predicate calculus is more difficult than it really is. Further, the variety of systems (esp. G1--G3 and GK) might be more irritating rather than helpful. In order to see the simplicity of concepts, it would as well have been nice to mention the almost trivial proof of cut elimination for the (classical) Tait calculus, which is unfortunately called Gentzen-Schütte system in this book. In a book of such length almost inevitably some typos occur. A list of corrections is available from \url{http://www.mathematik.uni-muenchen.de/~schwicht/}.