NF weak partition development: NFChoiceFoundation.Basic.

This file fixes the trusted first-order boundary for the NF choice experiment. There are no nonlogical function symbols and membership is the sole nonlogical predicate. Equality is Flypitch's logical equality.

inductive NFChoice.Foundation.LNFRelation : ℕ → Type

The only nonlogical relation symbol of the language of NF.

• mem : LNFRelation 2

def NFChoice.Foundation.LNF : Fol.Language

The membership-only first-order language used for NF.

Equations

• NFChoice.Foundation.LNF = { functions := fun (x : ℕ) => Empty, relations := NFChoice.Foundation.LNFRelation }

Formula n is a small intrinsically scoped front end. Its variables are de Bruijn indices in Fin n. It has exactly Flypitch's primitive logical constructors, specialized to the membership-only language.

inductive NFChoice.Foundation.Formula : ℕ → Type

Intrinsically scoped membership-only first-order formulas.

• falsum {n : ℕ} : Formula n
• equal {n : ℕ} : Fin n → Fin n → Formula n
• mem {n : ℕ} : Fin n → Fin n → Formula n
• imp {n : ℕ} : Formula n → Formula n → Formula n
• all {n : ℕ} : Formula (n + 1) → Formula n

@[reducible, inline]

abbrev NFChoice.Foundation.Sentence : Type

A closed membership-only formula.

Equations

• NFChoice.Foundation.Sentence = NFChoice.Foundation.Formula 0

def NFChoice.Foundation.Formula.neg {n : ℕ} (p : Formula n) : Formula n

Negation, with falsity and implication as primitives.

Equations

• p.neg = p.imp NFChoice.Foundation.Formula.falsum

def NFChoice.Foundation.Formula.conj {n : ℕ} (p q : Formula n) : Formula n

Classical conjunction in Flypitch's primitive basis.

Equations

• p.conj q = (p.imp q.neg).neg

def NFChoice.Foundation.Formula.disj {n : ℕ} (p q : Formula n) : Formula n

Classical disjunction in Flypitch's primitive basis.

Equations

• p.disj q = p.neg.imp q

def NFChoice.Foundation.Formula.biimp {n : ℕ} (p q : Formula n) : Formula n

Biconditional.

Equations

• p.biimp q = (p.imp q).conj (q.imp p)

def NFChoice.Foundation.Formula.ex {n : ℕ} (p : Formula (n + 1)) : Formula n

Existential quantification, defined from universal quantification.

Equations

• p.ex = p.neg.all.neg

def NFChoice.Foundation.Formula.memToFlypitch {n : ℕ} (x y : Fol.boundedTerm LNF n) : Fol.boundedFormula LNF n

Apply the sole binary relation symbol to two bounded variables.

Equations

• NFChoice.Foundation.Formula.memToFlypitch x y = ((NFChoice.Fol.bd_rel NFChoice.Foundation.LNFRelation.mem).bd_apprel x).bd_apprel y

def NFChoice.Foundation.Formula.toFlypitch {n : ℕ} : Formula n → Fol.boundedFormula LNF n

Translate the small front end into Flypitch's bounded syntax.

Equations

• NFChoice.Foundation.Formula.falsum.toFlypitch = NFChoice.Fol.bd_falsum
• (NFChoice.Foundation.Formula.equal x_3 y).toFlypitch = NFChoice.Fol.bd_equal (NFChoice.Fol.bd_var x_3) (NFChoice.Fol.bd_var y)
• (NFChoice.Foundation.Formula.mem x_3 y).toFlypitch = NFChoice.Foundation.Formula.memToFlypitch (NFChoice.Fol.bd_var x_3) (NFChoice.Fol.bd_var y)
• (p.imp q).toFlypitch = NFChoice.Fol.bd_imp p.toFlypitch q.toFlypitch
• p.all.toFlypitch = NFChoice.Fol.bd_all p.toFlypitch

def NFChoice.Foundation.Formula.singleton {n : ℕ} (s a : Fin n) : Formula n

s is the singleton of a.

Equations

• NFChoice.Foundation.Formula.singleton s a = ((NFChoice.Foundation.Formula.mem 0 s.succ).biimp (NFChoice.Foundation.Formula.equal 0 a.succ)).all

def NFChoice.Foundation.Formula.unorderedPair {n : ℕ} (p a b : Fin n) : Formula n

p is the unordered pair of a and b.

Equations

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

def NFChoice.Foundation.Formula.subset {n : ℕ} (a b : Fin n) : Formula n

a is a subset of b.

Equations

• NFChoice.Foundation.Formula.subset a b = ((NFChoice.Foundation.Formula.mem 0 a.succ).imp (NFChoice.Foundation.Formula.mem 0 b.succ)).all

def NFChoice.Foundation.Formula.nonempty {n : ℕ} (a : Fin n) : Formula n

a has an element.

Equations

• NFChoice.Foundation.Formula.nonempty a = (NFChoice.Foundation.Formula.mem 0 a.succ).ex

def NFChoice.Foundation.Formula.isSomeSingleton {n : ℕ} (y : Fin n) : Formula n

y is a singleton (of some object).

Equations

• NFChoice.Foundation.Formula.isSomeSingleton y = (NFChoice.Foundation.Formula.singleton y.succ 0).ex

def NFChoice.Foundation.Formula.isKPair {n : ℕ} (p a b : Fin n) : Formula n

p is the Kuratowski ordered pair of a and b.

Equations

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

def NFChoice.Foundation.Formula.equalKPair {n : ℕ} (z a b : Fin n) : Formula n

z is the Kuratowski ordered pair of a and b.

Equations

• NFChoice.Foundation.Formula.equalKPair z a b = ((NFChoice.Foundation.Formula.isKPair 0 a.succ b.succ).conj (NFChoice.Foundation.Formula.equal z.succ 0)).ex

def NFChoice.Foundation.Formula.pairMem {n : ℕ} (a b r : Fin n) : Formula n

The Kuratowski ordered pair of a and b belongs to r.

Equations

• NFChoice.Foundation.Formula.pairMem a b r = ((NFChoice.Foundation.Formula.isKPair 0 a.succ b.succ).conj (NFChoice.Foundation.Formula.mem 0 r.succ)).ex

def NFChoice.Foundation.Formula.doubleSingleton {n : ℕ} (d a : Fin n) : Formula n

d is the double singleton of a.

Equations

• NFChoice.Foundation.Formula.doubleSingleton d a = ((NFChoice.Foundation.Formula.singleton 0 a.succ).conj (NFChoice.Foundation.Formula.singleton d.succ 0)).ex

def NFChoice.Foundation.Formula.singletonPairMem {n : ℕ} (a b r : Fin n) : Formula n

The ordered pair of the singletons of a and b belongs to r.

Equations

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

def NFChoice.Foundation.Formula.insertedPairMem {n : ℕ} (z w t r : Fin n) : Formula n

<< {{z}}, <<w,t>> >> belongs to r.

Equations

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

def NFChoice.Foundation.Formula.pairSingletonSecondMem {n : ℕ} (a z r : Fin n) : Formula n

The ordered pair of a and the singleton of z belongs to r.

Equations

• NFChoice.Foundation.Formula.pairSingletonSecondMem a z r = ((NFChoice.Foundation.Formula.singleton 0 z.succ).conj (NFChoice.Foundation.Formula.pairMem a.succ 0 r.succ)).ex

The direct first-order well-order predicate used in ChoiceNF.

def NFChoice.Foundation.Formula.reflexiveOn {n : ℕ} (r a : Fin n) : Formula n

Proof-translation construction identified upstream as reflexiveOn.

Equations

• NFChoice.Foundation.Formula.reflexiveOn r a = ((NFChoice.Foundation.Formula.mem 0 a.succ).imp (NFChoice.Foundation.Formula.pairMem 0 0 r.succ)).all

def NFChoice.Foundation.Formula.transitiveOn {n : ℕ} (r a : Fin n) : Formula n

Proof-translation construction identified upstream as transitiveOn.

Equations

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

def NFChoice.Foundation.Formula.antisymmetricOn {n : ℕ} (r a : Fin n) : Formula n

Proof-translation construction identified upstream as antisymmetricOn.

Equations

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

def NFChoice.Foundation.Formula.connectedOn {n : ℕ} (r a : Fin n) : Formula n

Proof-translation construction identified upstream as connectedOn.

Equations

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

def NFChoice.Foundation.Formula.foundedOn {n : ℕ} (r a : Fin n) : Formula n

Proof-translation construction identified upstream as foundedOn.

Equations

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

def NFChoice.Foundation.Formula.wellOrders {n : ℕ} (r a : Fin n) : Formula n

r well-orders a, matching the order/foundation conventions of df-we.

Equations

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

The eleven closed NF axioms below are the nf.mm source axioms ax-ext, ax-nin, ax-xp, ax-cnv, ax-1c, ax-sset, ax-si, ax-ins2, ax-ins3, ax-typlower, and ax-sn. Set-builder notation, singletons, and ordered pairs are expanded into equality and membership.

def NFChoice.Foundation.axExt : Sentence

Proof-translation construction identified upstream as axExt.

Equations

• NFChoice.Foundation.axExt = (((NFChoice.Foundation.Formula.mem 0 2).biimp (NFChoice.Foundation.Formula.mem 0 1)).all.imp (NFChoice.Foundation.Formula.equal 1 0)).all.all

def NFChoice.Foundation.axNin : Sentence

Proof-translation construction identified upstream as axNin.

Equations

• NFChoice.Foundation.axNin = ((NFChoice.Foundation.Formula.mem 0 1).biimp ((NFChoice.Foundation.Formula.mem 0 3).conj (NFChoice.Foundation.Formula.mem 0 2)).neg).all.ex.all.all

def NFChoice.Foundation.axXp : Sentence

Proof-translation construction identified upstream as axXp.

Equations

• NFChoice.Foundation.axXp = ((NFChoice.Foundation.Formula.mem 0 1).biimp ((NFChoice.Foundation.Formula.equalKPair 2 1 0).conj (NFChoice.Foundation.Formula.mem 0 4)).ex.ex).all.ex.all

def NFChoice.Foundation.axCnv : Sentence

Proof-translation construction identified upstream as axCnv.

Equations

• NFChoice.Foundation.axCnv = ((NFChoice.Foundation.Formula.pairMem 1 0 2).biimp (NFChoice.Foundation.Formula.pairMem 0 1 3)).all.all.ex.all

def NFChoice.Foundation.ax1c : Sentence

Proof-translation construction identified upstream as ax1c.

Equations

• NFChoice.Foundation.ax1c = ((NFChoice.Foundation.Formula.mem 0 1).biimp (NFChoice.Foundation.Formula.isSomeSingleton 0)).all.ex

def NFChoice.Foundation.axSset : Sentence

Proof-translation construction identified upstream as axSset.

Equations

• NFChoice.Foundation.axSset = ((NFChoice.Foundation.Formula.pairMem 1 0 2).biimp (NFChoice.Foundation.Formula.subset 1 0)).all.all.ex

def NFChoice.Foundation.axSi : Sentence

Proof-translation construction identified upstream as axSi.

Equations

• NFChoice.Foundation.axSi = ((NFChoice.Foundation.Formula.singletonPairMem 1 0 2).biimp (NFChoice.Foundation.Formula.pairMem 1 0 3)).all.all.ex.all

def NFChoice.Foundation.axIns2 : Sentence

Proof-translation construction identified upstream as axIns2.

Equations

• NFChoice.Foundation.axIns2 = ((NFChoice.Foundation.Formula.insertedPairMem 2 1 0 3).biimp (NFChoice.Foundation.Formula.pairMem 2 0 4)).all.all.all.ex.all

def NFChoice.Foundation.axIns3 : Sentence

Proof-translation construction identified upstream as axIns3.

Equations

• NFChoice.Foundation.axIns3 = ((NFChoice.Foundation.Formula.insertedPairMem 2 1 0 3).biimp (NFChoice.Foundation.Formula.pairMem 2 1 4)).all.all.all.ex.all

def NFChoice.Foundation.axTypeLower : Sentence

Proof-translation construction identified upstream as axTypeLower.

Equations

• NFChoice.Foundation.axTypeLower = ((NFChoice.Foundation.Formula.mem 0 1).biimp (NFChoice.Foundation.Formula.pairSingletonSecondMem 0 1 3).all).all.ex.all

def NFChoice.Foundation.axSn : Sentence

The singleton-existence axiom added to Metamath's Hailperin-derived NF basis. Metamath credits contributor SF on 12 January 2015; it identifies this as an addition missing from Hailperin's presentation. See https://us.metamath.org/nfeuni/ax-sn.html.

Equations

• NFChoice.Foundation.axSn = ((NFChoice.Foundation.Formula.mem 0 1).biimp (NFChoice.Foundation.Formula.equal 0 2)).all.ex.all

inductive NFChoice.Foundation.HailperinAxiomName : Type

The exact eleven source labels in the finite NF basis.

• axExt : HailperinAxiomName
• axNin : HailperinAxiomName
• axXp : HailperinAxiomName
• axCnv : HailperinAxiomName
• ax1c : HailperinAxiomName
• axSset : HailperinAxiomName
• axSi : HailperinAxiomName
• axIns2 : HailperinAxiomName
• axIns3 : HailperinAxiomName
• axTypeLower : HailperinAxiomName
• axSn : HailperinAxiomName

@[instance_reducible]

instance NFChoice.Foundation.instDecidableEqHailperinAxiomName : DecidableEq HailperinAxiomName

Equations

• NFChoice.Foundation.instDecidableEqHailperinAxiomName x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance NFChoice.Foundation.instReprHailperinAxiomName : Repr HailperinAxiomName

Equations

• NFChoice.Foundation.instReprHailperinAxiomName = { reprPrec := NFChoice.Foundation.instReprHailperinAxiomName.repr }

def NFChoice.Foundation.instReprHailperinAxiomName.repr : HailperinAxiomName → ℕ → Std.Format

Equations

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

def NFChoice.Foundation.axiomSyntax : HailperinAxiomName → Sentence

The closed membership-only sentence named by each source axiom.

Equations

• NFChoice.Foundation.axiomSyntax NFChoice.Foundation.HailperinAxiomName.axExt = NFChoice.Foundation.axExt
• NFChoice.Foundation.axiomSyntax NFChoice.Foundation.HailperinAxiomName.axNin = NFChoice.Foundation.axNin
• NFChoice.Foundation.axiomSyntax NFChoice.Foundation.HailperinAxiomName.axXp = NFChoice.Foundation.axXp
• NFChoice.Foundation.axiomSyntax NFChoice.Foundation.HailperinAxiomName.axCnv = NFChoice.Foundation.axCnv
• NFChoice.Foundation.axiomSyntax NFChoice.Foundation.HailperinAxiomName.ax1c = NFChoice.Foundation.ax1c
• NFChoice.Foundation.axiomSyntax NFChoice.Foundation.HailperinAxiomName.axSset = NFChoice.Foundation.axSset
• NFChoice.Foundation.axiomSyntax NFChoice.Foundation.HailperinAxiomName.axSi = NFChoice.Foundation.axSi
• NFChoice.Foundation.axiomSyntax NFChoice.Foundation.HailperinAxiomName.axIns2 = NFChoice.Foundation.axIns2
• NFChoice.Foundation.axiomSyntax NFChoice.Foundation.HailperinAxiomName.axIns3 = NFChoice.Foundation.axIns3
• NFChoice.Foundation.axiomSyntax NFChoice.Foundation.HailperinAxiomName.axTypeLower = NFChoice.Foundation.axTypeLower
• NFChoice.Foundation.axiomSyntax NFChoice.Foundation.HailperinAxiomName.axSn = NFChoice.Foundation.axSn

def NFChoice.Foundation.axiomFormula (name : HailperinAxiomName) : Fol.sentence LNF

The Flypitch sentence corresponding to a named NF axiom.

Equations

• NFChoice.Foundation.axiomFormula name = NFChoice.Foundation.Formula.toFlypitch (NFChoice.Foundation.axiomSyntax name)

@[reducible, inline]

abbrev NFChoice.Foundation.HailperinNF : Fol.SentTheory LNF

The eleven-sentence Metamath Hailperin-derived NF presentation, including axSn.

Equations

• NFChoice.Foundation.HailperinNF = Set.range NFChoice.Foundation.axiomFormula

theorem NFChoice.Foundation.axiom_mem_HailperinNF (name : HailperinAxiomName) : axiomFormula name ∈ HailperinNF

Every named axiom belongs to the finite theory.

def NFChoice.Foundation.ChoiceNFSyntax : Sentence

A direct membership-only statement that every set admits a well-order.

Equations

• NFChoice.Foundation.ChoiceNFSyntax = (NFChoice.Foundation.Formula.wellOrders 0 1).ex.all

def NFChoice.Foundation.ChoiceNF : Fol.sentence LNF

The choice sentence at the Flypitch boundary.

Equations

• NFChoice.Foundation.ChoiceNF = NFChoice.Foundation.Formula.toFlypitch NFChoice.Foundation.ChoiceNFSyntax

@[reducible, inline]

abbrev NFChoice.Foundation.SourceNFProvesNotChoiceTarget (SourceChoiceNF : Fol.sentence LNF) : Prop

The target interface for an exact source-generated choice sentence. A generated module supplies its concrete SourceChoiceNF; this foundation does not identify that sentence with the direct comparison sentence ChoiceNF.

Equations

• NFChoice.Foundation.SourceNFProvesNotChoiceTarget SourceChoiceNF = NFChoice.Foundation.HailperinNF.sprovable (NFChoice.Fol.bdNot SourceChoiceNF)

@[reducible, inline]

abbrev NFChoice.Foundation.DirectNFProvesNotChoiceTarget : Prop

The comparison target for the direct every-set-is-well-orderable sentence.

Equations

• NFChoice.Foundation.DirectNFProvesNotChoiceTarget = NFChoice.Foundation.SourceNFProvesNotChoiceTarget NFChoice.Foundation.ChoiceNF

theorem NFChoice.Foundation.source_not_choice_completeness_bridge (SourceChoiceNF : Fol.sentence LNF) : HailperinNF.sprovable (Fol.bdNot SourceChoiceNF) ↔ Fol.ssatisfied HailperinNF (Fol.bdNot SourceChoiceNF)

Completeness specialized to any exact source-generated choice sentence.

theorem NFChoice.Foundation.NF_not_choice_completeness_bridge : HailperinNF.sprovable (Fol.bdNot ChoiceNF) ↔ Fol.ssatisfied HailperinNF (Fol.bdNot ChoiceNF)

The exact syntactic/semantic bridge supplied by Gödel completeness.