Part I Reflections -- Gentzen’s Consistency Proof in Context, Reinhard Kahle -- Gentzen’s Anti-Formalist Views, Michael Detlefsen -- The Use of Trustworthy Principles in a Revised Hilbert’s Program, Anton Setzer -- Part II Gentzen’s Consistency Proofs -- On Gentzen’s First Consistency Proof for Arithmetic, Wilfried Buchholz -- From Hauptsatz to Hilfssatz, Jan von Plato -- A Note on How to Extend Gentzen’s Second Consistency Proof to a Proof of Normalization for First Order Arithmetic, Dag Prawitz -- A Direct Gentzen-Style Consistency Proof for Heyting Arithmetic, Annika Siders -- Gentzen’s Original Consistency Proof and the Bar Theorem, W.W. Tait -- Goodstein’s Theorem Revisited, Michael Rathjen -- Part III Results -- Cut Elimination In Situ, Sam Buss -- Spector’s Proof of the Consistency of Analysis, Fernando Ferreira -- Climbing Mount ε_0, Herman Ruge Jervell -- Semi-Formal Calculi and Their Applications, Wolfram Pohlers -- Part IV Developments -- Proof Theory for Theories of Ordinals III: Π_N-Reflection, Toshiyasu Arai -- A Proof-Theoretic Analysis of Theories for Stratified Inductive Definitions, Gerhard Jäger and Dieter Probst -- Classifying Phase Transition Thresholds for Goodstein Sequences and Hydra Games, Frederik Meskens and Andreas Weiermann -- Non-deterministic Epsilon Substitution Method for PA and ID_1, Grigori Mints -- A Game-Theoretic Computational Interpretation of Proofs in |