Weak normalization implies strong normalization in pure type systems

Proves that weak normalization implies strong normalization for every pure type system: if every legal expression in every valid context has a β-normal form, every β-reduction sequence terminates. This resolves the β-Barendregt–Geuvers–Klop conjecture, including nonfunctional rules and open contexts. (Lean)

Manuscript

Weak and strong normalization in pure type systems

September 25, 2026 · source · cite as \cite{OAI:Weak-and-strong-normalization-in-pure-type-systems-September-25-2026}

We prove that every weakly β-normalizing pure type system is strongly β-normalizing. Both properties quantify over all legal expressions in all valid contexts, and reduction acts inside type annotations. No functionality hypothesis is required. This resolves the β-Barendregt–Geuvers–Klop conjecture.

Result 245 · Mathematical logic. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.