Structural study of mathematical proofs: Hilbert program, Gentzen sequent calculus + cut-elimination, ordinal analysis (consistency-strength), Curry-Howard, type-theory, intuitionistic + linear logic.
proof-theory
Hilbert program + finitism
Hilbert 1922: prove math consistent + complete using only finitary methods. Goal: formalise math + prove no contradiction. Limited by Gödel…
Gentzen sequent calculus + cut-elimination
Gentzen 1934 LK / LJ sequent calculi for classical / intuitionistic logic. Hauptsatz: cut-elimination → consistency-proofs + decidable…
Ordinal analysis + consistency strength
Gentzen 1936 PA-consistency proof using ε_0 ordinal-induction. Modern: Π^1_1-CA0, KP, ATR_0, Bachmann-Howard, ψ-functions. Calibration of…
Curry-Howard correspondence
Curry 1958 / Howard 1969: types ≡ propositions, programs ≡ proofs, evaluation ≡ proof-normalisation. Cross-listed with L0 logic. Foundation…
Martin-Löf type theory
Martin-Löf 1972-84 intuitionistic type theory: dependent + inductive types + universe-polymorphism + identity-types. Foundation of Coq +…
Intuitionistic logic (Heyting)
Heyting 1930 formalisation of Brouwer intuitionism. Reject law-of-excluded-middle. Kripke-semantics 1965. BHK interpretation. Foundation of…
Linear logic (Girard)
Girard 1987: control of resource-use via !-modality. Tensor (⊗) vs par (℘) connectives. Coherence-spaces semantics. Foundation of…
Modal logic + Kripke frames
Kripke 1959 / 1963 possible-worlds-semantics for modal-logic ◻ / ◊. K / T / S4 / S5 systems. Bridges to L5 philosophy + computer-science…
Calculus of constructions (CoC)
Coquand-Huet 1988: dependently-typed λ-calculus extending System F + Martin-Löf. Foundation of Coq. Bridges proof-theory + type-theory +…
Proof nets (Girard / linear-logic)
Girard 1987 / Danos-Regnier 1989: graph-theoretic proofs in linear-logic without unnecessary sequential ordering. Foundation of…
Homotopy type theory + univalence (Voevodsky)
Voevodsky 2010-13 / HoTT-Book 2013. Type-theory with homotopical-interpretation. Univalence-axiom: equivalent-types are equal. Foundational…
Realisability (Kreisel-Kleene)
Kreisel 1959 / Kleene 1945. Computational-interpretation of intuitionistic-proofs. Modified-realisability / dialectica-interpretation.…
Gentzen cut-elimination theorem (Hauptsatz)
Gentzen 1934 Hauptsatz: every sequent-calculus proof reduces to cut-free form; foundation of proof-theory subformula property + automated…
Godel Dialectica translation
Godel 1958: interprets Heyting-arithmetic into computable functionals of finite type T; primitive-recursive over higher types; embedded in…
Ordinal analysis (Bachmann hierarchy)
Schutte-Bachmann ordinal-analysis: each formal theory T proves termination of recursion up to its proof-theoretic ordinal; ATR_0 ->…
Realizability (Kleene 1945)
Kleene 1945: assigns natural-number realizers to intuitionistic-arithmetic proofs; bridges constructive proof with computable function;…
Hilbert program + Godel limitation
Hilbert 1922 program: prove consistency of mathematics by finitary means; Godel 1931 second incompleteness theorem refutes finitary proof…
Veblen ordinal notation (1908)
Veblen 1908 hierarchy of normal functions phi_alpha; phi_0(x) = omega^x; foundation for representing recursive ordinals; basis of…
Hilbert program (1922)
D Hilbert 1922 + 'Grundlagen' 1928 finitary-consistency; modern modern foundational + Gödel 1931 incompleteness + 2024 ord-analysis…
Gödel incompleteness (1931)
K Gödel 1931 + 1939 incompleteness; modern modern foundational text + Rosser 1936 + 2024 ML-Lean-formalization Gödel-numbering…
Gentzen (1934)
G Gentzen 1934 cut-elimination + 1936 PA-consistency; modern modern foundational + Schütte-Feferman ordinal-analysis + 2024 ML-Lean…
Curry-Howard (1969)
H Curry 1958 + W Howard 1969 typed-λ-prop-proof; modern modern foundational + Coq + 2024 Lean-mathlib + Lean4 prove cluster-protein gen.
Schütte (1958)
K Schütte 1958 + Feferman 1968 ordinal-analysis ε_0 + Γ_0; modern modern foundational + Rathjen 2005 KPM analytic-strength inaccessible.
HoTT (Voevodsky 2013)
V Voevodsky 2009 univalence + UniMath 2013 + Lean4-mathlib 2024; modern modern foundational + 2024 cubical-CCHM constructive-univalence.