The structure of proof itself. Natural deduction, the sequent calculus, and the cut-elimination theorem (Hauptsatz) are rigorous and foundational — the basis of modern proof theory, automated reasoning, and proof assistants.
Around Gödel, not over him. Gentzen proved arithmetic consistent — but only by using transfinite induction up to ε₀, a principle outside arithmetic. It doesn't evade Gödel; it measures exactly how much extra strength a consistency proof costs.
Named without flinching. Gentzen joined the Nazi party and the SA, and benefited from the regime that expelled his Jewish colleagues. He died in 1945 in a Soviet-controlled Czech prison camp at 35. The logic is his; so is the record.
Natural deduction proves a goal by applying rules that each introduce or eliminate a connective. Here is a real derivation engine: pick a theorem, then apply the available rules in order to construct the proof. Each step is checked — a rule only fires when its inputs are already on the page — and the line that reaches the goal lights up. Watch a proof grow the way a mathematician would actually grow it.
A → B you assume A, derive B, then discharge the assumption (→-introduction); to use A → B together with A you get B (→-elimination, which is modus ponens, [[chrysippus]]' first rule). Every connective, two rules, perfectly balanced. ⚑ This balance is why proofs normalize — and why, under Curry–Howard, a proof of A → B is exactly a function taking evidence of A to evidence of B. A proof is a program."I wished to set up a formalism that comes as close as possible to actual reasoning." — Gerhard Gentzen, 1934
Any proof using a "cut" (an intermediate lemma) can be rewritten into one that doesn't — a direct, lemma-free proof. Proofs can always be normalized; from this, consistency and the subformula property follow.
Introduction/elimination rules match exactly the way you build and use data. A proof of A→B is a function; normalizing a proof is running a program. Logic and computation, the same thing.
Gentzen's cut-elimination is one of the most consequential theorems in logic: it says proof has a direct form, and that detours (lemmas) can always be removed. Decades later this became the deepest bridge in the field — the Curry–Howard correspondence — where a proposition is a type, a proof is a program of that type, and simplifying the proof is executing the program. The proof assistants that today verify the correctness of compilers, cryptography, and aircraft software ([[bertrand-russell]]'s types made to work) run on Gentzen's natural deduction directly. He also used his methods to prove the consistency of arithmetic — not in defiance of [[kurt-godel]], but by climbing into transfinite induction up to the ordinal ε₀, pinning down the exact "proof-theoretic strength" the job requires.
Gate kept on. The mathematics is first-rank and permanent: natural deduction and the sequent calculus are how logic is taught and how proof assistants are built; cut-elimination is a deep structural theorem; and his consistency proof for arithmetic (1936) is honestly not a loophole around Gödel — it uses transfinite induction up to ε₀, a resource stronger than arithmetic itself, and its real content is to measure exactly how much strength consistency costs (founding ordinal proof theory). On the biography, the record is dark and is stated without softening: Gerhard Gentzen joined the Nazi party (NSDAP) and the SA, signed the loyalty declarations of the regime, and continued his career within institutions from which his Jewish teachers and colleagues — including those who had shaped his field — were being expelled and worse. After the war, he was arrested in Prague and died in a Soviet-administered internment camp in 1945, at 35, of malnutrition. The work belongs in this lineage on its merits; the man's complicity belongs in the record beside it. Holding both is the whole point of keeping the gate on: the logic does not absolve the life, and the life does not erase the logic. ⚑ [[stephen-kleene]] ← · next → Saul Kripke.