Proof — Curry–Howard correspondence
Statement
There is a structural correspondence between formal proof systems and typed calculi: propositions correspond to types, proofs to terms (programs), implication to function types, conjunction to products, disjunction to sums, and normalization of proofs to reduction of programs. Curry observed the analogy for combinatory logic and implicational logic; Howard made the correspondence systematic for intuitionistic natural deduction and typed λ-calculus (“formulae as types”). The correspondence is a foundational bridge between logic and computation; it is not a single statement proved inside ZFC but a family of precise metatheorems (soundness, completeness, normalization) proved for each chosen logic–calculus pair.
Formula
Proofs(φ) ≃ Terms(⌜φ⌝) (up to isomorphism / equivalence)
Equation
φ → ψ ↦ (τ_φ → τ_ψ); ∧ ↦ ×; ∨ ↦ +
Proof sketch
Curry (1930s–1950s): combinatory logic and the interpretation of implicational Hilbert-style proofs. Howard (1969 manuscript, published 1980): natural deduction rules align with introduction and elimination for dependent or simple types. Extensions: de Bruijn (Automath), Girard (System F), Martin-Löf type theory, and homotopy type theory carry the same paradigm.
Source
Howard, W. A. The formulae-as-types notion of construction (1969 manuscript), in: Seldin & Hindley (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980. Curry, H. B. Foundations of Combinatory Logic, 1958; earlier papers 1930s.
Domains
mathematics, computer-science, logic