Proof theory — proofs as objects you can compute with and measure
Parent: logic
Treat a proof as a formal mathematical object: normalize it, run it, measure its strength.
Gentzen: natural deduction, sequent calculus, cut-elimination
Gentzen reorganized logic so proofs have structure. The cut rule = "use a lemma." His Hauptsatz (cut-elimination): every proof can be transformed into a cut-free one — no lemmas, no detours — which then has the subformula property (everything in the proof already occurs in the goal).
Cut-elimination = normalizationEliminating a cut from a proof is exactly β-reduction of the corresponding program (curry-howard). Normalizing a proof = running a program; a cut-free proof is a value.
Measuring strength: ordinal analysis
Gentzen (1936) proved PA consistent using transfinite induction up to the ordinal ε₀. That ε₀ is PA's proof-theoretic ordinal — a numeric measure of the theory's power; stronger theories have bigger ordinals. Gödel's second theorem says PA can't prove its own consistency, so the proof must climb just past PA (the ε₀-induction) — incompleteness, made quantitative in ordinals.
Reverse mathematics & extraction
- Reverse mathematics calibrates theorems by the minimal axioms they need (the "big five" subsystems of second-order arithmetic) — "which axioms is this theorem equivalent to?"
- Computational content: a normalized/cut-free proof carries a program (realizability; program extraction). A constructive proof of
∀x∃y. R(x,y)is an algorithm computingyfromx.
Why it matters here
Cut-elimination = normalization is the engine that lets Lean run proofs and extract verified code; ordinal analysis is where incompleteness becomes a measurable resource (cf. quantitative-incompleteness). Proof theory is the "dynamics" half of Curry–Howard — type theory is the "statics" half.