zbMATH — the first resource for mathematics

Basic proof theory. (English) Zbl 0868.03024
Cambridge Tracts in Theoretical Computer Science. 43. Cambridge: Cambridge University Press. xi, 343 p. (1996).
This monograph is not simply a further book on proof theory. The title is perhaps a bit misleading. The book does not convey neither the elements nor the basis of proof theory. It is no primer on proof theory and does not present the foundations of proof theory. According to the preface, the authors intend to fill a gap between introductory books on proof theory and textbooks on mathematical logic on one hand and advanced monographs on the other. But they present much more.
Of course, in the beginning six chapters, different formalisations are given for the standard logics, i.e. minimal logic, intuitionistic and classical logic, each as natural deduction system, Hilbert style and Gentzen type system. The equivalence of these systems, cut elimination, normalisation and moreover interpolation are shown. Positive and negative contexts as well as multisets are introduced. Simple type theory, combinatory logic and the formulas-as-types relation are presented. The nomenclature of the systems reveals the first author. In Chapter 7 the proof theoretical foundations of logic programming are treated. This shows the connections between proof theory and computer science. Chapter 8 is devoted to the relations between proof theory and categorical logic and culminates in the coherence theorem of Mints. In Chapter 9, proof theoretical aspects of modal and linear logic are outlined. This chapter as well as Chapter 7 is of special interest for computer scientists. Finally the last two chapters present classical (not in contrast to intuitionistic) proof theory of arithmetic and of second order Heyting arithmetic. Also the connection of the latter theory to computer science is described: From the proof of the totality of a number theoretic function \(f\), conceived as a term of \(\lambda 2\) (a \(\lambda\)-calculus with abstraction on type variables), an algorithm for computing the function \(f\) can be picked out.
This textbook on proof theory does not make another one superfluous and is not redundant because of others. The notes at the end of each chapter contain valuable connections of the topic of the chapter to other fields, historical and bibliographical remarks.

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
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