Natural Deduction

Mathematical Logic · Axiom Academy

Gerhard Gentzen's elegant proof system for constructive reasoning in propositional logic Natural deduction is a proof system that formalizes logical reasoning through inference rules. Each logical connective (∧, ∨, →, ¬) has two types of rules: Introduction rules (∧-intro, ∨-intro, →-intro, ¬-intro): Tell us how to prove a statement with that connective Elimination rules (∧-elim, ∨-elim, →-elim, ¬-elim): Tell us how to use a statement with that connective 2. Conjunction Rules (∧-intro, ∧-elim) Conjunction represents "and". The rules are straightforward: ∧-Introduction: If we have proven both P and Q separately, we can conclude P ∧ Q. ∧-Elimination: From P ∧ Q, we can derive either P (left) or Q (right). 3. Implication Rules (→-intro, →-elim) Implication represents "if...then". These rules involve subproofs: →-Introduction (Conditional Proof): To prove P → Q, assume P (start a subproof), derive Q, then discharge the assumption. The implication holds because we showed "if we had P, we'd get Q". →-Elimination (Modus Ponens): From P → Q and P, we can conclude Q. This is the most fundamental inference rule. 4. Disjunction Rules (∨-intro, ∨-elim) Disjunction represents "or". Introduction is easy; elimination requires case analysis: ∨-Introduction: From P (or Q), we can conclude P ∨ Q. We can add any disjunct we want.

This is the written version of the interactive lesson above. See the full Mathematical Logic course.