Natural Deduction

Origin. Gentzen (1934-1935). Proof system matching natural reasoning. Introduction and elimination rules. Normalization theorem. Curry-Howard correspondence to λ-calculus.

Models. Proofs as derivation trees. Each connective: intro and elim rules. Assumptions can be discharged. Normal forms: no detours. Proofs-as-programs.

Formalism.

Judgment: Γ ⊢ A (A provable from assumptions Γ)

Conjunction: Γ ⊢ A Γ ⊢ B Γ ⊢ A ∧ B ─────────────── ∧I ─────────── ∧E₁ Γ ⊢ A ∧ B Γ ⊢ A

Implication: Γ, A ⊢ B Γ ⊢ A → B Γ ⊢ A ────────── →I ───────────────────── →E Γ ⊢ A → B Γ ⊢ B

Disjunction: Γ ⊢ A Γ ⊢ A∨B Γ,A ⊢ C Γ,B ⊢ C ─────── ∨I₁ ─────────────────────────── ∨E Γ ⊢ A∨B Γ ⊢ C

Negation (intuitionistic): Γ, A ⊢ ⊥ Γ ⊢ ⊥ ────────── ¬I ─────── ⊥E Γ ⊢ ¬A Γ ⊢ C

Classical (additional): Γ, ¬A ⊢ ⊥ ────────── RAA (reductio) Γ ⊢ A

Normalization: Detour: intro immediately followed by elim. (λx.M) N ↝ M[N/x] Cut elimination = normalization.

Symbols.

Symbol	Unicode	Name	Meaning
⊢	U+22A2	Turnstile	Derivability from the open assumptions Γ
Γ	U+0393	Gamma / Context	The undischarged assumptions
∧	U+2227	Conjunction	Rules ∧I, ∧E₁, ∧E₂
∨	U+2228	Disjunction	Rules ∨I₁, ∨I₂, ∨E
→	U+2192	Implication	Rules →I (discharging) and →E
¬	U+00AC	Negation	Defined by ¬A ≡ A → ⊥
⊥	U+22A5	Absurdity	Falsehood; premise of ⊥E
λ	U+03BB	Lambda	Term-former matching →I
↝	U+219D	Reduces to	Detour conversion, i.e. β-reduction
I	—	Introduction rule	Specifies how the connective is asserted
E	—	Elimination rule	Specifies how the connective is used
[ ]ⁿ	—	Discharge	Cancels an assumption at the labelled inference
RAA	—	Reductio ad absurdum	The rule that makes the system classical

Metatheory. Gentzen introduced NJ and NK in 1934–35 and sketched normalization for NJ; Prawitz's Natural Deduction (1965) proved it, and strong normalization for the intuitionistic system followed in his 1971 survey. Normal derivations decompose each branch into an elimination part, a minimum formula, and an introduction part, and from that decomposition the subformula property follows, and with it consistency and — for NJ — the disjunction and existence properties. Normalization corresponds to cut elimination, but the correspondence is not a bijection: many sequent derivations map to one natural-deduction derivation, because natural deduction already quotients away some rule permutations. Under Curry–Howard the NJ derivations of the implicational fragment are exactly the simply typed λ-terms, detour conversion is β-reduction, and strong normalization of the typed calculus (Tait 1967; Girard 1972 for System F) is the normalization theorem for the proofs. The cost matches cut elimination: normalization is non-elementary, and Statman (1979) showed deciding equality of simply typed terms is not elementary recursive.

Applies to. Proof assistants. Logical reasoning. Type theory foundations. Philosophy of logic. Proof search.

Limitations. The eliminations for ∨ and ∃ are the defect: their conclusion is an arbitrary formula C, so detour conversions alone do not yield the subformula property and permutative conversions must be added; Prawitz's normalization theorem for classical NK is proved only for the fragment without ∨ and ∃, and recovering the full classical case requires the λμ-calculus or a translation. Classical reductio has no matching introduction rule, so the classical constants are not determined by their introduction rules alone, and the proof-theoretic justification of the connectives that natural deduction is prized for does not extend to NK. Read bottom-up the elimination rules are not analytic — →E requires inventing the minor premise A — so proof search is worse than in the sequent calculus, where every rule decomposes its conclusion. Contexts are implicit in the tree of discharged assumptions, so linear and relevant variants must add explicit bookkeeping to control duplication and vacuous discharge. There is no generally accepted natural deduction for classical modal logics without labels or a multiple-conclusion generalization.