Paolo Mancosu, Sergio Galvan, and Richard Zach. An Introduction to Proof Theory: Normalization, Cut-elimination, and Consistency Proofs. Oxford: Oxford University Press, 2021. DOI: 10.1093/oso/9780192895936.001.0001
Published in the UK on August 17, 2021. Available in hardcover and paperback.
An Introduction to Proof Theory provides an accessible introduction to the theory of proofs, with details worked out and many examples and exercises. It also serves as a companion to reading the original pathbreaking articles by Gerhard Gentzen. The first half covers topics in structural proof theory, including the Gödel-Gentzen translation of classical into intuitionistic logic (and arithmetic), natural deduction and the normalization theorems (for both NJ and NK), the sequent calculus, including cut-elimination and mid-sequent theorems, and various applications of these results. The second half examines Gentzen’s consistency proof for first-order Peano Arithmetic. The theory of ordinal notations and other elements of ordinal proof theory are developed from scratch. The proof methods needed, especially proof by induction, are introduced in stages throughout the text.