{"id":"palomar/PALOMAR-2026-08-27-000005","url":"https://github.com/elliotglazer/nf-not-wpp/tree/fa58a7a895a73422042e167391c78e9149979913","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-27-000005-v2.json","repo":"https://github.com/elliotglazer/nf-not-wpp","tags":["math.LO","msc:03E70","msc:03E25","msc:03B35","set-theory","lean","new-foundations","metamath"],"score":0,"title":"elliotglazer/nf-not-wpp","trust":"high","domain":"math.LO","source":"palomar","authors":["Elliot Glazer"],"reviews":0,"subject":"math.LO","summary":"A Lean 4 proof that standard first-order New Foundations (NF), axiomatized by extensionality and the full stratified-comprehension schema, syntactically derives the negation of the Weak Partition Principle (WPP). The translated Metamath proof enters through eleven literal Hailperin sentences, which are used internally as a finite-basis bridge and are proved deductively equivalent to standard NF.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-27","reactions":{},"formalized":true,"formalizes":[{"title":"Metamath New Foundations Explorer basis (nf.mm)","identifier":"https://github.com/metamath/set.mm/blob/c1814c4fbaf88d329d7d73ec1c7358647570e435/nf.mm","relationship":"adapts"},{"title":"Project Metamath WPP extension and accepted strict-scope endpoint source","identifier":"provenance/metamath/accepted-translator-input.mm","relationship":"formalizes"},{"title":"New Foundations Refutes the Weak Partition Principle","identifier":"archive/paper/NF_Refutes_WPP_Unconditional_Proof.pdf","relationship":"formalizes"}]}