{"id":"palomar/PALOMAR-2026-10-27-000027","url":"https://github.com/localmotiveproofs/PTS-beta-eta/tree/9d0b54a7d5f6747410212c40acf53d12544eb2e6","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-27-000027-v1.json","repo":"https://github.com/localmotiveproofs/PTS-beta-eta","tags":["cs.LO","math.LO","msc:03B40","msc:03B38","msc:68N18","msc:03B35"],"score":0,"title":"Weak and strong βη-normalization in pure type systems with βη-conversion","trust":"high","domain":"cs.LO","source":"palomar","authors":["Ankit Pradhan","Cole Vick","Ruijie Fang","Carl Kwan"],"reviews":0,"subject":"cs.LO","summary":"A Lean formalization of the Barendregt-Geuvers-Klop conjecture, \"weak normalization implies strong normalization\", for the pure type systems PTS_βη of Geuvers (Logics and Type Systems, 1993), whose conversion rule uses βη-conversion. For every PTS specification, with no functionality assumption, it proves two theorems about the legal terms of PTS_βη. If every legal term is weakly βη-normalizing, then every legal term is strongly βη-normalizing. If every legal term is weakly β-normalizing, then every legal term is strongly βη-normalizing. The proof adapts OpenAI's 2026 proof of the β case for…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-27","reactions":{},"formalized":true,"formalizes":[{"title":"Weak and strong normalization in pure type systems","identifier":"https://github.com/openai/math/tree/main/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026","relationship":"adapts"}]}