Natural Deduction

Mathematicians do not verify theorems by enumerating cases. They PROVE them. 'The sum of angles in a triangle is 180°' is proved by reasoning, not by measuring every triangle. Natural deduction is the formal version of how people actually reason.

• **Proof assistants:** Coq, Lean, and Isabelle use rules close to natural deduction to verify programs and proofs
• **Compilers:** the type system is a logic where types = propositions and programs = proofs (the Curry-Howard correspondence)
• **Law:** courtroom arguments are chains of inferences: facts → application of the law → conclusion

Natural deduction

**Natural deduction** is a system of formal proofs that mirrors human reasoning. Unlike truth tables (which check every case), here we **construct the proof** step by step, applying inference rules.

**Gerhard Gentzen** (1934) created natural deduction as a formalization of mathematical reasoning. Every logical connective has two rules: **introduction** (how to obtain it) and **elimination** (how to use it).

A proof starts from **premises** (given) and ends with a **conclusion**. Along the way we can make **assumptions** (temporary hypotheses), later 'discharged' by the introduction rules for implication or negation.

Introduction rules

**Introduction rules** tell you how to **obtain** a formula with a given connective. To introduce a conjunction A ∧ B you need both A and B. To introduce a disjunction A ∨ B you need either A or B.

**Implication introduction (→I):** to prove A → B, assume A and derive B. Then discharge the assumption and conclude A → B. This corresponds to: 'If A were true, then B would be true'.

**Key idea of →I:** we are not claiming A is true. We are saying 'IF A were true, THEN B would be true'. An assumption is a hypothetical world we explore and then leave.

Elimination rules

**Elimination rules** tell you how to **use** a formula with a given connective. Modus ponens (→E) is the most important: from A → B and A you get B. From a conjunction A ∧ B you can extract either A or B.

**Disjunction elimination (∨E)** is the hardest rule. Given A ∨ B, you do not know which side is true. So you handle both cases: assume A and derive C; assume B and derive C. Then C follows in any case.

**Ex falso quodlibet** (from falsehood, anything follows): once you have a contradiction (⊥), you may derive any formula. This is not a bug but a feature. Inconsistent premises make the system useless, and the rule encodes exactly that.

Proof strategy

**Goal-directed strategy:** look at the conclusion and ask 'Which introduction rule produces this formula?' If the goal is A → B, assume A and prove B. If the goal is A ∧ B, prove A and B separately.

**Heuristics:** 1) Start by introducing the main connective of the goal. 2) Use every premise. They were given for a reason. 3) If A ∨ B appears among the premises, do case analysis. 4) When stuck, try proof by contradiction.

**Checking a proof:** every line must be either a premise, an assumption, or derived by a rule from earlier lines. All assumptions must be discharged by the end. You cannot reference a discharged assumption.

Key Ideas

• **Introduction** is how to obtain a formula with a given connective (∧I, ∨I, →I, ¬I)
• **Elimination** is how to use a formula with a given connective (∧E, ∨E, →E, ¬E)
• **Assumptions** are hypothetical worlds that must be discharged
• **Goal-directed strategy:** look at the main connective of the conclusion
• **Ex falso:** from a contradiction, anything follows

Related Topics

Natural deduction is the backbone of formal proofs:

• Proof by contradiction — A special technique using ¬I
• Implication — →I and →E are the key rules for working with implication
• Modus ponens — →E is the formalization of modus ponens

Вопросы для размышления

• Why is disjunction elimination (∨E) harder than the other rules?
• How would you explain ex falso quodlibet intuitively?
• If you were designing a programming language, how would types correspond to logical connectives?

Связанные уроки

• comp-18-type-checking
• ml-03