Type Theory Explorer

Propositions-as-types (Curry-Howard): proofs are programs, types are propositions

Proof Mode

Proof Tree

Inference Rules

Curry-Howard Correspondence

LogicType Theory
Proposition AType A
Proof of ATerm : A
A ∧ BA × B (product)
A ∨ BA + B (sum)
A → BA → B (function)
¬AA → ⊥
∀x.P(x)Π(x:A).B(x)
∃x.P(x)Σ(x:A).B(x)
⊤ (True)Unit type
⊥ (False)Empty type

Famous Results

Identity: λx.x : A → A

Composition:
λf.λg.λx.f(g x) : (B→C)→(A→B)→A→C

Swap: λp.(π₂p, π₁p) : A×B → B×A

S combinator:
λx.λy.λz.xz(yz) proves
(A→B→C)→(A→B)→A→C