Home / Tracks / Proof Theory

Proof Theory

Before Lean, before Coq, before any computer — there was natural deduction. Invented by Gerhard Gentzen in 1935, these inference rules are the universal language of proof. Every tactic in every theorem prover implements one of these rules. Learn them here in their pure form — Gentzen-style trees with horizontal bars — then recognise them everywhere.

  1. 01 →-Intro: Proving an implication easy
  2. 02 →-Elim: Modus ponens easy
  3. 03 Hypothetical syllogism (chaining) easy
  4. 04 ∧-Intro: Proving a conjunction easy
  5. 05 ∧-Elim: Taking a conjunction apart easy
  6. 06 ∨-Intro: Proving a disjunction easy
  7. 07 ∨-Elim: Proof by cases medium
  8. 08 ¬-Intro: Proving a negation medium
  9. 09 ⊥-Elim: Ex falso quodlibet medium
← All tracks Start →