NF weak partition development: NFStandard.ToHailperin.

This file proves the finite, semantic half of the equivalence between the ordinary NF axioms and Metamath's Hailperin-derived eleven-axiom presentation. The class notation in the literal Hailperin sentences is extensional notation, so the only substantive shared construction is the usual Kuratowski ordered pair.

def NFChoice.Foundation.NFStandard.singletonPred : Formula 2

The stratified predicate defining a singleton with one parameter.

Equations

• NFChoice.Foundation.NFStandard.singletonPred = NFChoice.Foundation.Formula.equal 0 1

theorem NFChoice.Foundation.NFStandard.singletonPred_stratified : singletonPred.Stratified

def NFChoice.Foundation.NFStandard.unorderedPairPred : Formula 3

The stratified predicate defining an unordered pair with two parameters.

Equations

• NFChoice.Foundation.NFStandard.unorderedPairPred = (NFChoice.Foundation.Formula.equal 0 1).disj (NFChoice.Foundation.Formula.equal 0 2)

theorem NFChoice.Foundation.NFStandard.unorderedPairPred_stratified : unorderedPairPred.Stratified

noncomputable def NFChoice.Foundation.NFStandard.singletonObj {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) (a : S.carrier) : S.carrier

A chosen singleton supplied by NF comprehension.

Equations

• NFChoice.Foundation.NFStandard.singletonObj hNF a = Classical.choose ⋯

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_singletonObj {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) (a z : S.carrier) : SemanticCore.Mem S z (singletonObj hNF a) ↔ z = a

noncomputable def NFChoice.Foundation.NFStandard.unorderedPairObj {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) (a b : S.carrier) : S.carrier

A chosen unordered pair supplied by NF comprehension.

Equations

• NFChoice.Foundation.NFStandard.unorderedPairObj hNF a b = Classical.choose ⋯

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_unorderedPairObj {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) (a b z : S.carrier) : SemanticCore.Mem S z (unorderedPairObj hNF a b) ↔ z = a ∨ z = b

noncomputable def NFChoice.Foundation.NFStandard.kPairObj {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) (a b : S.carrier) : S.carrier

The Kuratowski ordered pair {{a},{a,b}}.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_kPairObj {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) (a b z : S.carrier) : SemanticCore.Mem S z (kPairObj hNF a b) ↔ z = singletonObj hNF a ∨ z = unorderedPairObj hNF a b

theorem NFChoice.Foundation.NFStandard.singletonObj_injective {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : Function.Injective (singletonObj hNF)

theorem NFChoice.Foundation.NFStandard.unorderedPairObj_eq_iff {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) (a b c d : S.carrier) : unorderedPairObj hNF a b = unorderedPairObj hNF c d ↔ a = c ∧ b = d ∨ a = d ∧ b = c

theorem NFChoice.Foundation.NFStandard.singletonObj_eq_unorderedPairObj_iff {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) (a b c : S.carrier) : singletonObj hNF a = unorderedPairObj hNF b c ↔ b = a ∧ c = a

theorem NFChoice.Foundation.NFStandard.kPairObj_injective {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) {a b c d : S.carrier} (h : kPairObj hNF a b = kPairObj hNF c d) : a = c ∧ b = d

noncomputable def NFChoice.Foundation.NFStandard.evalLiteralClass {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) {n : ℕ} (xs : DVec S.carrier n) : ExactLiteralTrial.LiteralClass n → S.carrier

The actual set denoted by an exact literal class expression in an NF model.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Foundation.NFStandard.evalLiteralClass hNF xs (NFChoice.Foundation.ExactLiteralTrial.LiteralClass.setVar i) = NFChoice.SemanticCore.Lowering.lookup xs i
• NFChoice.Foundation.NFStandard.evalLiteralClass hNF xs A.singleton = NFChoice.Foundation.NFStandard.singletonObj hNF (NFChoice.Foundation.NFStandard.evalLiteralClass hNF xs A)

theorem NFChoice.Foundation.NFStandard.literalClassSem_iff_mem_eval {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) {n : ℕ} (xs : DVec S.carrier n) (A : ExactLiteralTrial.LiteralClass n) (z : S.carrier) : Compiler.NFCompactLeafSemanticAdapters.LiteralClassSem xs A z ↔ SemanticCore.Mem S z (evalLiteralClass hNF xs A)

Literal class semantics is membership in its canonically represented set.

theorem NFChoice.Foundation.NFStandard.formulaHolds_setEqClass_iff {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) {n : ℕ} (xs : DVec S.carrier n) (r : Fin n) (A : ExactLiteralTrial.LiteralClass n) : SemanticCore.Lowering.FormulaHolds S xs (ExactLiteralTrial.LiteralClass.setEqClass r A) ↔ SemanticCore.Lowering.lookup xs r = evalLiteralClass hNF xs A

theorem NFChoice.Foundation.NFStandard.formulaHolds_classMemSet_iff {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) {n : ℕ} (xs : DVec S.carrier n) (A : ExactLiteralTrial.LiteralClass n) (r : Fin n) : SemanticCore.Lowering.FormulaHolds S xs (A.classMemSet r) ↔ SemanticCore.Mem S (evalLiteralClass hNF xs A) (SemanticCore.Lowering.lookup xs r)

theorem NFChoice.Foundation.NFStandard.stratifiedBy_conj_iff {n : ℕ} (ty : Fin n → ℤ) (p q : Formula n) : Formula.StratifiedBy ty (p.conj q) ↔ Formula.StratifiedBy ty p ∧ Formula.StratifiedBy ty q

theorem NFChoice.Foundation.NFStandard.stratifiedBy_disj_iff {n : ℕ} (ty : Fin n → ℤ) (p q : Formula n) : Formula.StratifiedBy ty (p.disj q) ↔ Formula.StratifiedBy ty p ∧ Formula.StratifiedBy ty q

theorem NFChoice.Foundation.NFStandard.stratifiedBy_biimp_iff {n : ℕ} (ty : Fin n → ℤ) (p q : Formula n) : Formula.StratifiedBy ty (p.biimp q) ↔ Formula.StratifiedBy ty p ∧ Formula.StratifiedBy ty q

theorem NFChoice.Foundation.NFStandard.stratifiedBy_ex_iff {n : ℕ} (ty : Fin n → ℤ) (p : Formula (n + 1)) : Formula.StratifiedBy ty p.ex ↔ ∃ (k : ℤ), Formula.StratifiedBy (fun (i : Fin (n + 1)) => Fin.cases k ty i) p

theorem NFChoice.Foundation.NFStandard.stratifiedBy_renameVars {n m : ℕ} (rho : Fin n → Fin m) (smallTy : Fin n → ℤ) (largeTy : Fin m → ℤ) (hTy : ∀ (i : Fin n), largeTy (rho i) = smallTy i) (p : Formula n) (hp : Formula.StratifiedBy smallTy p) : Formula.StratifiedBy largeTy (ExactLiteralTrial.Formula.renameVars rho p)

theorem NFChoice.Foundation.NFStandard.stratifiedBy_liftClassPredicate {n : ℕ} (ty : Fin n → ℤ) (memberTy representedTy : ℤ) (p : Formula (n + 1)) (hp : Formula.StratifiedBy (fun (i : Fin (n + 1)) => Fin.cases memberTy ty i) p) : Formula.StratifiedBy (fun (i : Fin (n + 1 + 1)) => Fin.cases memberTy (fun (i : Fin (n + 1)) => Fin.cases representedTy ty i) i) (ExactLiteralTrial.Formula.liftClassPredicate p)

theorem NFChoice.Foundation.NFStandard.stratifiedBy_eqCandidateToPredicate {n : ℕ} (ty : Fin n → ℤ) (memberTy : ℤ) (p : Formula (n + 1)) (hp : Formula.StratifiedBy (fun (i : Fin (n + 1)) => Fin.cases memberTy ty i) p) : Formula.StratifiedBy (fun (i : Fin (n + 1)) => Fin.cases (memberTy + 1) ty i) (ExactLiteralTrial.Formula.eqCandidateToPredicate p)

inductive NFChoice.Foundation.NFStandard.LiteralClass.Typed {n : ℕ} (ty : Fin n → ℤ) : ExactLiteralTrial.LiteralClass n → ℤ → Prop

A literal class is typed by the type of one of its members.

• setVar {n : ℕ} {ty : Fin n → ℤ} (i : Fin n) (k : ℤ) (h : ty i = k + 1) : Typed ty (ExactLiteralTrial.LiteralClass.setVar i) k
• singleton {n : ℕ} {ty : Fin n → ℤ} {A : ExactLiteralTrial.LiteralClass n} {k : ℤ} : Typed ty A k → Typed ty A.singleton (k + 1)
• unorderedPair {n : ℕ} {ty : Fin n → ℤ} {A B : ExactLiteralTrial.LiteralClass n} {k : ℤ} : Typed ty A k → Typed ty B k → Typed ty (A.unorderedPair B) (k + 1)
• kPair {n : ℕ} {ty : Fin n → ℤ} {A B : ExactLiteralTrial.LiteralClass n} {k : ℤ} : Typed ty A k → Typed ty B k → Typed ty (A.kPair B) (k + 2)

theorem NFChoice.Foundation.NFStandard.LiteralClass.membership_stratifiedBy {n : ℕ} {ty : Fin n → ℤ} {A : ExactLiteralTrial.LiteralClass n} {k : ℤ} (hA : Typed ty A k) : Formula.StratifiedBy (fun (i : Fin (n + 1)) => Fin.cases k ty i) A.membership

theorem NFChoice.Foundation.NFStandard.LiteralClass.classEq_stratifiedBy {n : ℕ} {ty : Fin n → ℤ} {A B : ExactLiteralTrial.LiteralClass n} {k : ℤ} (hA : Typed ty A k) (hB : Typed ty B k) : Formula.StratifiedBy ty (A.classEq B)

theorem NFChoice.Foundation.NFStandard.LiteralClass.setEqClass_stratifiedBy {n : ℕ} {ty : Fin n → ℤ} {x : Fin n} {A : ExactLiteralTrial.LiteralClass n} {k : ℤ} (hx : ty x = k + 1) (hA : Typed ty A k) : Formula.StratifiedBy ty (ExactLiteralTrial.LiteralClass.setEqClass x A)

theorem NFChoice.Foundation.NFStandard.LiteralClass.classMemSet_stratifiedBy {n : ℕ} {ty : Fin n → ℤ} {A : ExactLiteralTrial.LiteralClass n} {r : Fin n} {k : ℤ} (hA : Typed ty A k) (hr : ty r = k + 2) : Formula.StratifiedBy ty (A.classMemSet r)

Strong unary predicates whose comprehension sets witness the eleven axioms.

def NFChoice.Foundation.NFStandard.ninPred : Formula 3

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

Equations

• NFChoice.Foundation.NFStandard.ninPred = ((NFChoice.Foundation.Formula.mem 0 2).conj (NFChoice.Foundation.Formula.mem 0 1)).neg

def NFChoice.Foundation.NFStandard.xpPred : Formula 2

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

Equations

• NFChoice.Foundation.NFStandard.xpPred = ((NFChoice.Foundation.ExactLiteralTrial.literalKPair 2 1 0).conj (NFChoice.Foundation.Formula.mem 0 3)).ex.ex

def NFChoice.Foundation.NFStandard.oneCPred : Formula 1

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

Equations

• NFChoice.Foundation.NFStandard.oneCPred = NFChoice.Foundation.Formula.isSomeSingleton 0

def NFChoice.Foundation.NFStandard.cnvPred : Formula 2

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

Equations

• NFChoice.Foundation.NFStandard.cnvPred = ((NFChoice.Foundation.ExactLiteralTrial.literalKPair 2 1 0).conj (NFChoice.Foundation.ExactLiteralTrial.literalPairMem 0 1 3)).ex.ex

def NFChoice.Foundation.NFStandard.ssetPred : Formula 1

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

Equations

• NFChoice.Foundation.NFStandard.ssetPred = ((NFChoice.Foundation.ExactLiteralTrial.literalKPair 2 1 0).conj (NFChoice.Foundation.Formula.subset 1 0)).ex.ex

def NFChoice.Foundation.NFStandard.siPred : Formula 2

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

Equations

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

def NFChoice.Foundation.NFStandard.ins2Pred : Formula 2

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

Equations

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

def NFChoice.Foundation.NFStandard.ins3Pred : Formula 2

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

Equations

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

def NFChoice.Foundation.NFStandard.typeLowerPred : Formula 2

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

Equations

• NFChoice.Foundation.NFStandard.typeLowerPred = (NFChoice.Foundation.ExactLiteralTrial.literalPairSingletonSecondMem 0 1 2).all

theorem NFChoice.Foundation.NFStandard.ninPred_stratified : ninPred.Stratified

theorem NFChoice.Foundation.NFStandard.oneCPred_stratified : oneCPred.Stratified

theorem NFChoice.Foundation.NFStandard.xpPred_stratified : xpPred.Stratified

theorem NFChoice.Foundation.NFStandard.cnvPred_stratified : cnvPred.Stratified

theorem NFChoice.Foundation.NFStandard.ssetPred_stratified : ssetPred.Stratified

theorem NFChoice.Foundation.NFStandard.siPred_stratified : siPred.Stratified

theorem NFChoice.Foundation.NFStandard.ins2Pred_stratified : ins2Pred.Stratified

theorem NFChoice.Foundation.NFStandard.ins3Pred_stratified : ins3Pred.Stratified

theorem NFChoice.Foundation.NFStandard.typeLowerPred_stratified : typeLowerPred.Stratified

noncomputable def NFChoice.Foundation.NFStandard.comprehensionObj {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) {n : ℕ} (p : Formula (n + 1)) (hp : p.Stratified) (xs : DVec S.carrier n) : S.carrier

A named choice of the set delivered by an NF comprehension instance.

Equations

• NFChoice.Foundation.NFStandard.comprehensionObj hNF p hp xs = Classical.choose ⋯

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_comprehensionObj {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) {n : ℕ} (p : Formula (n + 1)) (hp : p.Stratified) (xs : DVec S.carrier n) (z : S.carrier) : SemanticCore.Mem S z (comprehensionObj hNF p hp xs) ↔ SemanticCore.Lowering.FormulaHolds S (DVec.cons z xs) p

theorem NFChoice.Foundation.NFStandard.realizes_literalAxSn {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : Fol.realizeSentence S (ExactLiteralTrial.literalAxiomFormula HailperinAxiomName.axSn)

theorem NFChoice.Foundation.NFStandard.realizes_literalAxNin {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : Fol.realizeSentence S (ExactLiteralTrial.literalAxiomFormula HailperinAxiomName.axNin)

theorem NFChoice.Foundation.NFStandard.realizes_literalAx1c {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : Fol.realizeSentence S (ExactLiteralTrial.literalAxiomFormula HailperinAxiomName.ax1c)

theorem NFChoice.Foundation.NFStandard.realizes_literalAxXp {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : Fol.realizeSentence S (ExactLiteralTrial.literalAxiomFormula HailperinAxiomName.axXp)

theorem NFChoice.Foundation.NFStandard.realizes_literalAxExt {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : Fol.realizeSentence S (ExactLiteralTrial.literalAxiomFormula HailperinAxiomName.axExt)

theorem NFChoice.Foundation.NFStandard.realizes_literalAxTypeLower {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : Fol.realizeSentence S (ExactLiteralTrial.literalAxiomFormula HailperinAxiomName.axTypeLower)

theorem NFChoice.Foundation.NFStandard.realizes_literalAxCnv {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : Fol.realizeSentence S (ExactLiteralTrial.literalAxiomFormula HailperinAxiomName.axCnv)

theorem NFChoice.Foundation.NFStandard.realizes_literalAxSset {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : Fol.realizeSentence S (ExactLiteralTrial.literalAxiomFormula HailperinAxiomName.axSset)

theorem NFChoice.Foundation.NFStandard.realizes_literalAxSi {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : Fol.realizeSentence S (ExactLiteralTrial.literalAxiomFormula HailperinAxiomName.axSi)

theorem NFChoice.Foundation.NFStandard.realizes_literalAxIns2 {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : Fol.realizeSentence S (ExactLiteralTrial.literalAxiomFormula HailperinAxiomName.axIns2)

theorem NFChoice.Foundation.NFStandard.realizes_literalAxIns3 {S : Fol.Structure LNF} (hNF : Fol.allRealizeSentence S NF) : Fol.realizeSentence S (ExactLiteralTrial.literalAxiomFormula HailperinAxiomName.axIns3)

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

Every model of ordinary NF satisfies all eleven axioms of the literal Metamath Hailperin-derived presentation.