Constructive Mathematics & Type Theory
Curry-Howard correspondence: propositions as types, proofs as programs
Propositions as Types
Logic
↔
Type Theory
proposition
↔
type
proof
↔
term/program
A ∧ B
↔
A × B
A ∨ B
↔
A + B
A → B
↔
A → B
¬A
↔
A → ⊥
∀x.P(x)
↔
Πx:A.P(x)
∃x.P(x)
↔
Σx:A.P(x)
⊤ (true)
↔
Unit
⊥ (false)
↔
Empty
Typing Rules
→-Intro (abstraction):
Γ, x:A ⊢ t:B
Γ ⊢ λx.t : A→B
(→-I)
→-Elim (application):
Γ ⊢ f:A→B Γ ⊢ a:A
Γ ⊢ f a : B
(→-E / modus ponens)
×-Intro (conjunction):
Γ ⊢ a:A Γ ⊢ b:B
Γ ⊢ (a,b) : A×B
(×-I / ∧-I)
Classical vs Constructive
Classical: LEM (A ∨ ¬A) — can prove ∃ without witnessing.
Constructive: to prove ∃x.P(x) you must provide x and proof of P(x).
Live Proof Explorer
Identity
Composition
Currying
¬¬-intro
∃-witness
β-Reduction (Normalization)
Reduce
Reset
Normalization = Cut elimination
(Gentzen 1935 = Church 1936)
(λx.M) N →
β
M[N/x]
Every well-typed λ-term normalizes (strong normalization theorem). This is why type-checked proofs always terminate.