Selected papers in proof theory

This collection includes papers devoted to the structural theory of proofs, which was born in the framework of Hilbert's program and is applied now in connection with various projects using the effective contents of formalized proofs. The main tool and unifying topic here is normalization, i.e. putting proofs into a normal form. The book presupposes some familiarity with the definition and elementary properties of Gentzen-type systems but little more. The first three papers introduce various normalization procedures different from popular ones. The next group deals with unwinding proofs, that is the extraction of an explicit realization from the proof of existential theorems. Normalization (or more precisely, normal form theorems) is applied to the solution of some problems in the following two papers. A separate group is formed by three papers dealing with applications of the theory of proofs to algebra, more specifically to coherence theorems in category theory. The last paper of the volume is a survey of proof theory and elementary model theory for modal logic up to the year 1974