Introduction
Natural deduction is a proof system designed to mirror the way mathematicians naturally construct proofs. Unlike resolution, which uses a single inference rule, natural deduction provides multiple inference rules—one for introducing each logical connective and one for eliminating it. This approach is more intuitive and closer to human mathematical reasoning.
This article explores natural deduction systems, proof construction, and applications in formal verification.
Historical Context
Natural deduction was developed independently by Gerhard Gentzen and Stanisław Jaśkowski in the 1930s. Gentzen’s formulation, with introduction and elimination rules for each connective, became the standard. Natural deduction has become the preferred proof system in logic courses and proof assistants like Coq and Isabelle, because it closely mirrors human reasoning.
Core Principles
Introduction and Elimination Rules
Principle: For each logical connective, there are two types of rules:
- Introduction Rule: How to prove a formula with that connective
- Elimination Rule: How to use a formula with that connective
Example: For conjunction (∧)
- Introduction: From P and Q, infer P ∧ Q
- Elimination: From P ∧ Q, infer P (or Q)
Proof Structure
Proof: A tree of inferences with:
- Leaves: Assumptions or axioms
- Internal nodes: Inferences
- Root: The conclusion
Assumption Discharge: Assumptions can be discharged (removed) by introduction rules
Propositional Natural Deduction
Conjunction (∧)
Introduction (∧I):
P Q
──────
P ∧ Q
From P and Q, infer P ∧ Q
Elimination (∧E):
P ∧ Q P ∧ Q
───── or ─────
P Q
From P ∧ Q, infer P or Q
Disjunction (∨)
Introduction (∨I):
P Q
───── or ─────
P ∨ Q P ∨ Q
From P, infer P ∨ Q (or from Q)
Elimination (∨E):
P ∨ Q [P] [Q]
⋮ ⋮
R R
─────────────────────
R
From P ∨ Q, if both P and Q lead to R, infer R
Implication (→)
Introduction (→I):
[P]
⋮
Q
─────
P → Q
Assume P; if we can derive Q, then infer P → Q (discharge assumption)
Elimination (→E, Modus Ponens):
P → Q P
─────────
Q
From P → Q and P, infer Q
Negation (¬)
Introduction (¬I):
[P]
⋮
⊥
─────
¬P
Assume P; if we derive contradiction, infer ¬P (discharge assumption)
Elimination (¬E):
¬P P
───────
⊥
From ¬P and P, infer contradiction
Contradiction (⊥)
Elimination (⊥E):
⊥
───
P
From contradiction, infer anything (ex falso quodlibet)
First-Order Natural Deduction
Universal Quantification (∀)
Introduction (∀I):
[x]
⋮
P(x)
─────
∀x P(x)
If P(x) holds for arbitrary x, infer ∀x P(x)
Restriction: x must not appear free in any undischarged assumption
Elimination (∀E):
∀x P(x)
───────
P(a)
From ∀x P(x), infer P(a) for any term a
Existential Quantification (∃)
Introduction (∃I):
P(a)
─────
∃x P(x)
From P(a), infer ∃x P(x)
Elimination (∃E):
∃x P(x) [P(x)]
⋮
Q
─────────────────
Q
From ∃x P(x), if P(x) leads to Q (for arbitrary x), infer Q
Restriction: x must not appear free in Q or undischarged assumptions
Proof Examples
Example 1: Modus Ponens
Goal: Prove Q from {P → Q, P}
Proof:
1. P → Q (assumption)
2. P (assumption)
3. Q (→E, 1, 2)
Example 2: Hypothetical Syllogism
Goal: Prove P → R from {P → Q, Q → R}
Proof:
1. P → Q (assumption)
2. Q → R (assumption)
3. [P] (assumption for →I)
4. Q (→E, 1, 3)
5. R (→E, 2, 4)
6. P → R (→I, 3-5, discharge P)
Example 3: Proof by Contradiction
Goal: Prove P from {¬¬P}
Proof:
1. ¬¬P (assumption)
2. [¬P] (assumption for ¬I)
3. ⊥ (¬E, 1, 2)
4. P (⊥E, 3)
5. ¬¬P → P (→I, 1-4)
Example 4: First-Order Logic
Goal: Prove ∃x Q(x) from {∀x(P(x) → Q(x)), ∃x P(x)}
Proof:
1. ∀x(P(x) → Q(x)) (assumption)
2. ∃x P(x) (assumption)
3. [P(a)] (assumption for ∃E)
4. P(a) → Q(a) (∀E, 1)
5. Q(a) (→E, 4, 3)
6. ∃x Q(x) (∃I, 5)
7. ∃x Q(x) (∃E, 2, 3-6)
Proof Strategies
Forward Reasoning
Strategy: Start with assumptions, derive new facts
Advantages: Intuitive, follows logical flow Disadvantage: May explore irrelevant paths
Backward Reasoning
Strategy: Start with goal, work backward to assumptions
Advantages: Focused on goal, avoids irrelevant facts Disadvantage: Requires knowing what to assume
Mixed Strategy
Strategy: Combine forward and backward reasoning
Advantages: Efficient, flexible Disadvantage: Requires skill to balance
Normalization and Cut Elimination
Normal Form
Definition: A proof is in normal form if:
- No introduction rule is immediately followed by elimination of the same connective
- No detours through unnecessary steps
Example of Detour:
P ∧ Q
───── (∧E)
P
───── (∧I with Q)
P ∧ Q
Cut Elimination
Cut: An inference that introduces and immediately eliminates a formula
Normalization: Process of removing cuts
Significance: Normalized proofs are more direct and often shorter
Comparison with Other Systems
Natural Deduction vs Resolution
| Aspect | Natural Deduction | Resolution |
|---|---|---|
| Inference Rules | Multiple (one per connective) | Single rule |
| Proof Structure | Tree | Linear sequence |
| Intuitiveness | High | Low |
| Automation | Harder | Easier |
| Proof Length | Often shorter | Often longer |
Natural Deduction vs Sequent Calculus
| Aspect | Natural Deduction | Sequent Calculus |
|---|---|---|
| Assumptions | Explicit in proof | In sequent |
| Discharge | Explicit | Implicit |
| Symmetry | Asymmetric | Symmetric |
| Automation | Moderate | Better |
Applications
Proof Assistants
Coq: Uses natural deduction-like tactics Isabelle: Supports natural deduction proofs Lean: Modern proof assistant with natural deduction
Mathematical Proofs
Textbooks: Natural deduction mirrors textbook proofs Education: Teaches logical reasoning naturally Verification: Formal verification of mathematics
Logic Programming
Prolog: Uses SLD resolution (related to natural deduction) Datalog: Logic programming with natural deduction
Glossary
Assumption: A formula assumed to be true (can be discharged)
Discharge: Remove an assumption from a proof
Elimination Rule: How to use a formula with a connective
Introduction Rule: How to prove a formula with a connective
Normal Form: Proof without detours or cuts
Proof Tree: Tree structure representing a proof
Sequent: Expression Γ ⊢ Δ (from Γ, derive Δ)
Tactic: A proof strategy in proof assistants
Practice Problems
Problem 1: Prove P ∧ Q from {P, Q} using natural deduction.
Solution:
1. P (assumption)
2. Q (assumption)
3. P ∧ Q (∧I, 1, 2)
Problem 2: Prove (P → Q) → (¬Q → ¬P) using natural deduction.
Solution:
1. [P → Q] (assumption for →I)
2. [¬Q] (assumption for →I)
3. [P] (assumption for ¬I)
4. Q (→E, 1, 3)
5. ⊥ (¬E, 2, 4)
6. ¬P (¬I, 3-5)
7. ¬Q → ¬P (→I, 2-6)
8. (P → Q) → (¬Q → ¬P) (→I, 1-7)
Problem 3: Prove ∀x P(x) from {∀x(Q(x) → P(x)), ∀x Q(x)} using natural deduction.
Solution:
1. ∀x(Q(x) → P(x)) (assumption)
2. ∀x Q(x) (assumption)
3. [x] (arbitrary for ∀I)
4. Q(x) → P(x) (∀E, 1)
5. Q(x) (∀E, 2)
6. P(x) (→E, 4, 5)
7. ∀x P(x) (∀I, 3-6)
Related Resources
- Natural Deduction: https://en.wikipedia.org/wiki/Natural_deduction
- Proof Theory: https://plato.stanford.edu/entries/proof-theory/
- Sequent Calculus: https://en.wikipedia.org/wiki/Sequent_calculus
- Formal Logic: https://plato.stanford.edu/entries/logic-classical/
- Proof Assistants: https://en.wikipedia.org/wiki/Proof_assistant
- Coq: https://coq.inria.fr/
- Isabelle: https://isabelle.in.tum.de/
- Lean: https://leanprover.github.io/
- Inference Rules: https://en.wikipedia.org/wiki/Inference_rule
- Logical Consequence: https://en.wikipedia.org/wiki/Logical_consequence
- Completeness Theorem: https://en.wikipedia.org/wiki/Gödel%27s_completeness_theorem
- Soundness: https://en.wikipedia.org/wiki/Soundness
- Normalization: https://en.wikipedia.org/wiki/Normalization_(logic)
- Cut Elimination: https://en.wikipedia.org/wiki/Cut-elimination_theorem
- Formal Verification: https://en.wikipedia.org/wiki/Formal_verification
Conclusion
Natural deduction provides an intuitive, human-friendly approach to formal reasoning. By providing introduction and elimination rules for each logical connective, natural deduction mirrors the way mathematicians naturally construct proofs. This makes it ideal for education, mathematical reasoning, and proof assistants.
Understanding natural deduction is essential for anyone working with formal logic, proof assistants, or formal verification. Its close alignment with human reasoning makes it a powerful tool for both understanding logic and implementing automated reasoning systems.
The elegance of natural deduction—combining intuitive reasoning with formal rigor—demonstrates how logical systems can be both mathematically sound and practically useful.
Comments