Saved from the Cellar

Gerhard Gentzen is best known for his development of the proof systems of natural deduction and sequent calculus, central in many areas of logic and computer science today. Another noteworthy achievement is his resolution of the embarrassing situation created by Gödel''s incompleteness results, especially the second one about the unprovability of consistency of elementary arithmetic. After these s...