NF weak partition development: NFStandard.Equivalence.

The two directions are deliberately exposed at the model boundary. The forward direction verifies the eleven axioms of Metamath's Hailperin-derived presentation by ordinary stratified comprehension. The reverse direction instantiates the uniform cylinder compiler with the operations constructed from those eleven axioms. First-order completeness then converts equality of model classes into full deductive equivalence.

theorem NFChoice.Foundation.NFStandard.literalHailperin_models_NF {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) : Fol.allRealizeSentence S NF

The exact literal Hailperin basis supplies every stratified comprehension.

theorem NFChoice.Foundation.NFStandard.models_NF_iff_literalHailperinNF (S : Fol.Structure LNF) : Fol.allRealizeSentence S NF ↔ Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF

Standard NF and the exact literal finite basis have the same models.

theorem NFChoice.Foundation.NFStandard.nf_literalHailperin_deductivelyEquivalent : DeductivelyEquivalent NF ExactLiteralTrial.LiteralHailperinNF

Standard NF and the exact literal finite basis have the same consequences.

theorem NFChoice.Foundation.NFStandard.hailperin_models_NF {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) : Fol.allRealizeSentence S NF

The existing finite theory HailperinNF supplies standard NF.

theorem NFChoice.Foundation.NFStandard.nf_models_HailperinNF {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : Fol.allRealizeSentence S HailperinNF

Standard NF supplies the existing finite theory HailperinNF.

theorem NFChoice.Foundation.NFStandard.models_NF_iff_HailperinNF (S : Fol.Structure LNF) : Fol.allRealizeSentence S NF ↔ Fol.allRealizeSentence S HailperinNF

Standard NF and finite HailperinNF have exactly the same models.

theorem NFChoice.Foundation.NFStandard.nf_hailperin_deductivelyEquivalent : DeductivelyEquivalent NF HailperinNF

Full equivalence of the standard stratified-comprehension theory and Metamath's Hailperin-derived finite first-order presentation.