Natural Deduction — Mathematics Knowledge System

Overview

Natural deduction is a formal proof system, introduced independently by Gerhard Gentzen and Stanisław Jaśkowski in 1934, designed to mirror the way mathematicians actually reason rather than to minimize the number of primitive axioms. Instead of a handful of axiom schemas and one inference rule (as in Hilbert-style systems), natural deduction gives every logical connective and quantifier a matched pair of rules: an introduction rule, showing how to derive a formula whose main connective is that symbol, and an elimination rule, showing what can be derived from such a formula. Its signature device is the discharged assumption: to prove an implication φ → ψ, you temporarily assume φ, derive ψ under that assumption, and then discharge (retract) the assumption, packaging the whole sub-argument into a single implication that no longer depends on φ. This assumption-and-discharge bookkeeping is exactly how conditional and indirect proofs are written in ordinary mathematical practice, which is why natural deduction (and its descendant, sequent calculus) is the proof system of choice for proof assistants like Coq, Lean, and Isabelle.

Intuition

Each connective comes with an honest pair of rules: the introduction rule tells you the minimal, principled way to manufacture a formula with that connective as its main symbol, and the elimination rule tells you the minimal, principled way to use one once you have it — nothing is smuggled in. Implication is the most distinctive case: to prove 'if φ then ψ,' you don't need φ to actually be true, you just borrow it as a hypothesis, see what follows, and then hand back an implication that stands on its own once the hypothesis is discharged. This is precisely the pattern behind every 'assume x is even; then...; therefore if x is even, then...' argument a mathematician writes by hand, which is why natural deduction proofs read like ordinary informal proofs dressed in explicit syntax.

Formal Definition

Definition

Each connective has an introduction (I) and elimination (E) rule. Selected core rules, written with Γ for the set of undischarged assumptions in force:

\dfrac{\Gamma, \varphi \vdash \psi}{\Gamma \vdash \varphi \rightarrow \psi} \ (\rightarrow\text{-I})

Conditional (implication) introduction — discharges the assumption φ

\dfrac{\Gamma \vdash \varphi \rightarrow \psi \qquad \Gamma \vdash \varphi}{\Gamma \vdash \psi} \ (\rightarrow\text{-E})

Implication elimination (modus ponens)

\dfrac{\Gamma \vdash \varphi \qquad \Gamma \vdash \psi}{\Gamma \vdash \varphi \wedge \psi} \ (\wedge\text{-I}) \qquad \dfrac{\Gamma \vdash \varphi \wedge \psi}{\Gamma \vdash \varphi} \ (\wedge\text{-E})

Conjunction introduction and (left) elimination

\dfrac{\Gamma, \varphi \vdash \bot}{\Gamma \vdash \neg \varphi} \ (\neg\text{-I}) \qquad \dfrac{\Gamma \vdash \neg\neg\varphi}{\Gamma \vdash \varphi} \ (\text{DNE, classical only})

Negation introduction, and double-negation elimination

Worked Examples

Open a subproof by assuming φ.
$1.\ \varphi \quad \text{(assumption)}$
The assumption itself is already a derivation of φ under that assumption — nothing further is needed.
$2.\ \varphi \quad \text{(reiteration of line 1)}$
Discharge the assumption φ, packaging lines 1–2 into an implication that depends on nothing.
$3.\ \varphi \rightarrow \varphi \quad (\rightarrow\text{-I, discharging 1})$

Answer: ⊢ φ → φ, a one-assumption, one-discharge natural deduction proof — the simplest possible use of →-introduction.

Practice Problems

Difficulty 3/10

What natural deduction rule allows concluding φ from a proof of φ ∧ ψ?

Difficulty 4/10

Explain the role of 'discharging an assumption' in the →-introduction rule.

Difficulty 6/10

Give a natural deduction proof of φ → (ψ → φ).

Quiz

Summary

Natural deduction gives every connective and quantifier a matched introduction/elimination rule pair, rather than relying on axiom schemas.
Its hallmark device is the discharged assumption: →-introduction temporarily assumes the antecedent, derives the consequent, then discharges the assumption to produce an unconditional implication.
Because its proof style mirrors informal mathematical argument, natural deduction (and sequent calculus) underlies modern proof assistants such as Coq, Lean, and Isabelle.

References

WebsiteWikipedia — Natural deduction