NF weak partition development: NFStandard.HailperinModel.

This file packages the eleven axioms of the literal Metamath Hailperin-derived presentation as ordinary operations on an arbitrary model. All operations are Skolem choices from the actual axioms; their API exposes only extensional membership laws.

theorem NFChoice.Foundation.NFStandard.formulaHolds_literal_axiom {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (name : HailperinAxiomName) : SemanticCore.Lowering.FormulaHolds S DVec.nil (ExactLiteralTrial.literalAxiomSyntax name)

The intrinsic formula underlying any literal axiom holds in its model.

theorem NFChoice.Foundation.NFStandard.exists_nin {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (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)

Raw semantic content of ax-nin.

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

A selected NAND set supplied by ax-nin.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_nin {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x y z : S.carrier) : SemanticCore.Mem S z (nin hH x y) ↔ ¬(SemanticCore.Mem S z x ∧ SemanticCore.Mem S z y)

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

Raw semantic content of ax-sn.

noncomputable def NFChoice.Foundation.NFStandard.singleton {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : S.carrier

A selected singleton supplied by ax-sn.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_singleton {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x z : S.carrier) : SemanticCore.Mem S z (singleton hH x) ↔ z = x

noncomputable def NFChoice.Foundation.NFStandard.complement {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : S.carrier

Complement, derived from NAND.

Equations

• NFChoice.Foundation.NFStandard.complement hH x = NFChoice.Foundation.NFStandard.nin hH x x

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_complement {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x z : S.carrier) : SemanticCore.Mem S z (complement hH x) ↔ ¬SemanticCore.Mem S z x

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

Binary union, derived by De Morgan from NAND.

Equations

• NFChoice.Foundation.NFStandard.union hH x y = NFChoice.Foundation.NFStandard.nin hH (NFChoice.Foundation.NFStandard.complement hH x) (NFChoice.Foundation.NFStandard.complement hH y)

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_union {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x y z : S.carrier) : SemanticCore.Mem S z (union hH x y) ↔ SemanticCore.Mem S z x ∨ SemanticCore.Mem S z y

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

Unordered pair, derived as the union of two selected singletons.

Equations

• NFChoice.Foundation.NFStandard.unorderedPair hH x y = NFChoice.Foundation.NFStandard.union hH (NFChoice.Foundation.NFStandard.singleton hH x) (NFChoice.Foundation.NFStandard.singleton hH y)

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_unorderedPair {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x y z : S.carrier) : SemanticCore.Mem S z (unorderedPair hH x y) ↔ z = x ∨ z = y

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

The selected Kuratowski ordered pair.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_kPair {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x y z : S.carrier) : SemanticCore.Mem S z (kPair hH x y) ↔ z = singleton hH x ∨ z = unorderedPair hH x y

def NFChoice.Foundation.NFStandard.RepresentsLiteral {S : Fol.Structure LNF} {n : ℕ} (xs : DVec S.carrier n) (A : ExactLiteralTrial.LiteralClass n) (a : S.carrier) : Prop

An element of the carrier extensionally represents a literal class.

Equations

• NFChoice.Foundation.NFStandard.RepresentsLiteral xs A a = ∀ (z : S.carrier), NFChoice.SemanticCore.Mem S z a ↔ NFChoice.Compiler.NFCompactLeafSemanticAdapters.LiteralClassSem xs A z

theorem NFChoice.Foundation.NFStandard.representsLiteral_unique {S : Fol.Structure LNF} {n : ℕ} (hExt : SemanticCore.Extensional S) {xs : DVec S.carrier n} {A : ExactLiteralTrial.LiteralClass n} {a b : S.carrier} (ha : RepresentsLiteral xs A a) (hb : RepresentsLiteral xs A b) : a = b

@[simp]

theorem NFChoice.Foundation.NFStandard.representsLiteral_setVar {S : Fol.Structure LNF} {n : ℕ} (xs : DVec S.carrier n) (i : Fin n) : RepresentsLiteral xs (ExactLiteralTrial.LiteralClass.setVar i) (SemanticCore.Lowering.lookup xs i)

theorem NFChoice.Foundation.NFStandard.representsLiteral_singleton {S : Fol.Structure LNF} {n : ℕ} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {xs : DVec S.carrier n} {A : ExactLiteralTrial.LiteralClass n} {a : S.carrier} (ha : RepresentsLiteral xs A a) : RepresentsLiteral xs A.singleton (singleton hH a)

theorem NFChoice.Foundation.NFStandard.representsLiteral_unorderedPair {S : Fol.Structure LNF} {n : ℕ} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {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) (unorderedPair hH a b)

theorem NFChoice.Foundation.NFStandard.representsLiteral_kPair {S : Fol.Structure LNF} {n : ℕ} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {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) (kPair hH a b)

theorem NFChoice.Foundation.NFStandard.formulaHolds_setEqClass_iff_eq {S : Fol.Structure LNF} {n : ℕ} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (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

A literal set-equality formula identifies the canonical representative.

theorem NFChoice.Foundation.NFStandard.formulaHolds_classMemSet_iff_mem {S : Fol.Structure LNF} {n : ℕ} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (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)

A literal class-membership formula is membership of its canonical representative.

@[simp]

theorem NFChoice.Foundation.NFStandard.formulaHolds_literalKPair_iff {S : Fol.Structure LNF} {n : ℕ} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (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 = kPair hH (SemanticCore.Lowering.lookup xs ia) (SemanticCore.Lowering.lookup xs ib)

@[simp]

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

@[simp]

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

@[simp]

theorem NFChoice.Foundation.NFStandard.formulaHolds_literalInsertedPairMem_iff {S : Fol.Structure LNF} {n : ℕ} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (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 (kPair hH (singleton hH (singleton hH (SemanticCore.Lowering.lookup xs iz))) (kPair hH (SemanticCore.Lowering.lookup xs iw) (SemanticCore.Lowering.lookup xs it))) (SemanticCore.Lowering.lookup xs ir)

@[simp]

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

Skolem witnesses for the remaining Hailperin axioms

theorem NFChoice.Foundation.NFStandard.exists_xp {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : ∃ (y : S.carrier), ∀ (z : S.carrier), SemanticCore.Mem S z y ↔ ∃ (w : S.carrier) (t : S.carrier), z = kPair hH w t ∧ SemanticCore.Mem S t x

theorem NFChoice.Foundation.NFStandard.exists_cnv {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : ∃ (y : S.carrier), ∀ (z w : S.carrier), SemanticCore.Mem S (kPair hH z w) y ↔ SemanticCore.Mem S (kPair hH w z) x

theorem NFChoice.Foundation.NFStandard.exists_oneC {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) : ∃ (x : S.carrier), ∀ (y : S.carrier), SemanticCore.Mem S y x ↔ ∃ (z : S.carrier), ∀ (w : S.carrier), SemanticCore.Mem S w y ↔ w = z

theorem NFChoice.Foundation.NFStandard.exists_sset {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) : ∃ (x : S.carrier), ∀ (y z : S.carrier), SemanticCore.Mem S (kPair hH y z) x ↔ ∀ (w : S.carrier), SemanticCore.Mem S w y → SemanticCore.Mem S w z

theorem NFChoice.Foundation.NFStandard.exists_si {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : ∃ (y : S.carrier), ∀ (z w : S.carrier), SemanticCore.Mem S (kPair hH (singleton hH z) (singleton hH w)) y ↔ SemanticCore.Mem S (kPair hH z w) x

theorem NFChoice.Foundation.NFStandard.exists_ins2 {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : ∃ (y : S.carrier), ∀ (z w t : S.carrier), SemanticCore.Mem S (kPair hH (singleton hH (singleton hH z)) (kPair hH w t)) y ↔ SemanticCore.Mem S (kPair hH z t) x

theorem NFChoice.Foundation.NFStandard.exists_ins3 {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : ∃ (y : S.carrier), ∀ (z w t : S.carrier), SemanticCore.Mem S (kPair hH (singleton hH (singleton hH z)) (kPair hH w t)) y ↔ SemanticCore.Mem S (kPair hH z w) x

theorem NFChoice.Foundation.NFStandard.exists_typeLower {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : ∃ (y : S.carrier), ∀ (z : S.carrier), SemanticCore.Mem S z y ↔ ∀ (w : S.carrier), SemanticCore.Mem S (kPair hH w (singleton hH z)) x

noncomputable def NFChoice.Foundation.NFStandard.xp {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : S.carrier

Cartesian-product/range constructor selected from ax-xp.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_xp {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x z : S.carrier) : SemanticCore.Mem S z (xp hH x) ↔ ∃ (w : S.carrier) (t : S.carrier), z = kPair hH w t ∧ SemanticCore.Mem S t x

noncomputable def NFChoice.Foundation.NFStandard.cnv {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : S.carrier

Converse-relation constructor selected from ax-cnv.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_cnv {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x z w : S.carrier) : SemanticCore.Mem S (kPair hH z w) (cnv hH x) ↔ SemanticCore.Mem S (kPair hH w z) x

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

The set of all singleton sets selected from ax-1c.

Equations

• NFChoice.Foundation.NFStandard.oneC hH = Classical.choose ⋯

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_oneC {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (y : S.carrier) : SemanticCore.Mem S y (oneC hH) ↔ ∃ (z : S.carrier), ∀ (w : S.carrier), SemanticCore.Mem S w y ↔ w = z

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

The subset relation selected from ax-sset.

Equations

• NFChoice.Foundation.NFStandard.sset hH = Classical.choose ⋯

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_sset {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (y z : S.carrier) : SemanticCore.Mem S (kPair hH y z) (sset hH) ↔ ∀ (w : S.carrier), SemanticCore.Mem S w y → SemanticCore.Mem S w z

noncomputable def NFChoice.Foundation.NFStandard.si {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : S.carrier

Singleton-image relation transformer selected from ax-si.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_si {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x z w : S.carrier) : SemanticCore.Mem S (kPair hH (singleton hH z) (singleton hH w)) (si hH x) ↔ SemanticCore.Mem S (kPair hH z w) x

noncomputable def NFChoice.Foundation.NFStandard.ins2 {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : S.carrier

Second inserted-pair transformer selected from ax-ins2.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_ins2 {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x z w t : S.carrier) : SemanticCore.Mem S (kPair hH (singleton hH (singleton hH z)) (kPair hH w t)) (ins2 hH x) ↔ SemanticCore.Mem S (kPair hH z t) x

noncomputable def NFChoice.Foundation.NFStandard.ins3 {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : S.carrier

Third inserted-pair transformer selected from ax-ins3.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_ins3 {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x z w t : S.carrier) : SemanticCore.Mem S (kPair hH (singleton hH (singleton hH z)) (kPair hH w t)) (ins3 hH x) ↔ SemanticCore.Mem S (kPair hH z w) x

noncomputable def NFChoice.Foundation.NFStandard.typeLower {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x : S.carrier) : S.carrier

Type-lowering transformer selected from ax-typlower.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_typeLower {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (x z : S.carrier) : SemanticCore.Mem S z (typeLower hH x) ↔ ∀ (w : S.carrier), SemanticCore.Mem S (kPair hH w (singleton hH z)) x

A reusable bundled kernel

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

All semantic operations supplied by the Metamath Hailperin-derived finite basis, detached from the syntactic theory after extraction. The equations on the four derived constructors record that no additional choices were made for them.

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

  The nin operation of this NF model presentation.

• mem_nin (x y z : S.carrier) : SemanticCore.Mem S z (self.nin x y) ↔ ¬(SemanticCore.Mem S z x ∧ SemanticCore.Mem S z y)
• 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
• complement : S.carrier → S.carrier

  The complement operation of this NF model presentation.

• complement_eq (x : S.carrier) : self.complement x = self.nin x x
• mem_complement (x z : S.carrier) : SemanticCore.Mem S z (self.complement x) ↔ ¬SemanticCore.Mem S z x
• union : S.carrier → S.carrier → S.carrier

  The union operation of this NF model presentation.

• union_eq (x y : S.carrier) : self.union x y = self.nin (self.complement x) (self.complement y)
• mem_union (x y z : S.carrier) : SemanticCore.Mem S z (self.union x y) ↔ SemanticCore.Mem S z x ∨ SemanticCore.Mem S z y
• unorderedPair : S.carrier → S.carrier → S.carrier

  The unordered Pair operation of this NF model presentation.

• unorderedPair_eq (x y : S.carrier) : self.unorderedPair x y = self.union (self.singleton x) (self.singleton y)
• 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
• xp : S.carrier → S.carrier

  The xp operation of this NF model presentation.

• mem_xp (x z : S.carrier) : SemanticCore.Mem S z (self.xp x) ↔ ∃ (w : S.carrier) (t : S.carrier), z = self.kPair w t ∧ SemanticCore.Mem S t x
• cnv : S.carrier → S.carrier

  The cnv operation of this NF model presentation.

• mem_cnv (x z w : S.carrier) : SemanticCore.Mem S (self.kPair z w) (self.cnv x) ↔ SemanticCore.Mem S (self.kPair w z) x
• oneC : S.carrier

  The one C operation of this NF model presentation.

• mem_oneC (y : S.carrier) : SemanticCore.Mem S y self.oneC ↔ ∃ (z : S.carrier), ∀ (w : S.carrier), SemanticCore.Mem S w y ↔ w = z
• sset : S.carrier

  The sset operation of this NF model presentation.

• mem_sset (y z : S.carrier) : SemanticCore.Mem S (self.kPair y z) self.sset ↔ ∀ (w : S.carrier), SemanticCore.Mem S w y → SemanticCore.Mem S w z
• si : S.carrier → S.carrier

  The si operation of this NF model presentation.

• mem_si (x z w : S.carrier) : SemanticCore.Mem S (self.kPair (self.singleton z) (self.singleton w)) (self.si x) ↔ SemanticCore.Mem S (self.kPair z w) x
• ins2 : S.carrier → S.carrier

  The ins2 operation of this NF model presentation.

• mem_ins2 (x z w t : S.carrier) : SemanticCore.Mem S (self.kPair (self.singleton (self.singleton z)) (self.kPair w t)) (self.ins2 x) ↔ SemanticCore.Mem S (self.kPair z t) x
• ins3 : S.carrier → S.carrier

  The ins3 operation of this NF model presentation.

• mem_ins3 (x z w t : S.carrier) : SemanticCore.Mem S (self.kPair (self.singleton (self.singleton z)) (self.kPair w t)) (self.ins3 x) ↔ SemanticCore.Mem S (self.kPair z w) x
• typeLower : S.carrier → S.carrier

  The type Lower operation of this NF model presentation.

• mem_typeLower (x z : S.carrier) : SemanticCore.Mem S z (self.typeLower x) ↔ ∀ (w : S.carrier), SemanticCore.Mem S (self.kPair w (self.singleton z)) x

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

Extract the complete semantic Skolem kernel from a literal Hailperin model.

Equations

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