Gerhard Gentzen has been described as logic’s lost genius, whom Gödel called a better logician than himself. This work comprises articles by leading proof theorists, attesting to Gentzen’s enduring legacy to mathematical logic and beyond. The contributions range from philosophical reflections and re-evaluations of Gentzen’s original consistency proofs to the most recent developments in proof theory. Gentzen founded modern proof theory. His sequent calculus and natural deduction system beautifully explain the deep symmetries of logic. They underlie modern developments in computer science such as automated theorem proving and type theory.
Author(s): Reinhard Kahle, Michael Rathjen (eds.)
Edition: 1
Publisher: Springer
Year: 2015
Language: English
Pages: 563
Tags: Mathematical Logic and Foundations; Mathematical Logic and Formal Languages
Front Matter....Pages i-x
Front Matter....Pages 1-1
Gentzen’s Consistency Proof in Context....Pages 3-24
Gentzen’s Anti-Formalist Views....Pages 25-44
The Use of Trustworthy Principles in a Revised Hilbert’s Program....Pages 45-60
Front Matter....Pages 61-61
On Gentzen’s First Consistency Proof for Arithmetic....Pages 63-87
From Hauptsatz to Hilfssatz ....Pages 89-130
A Note on How to Extend Gentzen’s Second Consistency Proof to a Proof of Normalization for First Order Arithmetic....Pages 131-176
A Direct Gentzen-Style Consistency Proof for Heyting Arithmetic....Pages 177-211
Gentzen’s Original Consistency Proof and the Bar Theorem....Pages 213-228
Goodstein’s Theorem Revisited....Pages 229-242
Front Matter....Pages 243-243
Cut Elimination In Situ....Pages 245-277
Spector’s Proof of the Consistency of Analysis....Pages 279-300
Climbing Mount \(\varepsilon _{0}\) ....Pages 301-315
Semi-Formal Calculi and Their Applications....Pages 317-354
Front Matter....Pages 355-355
Proof Theory for Theories of Ordinals III: \(\Pi _{N}\) -Reflection....Pages 357-424
A Proof-Theoretic Analysis of Theories for Stratified Inductive Definitions....Pages 425-454
Classifying Phase Transition Thresholds for Goodstein Sequences and Hydra Games....Pages 455-478
Non-deterministic Epsilon Substitution Method for PA and ID 1 ....Pages 479-500
A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis....Pages 501-531
Well-Ordering Principles and Bar Induction....Pages 533-561
