NF weak partition development: NFStandard.HailperinPresentationBridge.

The original foundation file expands class constructors by introducing intermediate set representatives. The exact-literal presentation expands the same constructors extensionally. The two presentations are equivalent in an extensional structure once singleton and unordered-pair representatives are available. Those representatives are supplied in either presentation by ax-sn and ax-nin.

structure NFChoice.Foundation.NFStandard.PresentationKernel (S : Fol.Structure LNF) : Type

The small common kernel needed to compare the two presentations.

• extensional : SemanticCore.Extensional S
• singleton : S.carrier → S.carrier

  The singleton operation of this NF model presentation.

• mem_singleton (x z : S.carrier) : SemanticCore.Mem S z (self.singleton x) ↔ z = x
• unorderedPair : S.carrier → S.carrier → S.carrier

  The unordered Pair operation of this NF model presentation.

• mem_unorderedPair (x y z : S.carrier) : SemanticCore.Mem S z (self.unorderedPair x y) ↔ z = x ∨ z = y
• kPair : S.carrier → S.carrier → S.carrier

  The k Pair operation of this NF model presentation.

• kPair_eq (x y : S.carrier) : self.kPair x y = self.unorderedPair (self.singleton x) (self.unorderedPair x y)
• mem_kPair (x y z : S.carrier) : SemanticCore.Mem S z (self.kPair x y) ↔ z = self.singleton x ∨ z = self.unorderedPair x y

The existential-intermediate presentation

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_singleton_iff {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (is ia : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (Formula.singleton is ia) ↔ SemanticCore.Lowering.lookup xs is = K.singleton (SemanticCore.Lowering.lookup xs ia)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_unorderedPair_iff {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (ip ia ib : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (Formula.unorderedPair ip ia ib) ↔ SemanticCore.Lowering.lookup xs ip = K.unorderedPair (SemanticCore.Lowering.lookup xs ia) (SemanticCore.Lowering.lookup xs ib)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_isKPair_iff {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (ip ia ib : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (Formula.isKPair ip ia ib) ↔ SemanticCore.Lowering.lookup xs ip = K.kPair (SemanticCore.Lowering.lookup xs ia) (SemanticCore.Lowering.lookup xs ib)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_equalKPair_iff {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (iz ia ib : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (Formula.equalKPair iz ia ib) ↔ SemanticCore.Lowering.lookup xs iz = K.kPair (SemanticCore.Lowering.lookup xs ia) (SemanticCore.Lowering.lookup xs ib)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_pairMem_iff {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (ia ib ir : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (Formula.pairMem ia ib ir) ↔ SemanticCore.Mem S (K.kPair (SemanticCore.Lowering.lookup xs ia) (SemanticCore.Lowering.lookup xs ib)) (SemanticCore.Lowering.lookup xs ir)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_doubleSingleton_iff {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (id ia : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (Formula.doubleSingleton id ia) ↔ SemanticCore.Lowering.lookup xs id = K.singleton (K.singleton (SemanticCore.Lowering.lookup xs ia))

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_singletonPairMem_iff {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (ia ib ir : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (Formula.singletonPairMem ia ib ir) ↔ SemanticCore.Mem S (K.kPair (K.singleton (SemanticCore.Lowering.lookup xs ia)) (K.singleton (SemanticCore.Lowering.lookup xs ib))) (SemanticCore.Lowering.lookup xs ir)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_insertedPairMem_iff {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (iz iw it ir : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (Formula.insertedPairMem iz iw it ir) ↔ SemanticCore.Mem S (K.kPair (K.singleton (K.singleton (SemanticCore.Lowering.lookup xs iz))) (K.kPair (SemanticCore.Lowering.lookup xs iw) (SemanticCore.Lowering.lookup xs it))) (SemanticCore.Lowering.lookup xs ir)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_pairSingletonSecondMem_iff {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (ia iz ir : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (Formula.pairSingletonSecondMem ia iz ir) ↔ SemanticCore.Mem S (K.kPair (SemanticCore.Lowering.lookup xs ia) (K.singleton (SemanticCore.Lowering.lookup xs iz))) (SemanticCore.Lowering.lookup xs ir)

The exact-literal presentation

theorem NFChoice.Foundation.NFStandard.PresentationKernel.representsLiteral_singleton_ofKernel {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} {xs : DVec S.carrier n} {A : ExactLiteralTrial.LiteralClass n} {a : S.carrier} (ha : RepresentsLiteral xs A a) : RepresentsLiteral xs A.singleton (K.singleton a)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.representsLiteral_unorderedPair_ofKernel {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} {xs : DVec S.carrier n} {A B : ExactLiteralTrial.LiteralClass n} {a b : S.carrier} (ha : RepresentsLiteral xs A a) (hb : RepresentsLiteral xs B b) : RepresentsLiteral xs (A.unorderedPair B) (K.unorderedPair a b)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.representsLiteral_kPair_ofKernel {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} {xs : DVec S.carrier n} {A B : ExactLiteralTrial.LiteralClass n} {a b : S.carrier} (ha : RepresentsLiteral xs A a) (hb : RepresentsLiteral xs B b) : RepresentsLiteral xs (A.kPair B) (K.kPair a b)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_setEqClass_iff_eq_ofKernel {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (r : Fin n) (A : ExactLiteralTrial.LiteralClass n) (a : S.carrier) (ha : RepresentsLiteral xs A a) : SemanticCore.Lowering.FormulaHolds S xs (ExactLiteralTrial.LiteralClass.setEqClass r A) ↔ SemanticCore.Lowering.lookup xs r = a

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_classMemSet_iff_mem_ofKernel {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (A : ExactLiteralTrial.LiteralClass n) (r : Fin n) (a : S.carrier) (ha : RepresentsLiteral xs A a) : SemanticCore.Lowering.FormulaHolds S xs (A.classMemSet r) ↔ SemanticCore.Mem S a (SemanticCore.Lowering.lookup xs r)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_literalKPair_iff_kernel {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (ip ia ib : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (ExactLiteralTrial.literalKPair ip ia ib) ↔ SemanticCore.Lowering.lookup xs ip = K.kPair (SemanticCore.Lowering.lookup xs ia) (SemanticCore.Lowering.lookup xs ib)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_literalPairMem_iff_kernel {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (ia ib ir : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (ExactLiteralTrial.literalPairMem ia ib ir) ↔ SemanticCore.Mem S (K.kPair (SemanticCore.Lowering.lookup xs ia) (SemanticCore.Lowering.lookup xs ib)) (SemanticCore.Lowering.lookup xs ir)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_literalSingletonPairMem_iff_kernel {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (ia ib ir : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (ExactLiteralTrial.literalSingletonPairMem ia ib ir) ↔ SemanticCore.Mem S (K.kPair (K.singleton (SemanticCore.Lowering.lookup xs ia)) (K.singleton (SemanticCore.Lowering.lookup xs ib))) (SemanticCore.Lowering.lookup xs ir)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_literalInsertedPairMem_iff_kernel {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (iz iw it ir : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (ExactLiteralTrial.literalInsertedPairMem iz iw it ir) ↔ SemanticCore.Mem S (K.kPair (K.singleton (K.singleton (SemanticCore.Lowering.lookup xs iz))) (K.kPair (SemanticCore.Lowering.lookup xs iw) (SemanticCore.Lowering.lookup xs it))) (SemanticCore.Lowering.lookup xs ir)

theorem NFChoice.Foundation.NFStandard.PresentationKernel.formulaHolds_literalPairSingletonSecondMem_iff_kernel {S : Fol.Structure LNF} (K : PresentationKernel S) {n : ℕ} (xs : DVec S.carrier n) (ia iz ir : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (ExactLiteralTrial.literalPairSingletonSecondMem ia iz ir) ↔ SemanticCore.Mem S (K.kPair (SemanticCore.Lowering.lookup xs ia) (K.singleton (SemanticCore.Lowering.lookup xs iz))) (SemanticCore.Lowering.lookup xs ir)

Extracting the common kernel from the original presentation

theorem NFChoice.Foundation.NFStandard.realizes_foundation_axiom {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (name : HailperinAxiomName) : Fol.realizeSentence S (axiomFormula name)

Realize a named axiom from the original foundation theory.

theorem NFChoice.Foundation.NFStandard.formulaHolds_foundation_axiom {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (name : HailperinAxiomName) : SemanticCore.Lowering.FormulaHolds S DVec.nil (axiomSyntax name)

Intrinsic semantic form of an original foundation axiom.

theorem NFChoice.Foundation.NFStandard.foundation_model_extensional {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) : SemanticCore.Extensional S

theorem NFChoice.Foundation.NFStandard.foundation_exists_nin {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x y : S.carrier) : ∃ (a : S.carrier), ∀ (z : S.carrier), SemanticCore.Mem S z a ↔ ¬(SemanticCore.Mem S z x ∧ SemanticCore.Mem S z y)

noncomputable def NFChoice.Foundation.NFStandard.foundationNin {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x y : S.carrier) : S.carrier

Standard-NF model or stratification construction identified upstream as foundationNin.

Equations

• NFChoice.Foundation.NFStandard.foundationNin hH x y = Classical.choose ⋯

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_foundationNin {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x y z : S.carrier) : SemanticCore.Mem S z (foundationNin hH x y) ↔ ¬(SemanticCore.Mem S z x ∧ SemanticCore.Mem S z y)

theorem NFChoice.Foundation.NFStandard.foundation_exists_singleton {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x : S.carrier) : ∃ (a : S.carrier), ∀ (z : S.carrier), SemanticCore.Mem S z a ↔ z = x

noncomputable def NFChoice.Foundation.NFStandard.foundationSingleton {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x : S.carrier) : S.carrier

Standard-NF model or stratification construction identified upstream as foundationSingleton.

Equations

• NFChoice.Foundation.NFStandard.foundationSingleton hH x = Classical.choose ⋯

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_foundationSingleton {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x z : S.carrier) : SemanticCore.Mem S z (foundationSingleton hH x) ↔ z = x

noncomputable def NFChoice.Foundation.NFStandard.foundationComplement {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x : S.carrier) : S.carrier

Standard-NF model or stratification construction identified upstream as foundationComplement.

Equations

• NFChoice.Foundation.NFStandard.foundationComplement hH x = NFChoice.Foundation.NFStandard.foundationNin hH x x

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_foundationComplement {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x z : S.carrier) : SemanticCore.Mem S z (foundationComplement hH x) ↔ ¬SemanticCore.Mem S z x

noncomputable def NFChoice.Foundation.NFStandard.foundationUnion {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x y : S.carrier) : S.carrier

Standard-NF model or stratification construction identified upstream as foundationUnion.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_foundationUnion {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x y z : S.carrier) : SemanticCore.Mem S z (foundationUnion hH x y) ↔ SemanticCore.Mem S z x ∨ SemanticCore.Mem S z y

noncomputable def NFChoice.Foundation.NFStandard.foundationUnorderedPair {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x y : S.carrier) : S.carrier

Standard-NF model or stratification construction identified upstream as foundationUnorderedPair.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_foundationUnorderedPair {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x y z : S.carrier) : SemanticCore.Mem S z (foundationUnorderedPair hH x y) ↔ z = x ∨ z = y

noncomputable def NFChoice.Foundation.NFStandard.foundationKPair {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x y : S.carrier) : S.carrier

Standard-NF model or stratification construction identified upstream as foundationKPair.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_foundationKPair {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) (x y z : S.carrier) : SemanticCore.Mem S z (foundationKPair hH x y) ↔ z = foundationSingleton hH x ∨ z = foundationUnorderedPair hH x y

noncomputable def NFChoice.Foundation.NFStandard.PresentationKernel.ofFoundationModel {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S HailperinNF) : PresentationKernel S

Standard-NF model or stratification construction identified upstream as PresentationKernel.ofFoundationModel.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NFChoice.Foundation.NFStandard.PresentationKernel.ofLiteralModel {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) : PresentationKernel S

Standard-NF model or stratification construction identified upstream as PresentationKernel.ofLiteralModel.

Equations

• One or more equations did not get rendered due to their size.

Axiom-by-axiom and theory-level equivalence

theorem NFChoice.Foundation.NFStandard.formulaHolds_axiomSyntax_iff_literal {S : Fol.Structure LNF} (K : PresentationKernel S) (name : HailperinAxiomName) : SemanticCore.Lowering.FormulaHolds S DVec.nil (axiomSyntax name) ↔ SemanticCore.Lowering.FormulaHolds S DVec.nil (ExactLiteralTrial.literalAxiomSyntax name)

Each named original axiom has the same semantics as its literal expansion.

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

Every model of the original presentation is a model of the literal one.

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

Every model of the literal presentation is a model of the original one.

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

The two finite Hailperin presentations have exactly the same models.

theorem NFChoice.Foundation.NFStandard.hailperinPresentation_deductivelyEquivalent : DeductivelyEquivalent HailperinNF ExactLiteralTrial.LiteralHailperinNF

Hence the two presentations have exactly the same formal consequences.