Proof rules, proof trees, and classic derivations
Natural deduction is a proof system that mirrors how mathematicians actually reason. Each logical connective has introduction and elimination rules. To prove A → B, assume A and derive B (introduction). Given A → B and A, conclude B (elimination / modus ponens). Proofs build tree-like structures from assumptions to conclusions.
In this lesson, you will learn the proof rules, build proof trees, and walk through classic derivations step by step.
Natural deduction has a small set of rules, each tied to a connective. Introduction rules tell you how to prove a formula; elimination rules tell you how to use one. Together, they form a complete system for propositional logic.
Click any card to see a concrete example. Premises are above the line; conclusion is below.
Key insight: The introduction/elimination pattern is deeply symmetric. In type theory, this symmetry corresponds to constructors and deconstructors -- the Curry-Howard correspondence between proofs and programs.
A proof tree grows upward: the conclusion sits at the root (bottom), and each rule application adds premises as children. Assumptions appear as leaves. When a rule discharges an assumption (like →I), it is marked as used. Step through pre-built proofs to see the tree unfold.
Key insight: A proof tree with no undischarged assumptions is a proof of a theorem -- a formula true in all interpretations. Open assumptions represent hypotheses that the conclusion depends on.
Some proofs are milestones of logic. The identity proof (p → p) is the simplest non-trivial derivation. Double negation elimination (¬¬p → p) requires the classical rule of reductio ad absurdum. The law of excluded middle (p ∨ ¬p) is surprisingly tricky. Walk through each one.
Key insight: Without the rule of reductio ad absurdum (proof by contradiction), you get intuitionistic logic, where p ∨ ¬p and ¬¬p → p are not provable. The choice of rules determines which logic you are working in.