Natural Deduction Systems: Intuitive Proof Methods

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.