Normalization

Origin. Gentzen (1935) cut elimination. Prawitz (1965) for natural deduction. Proofs simplify to canonical form. Foundation for proof theory and type theory.

Models. Detours: intro followed by elim. Normalization: remove detours. Strong normalization: all reduction sequences terminate. Canonical proofs reveal structure.

Formalism.

Detour (natural deduction): ⋮ ─── ∧I A ∧ B ─── ∧E₁ A

Reduces to: ⋮ A

β-reduction (implication): [A] ⋮ B ─── →I A → B A ─────── →E B

Reduces to proof of B with A substituted.

Normal form: No detours. Subformula property: only subformulas of conclusion appear.

Strong normalization: All reduction sequences terminate. Well-typed λ-terms: SN. Proof: logical relations, reducibility candidates.

Weak normalization: Some reduction sequence terminates. Weaker property.

Church-Rosser: If M →* N₁ and M →* N₂, then ∃P. N₁ →* P and N₂ →* P. Unique normal form (if exists).

Cut elimination: Sequent calculus analog. Remove cut rule from proofs. Gentzen's Hauptsatz.

Symbols.

Symbol	Unicode	Name	Meaning
→	U+2192	Rightwards arrow / Reduction	One reduction step; also implication in the rules
→*	—	Reflexive transitive closure	Reduction in zero or more steps
∧	U+2227	Conjunction	Connective of the ∧I/∧E detour
β	U+03B2	Beta	The reduction matching →I followed by →E
λ	U+03BB	Lambda	Abstraction; the term-level →I
∃	U+2203	Exists	Confluence: a common reduct exists
⋮	U+22EE	Vertical ellipsis	Suppressed subderivation in a rule display
↓	U+2193	Downwards arrow / Normal form	Marks an irreducible term or derivation
SN	—	Strong normalization	Every reduction sequence terminates
WN	—	Weak normalization	Some reduction sequence terminates
CR	—	Church–Rosser	Confluence, hence unique normal forms

Metatheory. Gentzen proved cut elimination in 1935 and Prawitz proved normalization for natural deduction in 1965; the two are the same theorem in different formalisms, transported by the translation between LJ and NJ. Strong normalization for the simply typed λ-calculus, and hence for the implicational fragment of NJ, was proved by Tait (1967) with the computability-predicate method; Girard (1972) extended it to System F using reducibility candidates, an impredicative argument that cannot be replaced by a predicative one, since strong normalization for System F implies the consistency of second-order arithmetic and so is unprovable there. The same obstruction bounds System T: its normalization yields the consistency of Peano arithmetic, so it is not provable in PA. Strong normalization implies weak; combined with Church–Rosser it gives unique normal forms, so βη-equality of simply typed terms is decidable — but Statman (1979) proved the decision problem is not elementary recursive. Normal derivations satisfy the subformula property, which is how normalization delivers consistency.

Applies to. Proof assistants. Type theory. λ-calculus. Program termination. Constructive logic.

Limitations. Normalization and Turing completeness are incompatible: the untyped λ-calculus has non-normalizing terms such as (λx.xx)(λx.xx), and adding general recursion or a fixed-point combinator to a typed system destroys strong normalization, so a language in which every program terminates cannot express every computable function. Because normalization for a system implies that system's consistency, Gödel's second theorem forbids proving it internally — the proof always uses strength the system lacks, which is why normalization is a calibration of strength rather than a routine syntactic check. Impredicative type formation is fragile: Girard's paradox shows that a type of all types destroys normalization in dependent type theory, and adding large eliminations or impredicative universes must be justified case by case. Normalization by itself does not deliver the subformula property for full natural deduction; permutative conversions for ∨ and ∃ must be added, and the classical system with those connectives is not covered by Prawitz's theorem. Finally, a normal form can be astronomically larger than the term it came from, so normalization is a criterion of correctness, not a method of computation.