Basic proof theory. 2nd ed. (English) Zbl 0957.03053

Troelstra, A. S.; Schwichtenberg, H.

Cambridge Tracts in Theoretical Computer Science. 43. Cambridge: Cambridge University Press. xii, 417 p. (2000).

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 [K. Schütte, Beweistheorie, Die Grundlehren der mathematischen Wissenschaften. 103. Berlin-Göttingen-Heidelberg: Springer-Verlag (1960; Zbl 0102.24704); 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); 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); 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); W. Pohlers, Proof theory. An introduction. Lecture Notes in Mathematics 1407. Berlin etc.: Springer-Verlag (1989; Zbl 0695.03024); 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); W. Buchholz and K. Schütte, Proof theory of impredicative subsystems of analysis. Studies in Proof Theory, Monographs, 2. Napoli: Bibliopolis (1988; Zbl 0653.03039); 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 [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 http://www.mathematik.uni-muenchen.de/~schwicht/.

Reviewer: Anton Setzer (Uppsala)

MSC:

03F03	Proof theory in general (including proof-theoretic semantics)
03-02	Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
03-01	Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations
03F52	Proof-theoretic aspects of linear logic and other substructural logics
68N17	Logic programming
03F05	Cut-elimination and normal-form theorems
03B40	Combinatory logic and lambda calculus
03G30	Categorical logic, topoi
03B45	Modal logic (including the logic of norms)
03F30	First-order arithmetic and fragments
03F35	Second- and higher-order arithmetic and fragments
03B70	Logic in computer science

Keywords:

proof theory; minimal logic; classical logic; intuitionistic logic; natural deduction system; sequent calculus; Gentzen type system; cut elimination; strong normalization; interpolation; type theory; combinatory logic; formulas-as-types relation; categorical logic; coherence theorem; linear logic; second-order Heyting arithmetic; resolution; Hilbert-style system; modal logic; first-order arithmetic; connections with computer science; logic programming; Kleene-style sequent calculus; multi-succedent intuitionistic sequent calculus; E-logic; apartness

Citations:

Zbl 0868.03014; Zbl 0102.24704; Zbl 0367.02012; Zbl 0354.02027; Zbl 0355.02023; Zbl 0609.03019; Zbl 0635.03052; Zbl 0695.03024; Zbl 0638.03052; Zbl 0653.03039; Zbl 0898.03001; Zbl 0943.68086; Zbl 0868.03024