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	Proves
I	—	Introduction	Creates connective
E	—	Elimination	Uses connective
⊥	U+22A5	Absurdity	Falsehood
[ ]ⁿ	—	Discharge	Cancel assumption

Metatheory. Normalization: all proofs normalize. Strong normalization for typed systems. Subformula property. Curry-Howard: ND proofs ≅ λ-terms. Proof identity via normalization.

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

Limitations. Proof search harder than sequent calculus. Classical logic needs extra rules. Normalization doesn't always give unique normal form. Resource-sensitive variants need care.