NF weak partition development: exact_literal_trial.NFChoiceExactLiteral.

This append-only trial gives the literal class-elimination boundary for the eleven finite NF axioms. In particular, a class expression is represented by its unary membership predicate. Nested class constructors are not replaced by existential assertions that their values are sets.

For example, the exact predicate saying that the set p is the Kuratowski class pair <<a,b>> is

forall u, u in p <-> (u = {a} or u = {a,b}),

where both displayed class equalities are themselves expanded extensionally. This differs from asserting the existence of sets s = {a} and q = {a,b}.

def NFChoice.Foundation.ExactLiteralTrial.Formula.renameVars {n m : ℕ} (rho : Fin n → Fin m) : Formula n → Formula m

Rename every free de Bruijn variable in the small formula language.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Foundation.ExactLiteralTrial.Formula.renameVars rho NFChoice.Foundation.Formula.falsum = NFChoice.Foundation.Formula.falsum
• NFChoice.Foundation.ExactLiteralTrial.Formula.renameVars rho (NFChoice.Foundation.Formula.equal x_1 y) = NFChoice.Foundation.Formula.equal (rho x_1) (rho y)
• NFChoice.Foundation.ExactLiteralTrial.Formula.renameVars rho (NFChoice.Foundation.Formula.mem x_1 y) = NFChoice.Foundation.Formula.mem (rho x_1) (rho y)

def NFChoice.Foundation.ExactLiteralTrial.Formula.liftClassPredicate {n : ℕ} (p : Formula (n + 1)) : Formula (n + 2)

Insert a new ambient variable at index one while retaining index zero as the membership candidate of a unary class predicate.

Equations

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

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

In context [x, ambient...], assert that the set variable x is extensionally equal to the class whose unary membership predicate is p.

Equations

• NFChoice.Foundation.ExactLiteralTrial.Formula.eqCandidateToPredicate p = ((NFChoice.Foundation.Formula.mem 0 1).biimp (NFChoice.Foundation.ExactLiteralTrial.Formula.liftClassPredicate p)).all

inductive NFChoice.Foundation.ExactLiteralTrial.LiteralClass : ℕ → Type

The class constructors occurring in the eleven source axioms.

• setVar {n : ℕ} : Fin n → LiteralClass n
• singleton {n : ℕ} : LiteralClass n → LiteralClass n
• unorderedPair {n : ℕ} : LiteralClass n → LiteralClass n → LiteralClass n
• kPair {n : ℕ} : LiteralClass n → LiteralClass n → LiteralClass n

@[irreducible]

def NFChoice.Foundation.ExactLiteralTrial.LiteralClass.membership {n : ℕ} : LiteralClass n → Formula (n + 1)

The unary membership predicate of a class expression. Its index zero is the candidate member; the n ambient set variables occupy indices one onward.

Equations

• One or more equations did not get rendered due to their size.
• (NFChoice.Foundation.ExactLiteralTrial.LiteralClass.setVar a).membership = NFChoice.Foundation.Formula.mem 0 a.succ
• A.singleton.membership = NFChoice.Foundation.ExactLiteralTrial.Formula.eqCandidateToPredicate A.membership

def NFChoice.Foundation.ExactLiteralTrial.LiteralClass.classEq {n : ℕ} (A B : LiteralClass n) : Formula n

Literal df-cleq: extensional equality of two class expressions.

Equations

• A.classEq B = (A.membership.biimp B.membership).all

def NFChoice.Foundation.ExactLiteralTrial.LiteralClass.setEqClass {n : ℕ} (x : Fin n) (A : LiteralClass n) : Formula n

Extensional equality of a set variable and a class expression.

Equations

• NFChoice.Foundation.ExactLiteralTrial.LiteralClass.setEqClass x A = (NFChoice.Foundation.ExactLiteralTrial.LiteralClass.setVar x).classEq A

def NFChoice.Foundation.ExactLiteralTrial.LiteralClass.classMemSet {n : ℕ} (A : LiteralClass n) (r : Fin n) : Formula n

Literal df-clel when the right side is a set variable: A e. r <-> exists x, (x = A and x e. r).

Equations

• A.classMemSet r = ((NFChoice.Foundation.ExactLiteralTrial.Formula.eqCandidateToPredicate A.membership).conj (NFChoice.Foundation.Formula.mem 0 r.succ)).ex

Exact relational readings of the source class constructors.

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

Proof-translation construction identified upstream as literalSingleton.

Equations

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

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

Proof-translation construction identified upstream as literalUnorderedPair.

Equations

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

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

Proof-translation construction identified upstream as literalKPair.

Equations

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

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

Proof-translation construction identified upstream as literalPairMem.

Equations

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

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

Proof-translation construction identified upstream as literalDoubleSingleton.

Equations

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

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

Proof-translation construction identified upstream as literalSingletonPairMem.

Equations

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

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

Proof-translation construction identified upstream as literalInsertedPairMem.

Equations

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

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

Proof-translation construction identified upstream as literalPairSingletonSecondMem.

Equations

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

The following are the universal closures of the source token strings. Every constructor-bearing subexpression is interpreted by LiteralClass.membership, so the output contains only logical equality and the sole membership relation.

def NFChoice.Foundation.ExactLiteralTrial.literalAxExt : Sentence

ax-ext: ( A. z ( z e. x <-> z e. y ) -> x = y ).

Equations

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

def NFChoice.Foundation.ExactLiteralTrial.literalAxNin : Sentence

ax-nin: the source anti-conjunction (NAND) axiom.

Equations

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

def NFChoice.Foundation.ExactLiteralTrial.literalAxXp : Sentence

ax-xp: E. y A. z (z e. y <-> E. w E. t (z = <<w,t>> /\ t e. x)).

Equations

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

def NFChoice.Foundation.ExactLiteralTrial.literalAxCnv : Sentence

ax-cnv: E. y A. z A. w (<<z,w>> e. y <-> <<w,z>> e. x).

Equations

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

def NFChoice.Foundation.ExactLiteralTrial.literalAx1c : Sentence

ax-1c: E. x A. y (y e. x <-> E. z A. w (w e. y <-> w = z)).

Equations

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

def NFChoice.Foundation.ExactLiteralTrial.literalAxSset : Sentence

ax-sset: E. x A. y A. z (<<y,z>> e. x <-> A. w(w e. y -> w e. z)).

Equations

• NFChoice.Foundation.ExactLiteralTrial.literalAxSset = ((NFChoice.Foundation.ExactLiteralTrial.literalPairMem 1 0 2).biimp (NFChoice.Foundation.Formula.subset 1 0)).all.all.ex

def NFChoice.Foundation.ExactLiteralTrial.literalAxSi : Sentence

ax-si: E. y A. z A. w (<<{z},{w}>> e. y <-> <<z,w>> e. x).

Equations

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

def NFChoice.Foundation.ExactLiteralTrial.literalAxIns2 : Sentence

ax-ins2: the inserted-pair biconditional ending in <<z,t>> e. x.

Equations

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

def NFChoice.Foundation.ExactLiteralTrial.literalAxIns3 : Sentence

ax-ins3: the inserted-pair biconditional ending in <<z,w>> e. x.

Equations

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

def NFChoice.Foundation.ExactLiteralTrial.literalAxTypeLower : Sentence

ax-typlower: E. y A. z (z e. y <-> A. w <<w,{z}>> e. x).

Equations

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

def NFChoice.Foundation.ExactLiteralTrial.literalAxSn : Sentence

ax-sn: E. y A. z (z e. y <-> z = x).

Equations

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

Token-by-token equations, deliberately proved by reduction only.

theorem NFChoice.Foundation.ExactLiteralTrial.axExt_source_equation : literalAxExt = (((Formula.mem 0 2).biimp (Formula.mem 0 1)).all.imp (Formula.equal 1 0)).all.all

theorem NFChoice.Foundation.ExactLiteralTrial.axNin_source_equation : literalAxNin = ((Formula.mem 0 1).biimp ((Formula.mem 0 3).conj (Formula.mem 0 2)).neg).all.ex.all.all

theorem NFChoice.Foundation.ExactLiteralTrial.axXp_source_equation : literalAxXp = ((Formula.mem 0 1).biimp ((literalKPair 2 1 0).conj (Formula.mem 0 4)).ex.ex).all.ex.all

theorem NFChoice.Foundation.ExactLiteralTrial.axCnv_source_equation : literalAxCnv = ((literalPairMem 1 0 2).biimp (literalPairMem 0 1 3)).all.all.ex.all

theorem NFChoice.Foundation.ExactLiteralTrial.ax1c_source_equation : literalAx1c = ((Formula.mem 0 1).biimp (Formula.isSomeSingleton 0)).all.ex

theorem NFChoice.Foundation.ExactLiteralTrial.axSset_source_equation : literalAxSset = ((literalPairMem 1 0 2).biimp (Formula.subset 1 0)).all.all.ex

theorem NFChoice.Foundation.ExactLiteralTrial.axSi_source_equation : literalAxSi = ((literalSingletonPairMem 1 0 2).biimp (literalPairMem 1 0 3)).all.all.ex.all

theorem NFChoice.Foundation.ExactLiteralTrial.axIns2_source_equation : literalAxIns2 = ((literalInsertedPairMem 2 1 0 3).biimp (literalPairMem 2 0 4)).all.all.all.ex.all

theorem NFChoice.Foundation.ExactLiteralTrial.axIns3_source_equation : literalAxIns3 = ((literalInsertedPairMem 2 1 0 3).biimp (literalPairMem 2 1 4)).all.all.all.ex.all

theorem NFChoice.Foundation.ExactLiteralTrial.axTypeLower_source_equation : literalAxTypeLower = ((Formula.mem 0 1).biimp (literalPairSingletonSecondMem 0 1 3).all).all.ex.all

theorem NFChoice.Foundation.ExactLiteralTrial.axSn_source_equation : literalAxSn = ((Formula.mem 0 1).biimp (Formula.equal 0 2)).all.ex.all

def NFChoice.Foundation.ExactLiteralTrial.literalAxiomSyntax : HailperinAxiomName → Sentence

Literal sentence data, indexed by the exact eleven source labels.

Equations

• NFChoice.Foundation.ExactLiteralTrial.literalAxiomSyntax NFChoice.Foundation.HailperinAxiomName.axExt = NFChoice.Foundation.ExactLiteralTrial.literalAxExt
• NFChoice.Foundation.ExactLiteralTrial.literalAxiomSyntax NFChoice.Foundation.HailperinAxiomName.axNin = NFChoice.Foundation.ExactLiteralTrial.literalAxNin
• NFChoice.Foundation.ExactLiteralTrial.literalAxiomSyntax NFChoice.Foundation.HailperinAxiomName.axXp = NFChoice.Foundation.ExactLiteralTrial.literalAxXp
• NFChoice.Foundation.ExactLiteralTrial.literalAxiomSyntax NFChoice.Foundation.HailperinAxiomName.axCnv = NFChoice.Foundation.ExactLiteralTrial.literalAxCnv
• NFChoice.Foundation.ExactLiteralTrial.literalAxiomSyntax NFChoice.Foundation.HailperinAxiomName.ax1c = NFChoice.Foundation.ExactLiteralTrial.literalAx1c
• NFChoice.Foundation.ExactLiteralTrial.literalAxiomSyntax NFChoice.Foundation.HailperinAxiomName.axSset = NFChoice.Foundation.ExactLiteralTrial.literalAxSset
• NFChoice.Foundation.ExactLiteralTrial.literalAxiomSyntax NFChoice.Foundation.HailperinAxiomName.axSi = NFChoice.Foundation.ExactLiteralTrial.literalAxSi
• NFChoice.Foundation.ExactLiteralTrial.literalAxiomSyntax NFChoice.Foundation.HailperinAxiomName.axIns2 = NFChoice.Foundation.ExactLiteralTrial.literalAxIns2
• NFChoice.Foundation.ExactLiteralTrial.literalAxiomSyntax NFChoice.Foundation.HailperinAxiomName.axIns3 = NFChoice.Foundation.ExactLiteralTrial.literalAxIns3
• NFChoice.Foundation.ExactLiteralTrial.literalAxiomSyntax NFChoice.Foundation.HailperinAxiomName.axTypeLower = NFChoice.Foundation.ExactLiteralTrial.literalAxTypeLower
• NFChoice.Foundation.ExactLiteralTrial.literalAxiomSyntax NFChoice.Foundation.HailperinAxiomName.axSn = NFChoice.Foundation.ExactLiteralTrial.literalAxSn

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

Proof-translation construction identified upstream as literalAxiomFormula.

Equations

• NFChoice.Foundation.ExactLiteralTrial.literalAxiomFormula name = NFChoice.Foundation.Formula.toFlypitch (NFChoice.Foundation.ExactLiteralTrial.literalAxiomSyntax name)

@[reducible, inline]

abbrev NFChoice.Foundation.ExactLiteralTrial.LiteralHailperinNF : Fol.SentTheory LNF

Proof-translation construction identified upstream as LiteralHailperinNF.

Equations

• NFChoice.Foundation.ExactLiteralTrial.LiteralHailperinNF = Set.range NFChoice.Foundation.ExactLiteralTrial.literalAxiomFormula

theorem NFChoice.Foundation.ExactLiteralTrial.literalAxiom_mem (name : HailperinAxiomName) : literalAxiomFormula name ∈ LiteralHailperinNF

@[reducible, inline]

abbrev NFChoice.Foundation.ExactLiteralTrial.LiteralSourceNFProvesNotChoiceTarget (sourceChoiceNF : Fol.sentence LNF) : Prop

Proof-translation construction identified upstream as LiteralSourceNFProvesNotChoiceTarget.

Equations

• NFChoice.Foundation.ExactLiteralTrial.LiteralSourceNFProvesNotChoiceTarget sourceChoiceNF = NFChoice.Foundation.ExactLiteralTrial.LiteralHailperinNF.sprovable (NFChoice.Fol.bdNot sourceChoiceNF)