This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply them elsewhere in much (...) more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included. (shrink)

We introduce the notion of an alphabetic trace of a cut-free intuitionistic prepositional proof and show that it serves to characterize the equality of arrows in cartesian closed categories. We also show that alphabetic traces improve on the notion of the generality of proofs proposed in the literature. The main theorem of the paper yields a new and considerably simpler solution of the coherence problem for cartesian closed categories than those in [11, 14].

Provability, Computability and Reflection.

It is proved that equations between arrows assumed for cartesian categories are maximal in the sense that extending them with any new equation in the language of free cartesian categories collapses a cartesian category into a preorder. An analogous result holds for categories with binary products, which may lack a terminal object. The proof is based on a coherence result for cartesian categories, which is related to model-theoretic methods of normalization. This maximality of cartesian categories, which is analogous to Post (...) completeness, shows that the usual equivalence between deductions in conjunctive logic induced by βη normalization in natural deduction is chosen optimally. (shrink)