NF weak partition development: SemanticCore.LiteralFoundation.

This module fixes the replay boundary to the append-only literal Hailperin theory. Its pair/singleton class terms are unary predicates expanded extensionally; no representative set for a nested class term is postulated.

theorem NFChoice.SemanticCore.extensional_iff_literal_axExt (S : Fol.Structure Foundation.LNF) : Extensional S ↔ Fol.realizeSentence S (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axExt)

The literal trial's ax-ext sentence realizes exactly structure extensionality.

@[reducible, inline]

abbrev NFChoice.SemanticCore.LiteralReplayTarget (sourceChoiceNF : Fol.sentence Foundation.LNF) : Prop

The exact source target consumed by the generated semantic replay.

Equations

• NFChoice.SemanticCore.LiteralReplayTarget sourceChoiceNF = NFChoice.Foundation.ExactLiteralTrial.LiteralSourceNFProvesNotChoiceTarget sourceChoiceNF