NF weak partition development: NFStandard.CylinderToNF.

This module is the presentation-independent end of the Hailperin compiler. Once a structure supplies the small CylinderAlgebra interface, the generic compiler constructs the extension of every stratified formula. The lemmas below turn those constructed extensions back into the closed first-order sentences comprising NF.

theorem NFChoice.Foundation.NFStandard.realize_comprehensionInstance_of_cylinder {S : Fol.Structure LNF} (C : CylinderAlgebra S) {n : ℕ} (p : Formula (n + 1)) (hp : p.Stratified) : Fol.realizeSentence S (comprehensionInstance p)

A cylinder algebra realizes each closed stratified-comprehension axiom.

theorem NFChoice.Foundation.NFStandard.models_NF_of_cylinder {S : Fol.Structure LNF} (C : CylinderAlgebra S) (hExt : Fol.realizeSentence S (ExactLiteralTrial.literalAxiomFormula HailperinAxiomName.axExt)) : Fol.allRealizeSentence S NF

Extensionality plus a cylinder algebra is a model of standard NF. No feature of the particular Metamath Hailperin-derived finite presentation is used here.