NF weak partition development: NominalLogicalWrappers.

Nominal-syntax wrappers for the remaining primitive logical steps used by the Metamath replay. The wrappers whose source axiom carries a freshness or substitution side condition take the corresponding syntactic lowering identity explicitly. The certificate emitter can discharge these identities from its already checked $d/substitution data, without adding a formula axiom to the Flypitch theory.

def NFChoice.DirectNominalPrf.Nominal.gen {p : SemanticCore.Wff} (hp : NPrf p) (x : SemanticCore.Var) : NPrf (SemanticCore.Wff.all x p)

Metamath ax-gen: generalization of a closed nominal proof.

Equations

• NFChoice.DirectNominalPrf.Nominal.gen hp x rho = (⋯.mpr (hp (NFChoice.DirectNominalPrf.Nominal.bindRho rho x))).allI

def NFChoice.DirectNominalPrf.Nominal.ax5 (x : SemanticCore.Var) (p q : SemanticCore.Wff) : NPrf ((SemanticCore.Wff.all x (p.imp q)).imp ((SemanticCore.Wff.all x p).imp (SemanticCore.Wff.all x q)))

Metamath ax-5 (quantified implication).

Equations

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

def NFChoice.DirectNominalPrf.Nominal.freshIntroOfShift (p : SemanticCore.Wff) (x : SemanticCore.Var) (hShift : ∀ (rho : SemanticCore.Var → ℕ), lowerWff (bindRho rho x) p = Fol.liftFormula1 (lowerWff rho p)) : NPrf (p.imp (SemanticCore.Wff.all x p))

Fresh-variable introduction at nominal syntax. The equality is exactly the de-Bruijn shift certificate induced by the source $d x p condition.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.ax17OfShift (p : SemanticCore.Wff) (x : SemanticCore.Var) (hShift : ∀ (rho : SemanticCore.Var → ℕ), lowerWff (bindRho rho x) p = Fol.liftFormula1 (lowerWff rho p)) : NPrf (p.imp (SemanticCore.Wff.all x p))

Metamath ax-17, with its checked $d x p evidence compiled to shift.

Equations

• NFChoice.DirectNominalPrf.Nominal.ax17OfShift p x hShift = NFChoice.DirectNominalPrf.Nominal.freshIntroOfShift p x hShift

def NFChoice.DirectNominalPrf.Nominal.ax6OfShift (x : SemanticCore.Var) (p : SemanticCore.Wff) (hShift : ∀ (rho : SemanticCore.Var → ℕ), lowerWff (bindRho rho x) (SemanticCore.Wff.all x p).neg = Fol.liftFormula1 (lowerWff rho (SemanticCore.Wff.all x p).neg)) : NPrf ((SemanticCore.Wff.all x p).neg.imp (SemanticCore.Wff.all x (SemanticCore.Wff.all x p).neg))

Metamath ax-6. Its matrix ¬∀x.p is syntactically fresh for x; the separate identity keeps that structural fact kernel-visible.

Equations

• NFChoice.DirectNominalPrf.Nominal.ax6OfShift x p hShift = NFChoice.DirectNominalPrf.Nominal.freshIntroOfShift (NFChoice.SemanticCore.Wff.all x p).neg x hShift

def NFChoice.DirectNominalPrf.Nominal.ax7OfSwap (x y : SemanticCore.Var) (p : SemanticCore.Wff) (hSwap : ∀ (rho : SemanticCore.Var → ℕ), lowerWff (bindRho (bindRho rho y) x) p = GenericLogicalHandlers.swap01 (lowerWff (bindRho (bindRho rho x) y) p)) : NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.all y p)).imp (SemanticCore.Wff.all y (SemanticCore.Wff.all x p)))

Metamath ax-7. hSwap is the exact named-binder/de-Bruijn swap identity for the instantiated matrix.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.ax8 (x y z : SemanticCore.Var) : NPrf ((SemanticCore.Wff.objEq x y).imp ((SemanticCore.Wff.objEq x z).imp (SemanticCore.Wff.objEq y z)))

Metamath ax-8 (equality transitivity in its bundled orientation).

Equations

• NFChoice.DirectNominalPrf.Nominal.ax8 x y z rho = NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax8 NFChoice.Foundation.ExactLiteralTrial.LiteralHailperinNF.fst &(rho x) &(rho y) &(rho z)

def NFChoice.DirectNominalPrf.Nominal.ax9OfNe (x y : SemanticCore.Var) (hxy : y ≠ x) : NPrf (SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y).neg).neg

ax-9 when the two source variable names are distinct.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.ax13 (x y z : SemanticCore.Var) : NPrf ((SemanticCore.Wff.objEq x y).imp ((SemanticCore.Wff.objMem x z).imp (SemanticCore.Wff.objMem y z)))

Metamath ax-13 (left equality for membership).

Equations

• NFChoice.DirectNominalPrf.Nominal.ax13 x y z rho = NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax13 NFChoice.Foundation.ExactLiteralTrial.LiteralHailperinNF.fst &(rho x) &(rho y) &(rho z)

def NFChoice.DirectNominalPrf.Nominal.ax14 (x y z : SemanticCore.Var) : NPrf ((SemanticCore.Wff.objEq x y).imp ((SemanticCore.Wff.objMem z x).imp (SemanticCore.Wff.objMem z y)))

Metamath ax-14 (right equality for membership).

Equations

• NFChoice.DirectNominalPrf.Nominal.ax14 x y z rho = NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax14 NFChoice.Foundation.ExactLiteralTrial.LiteralHailperinNF.fst &(rho x) &(rho y) &(rho z)

def NFChoice.DirectNominalPrf.Nominal.ax12OfShift (x y z : SemanticCore.Var) (hShift : ∀ (rho : SemanticCore.Var → ℕ), lowerWff (bindRho rho x) (SemanticCore.Wff.objEq y z) = Fol.liftFormula1 (lowerWff rho (SemanticCore.Wff.objEq y z))) : NPrf ((SemanticCore.Wff.objEq x y).neg.imp ((SemanticCore.Wff.objEq y z).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z))))

Metamath ax-12, with the freshness of y = z for x represented by its lowering/shift identity. This is the nondegenerate branch used after $d checking; coincident bundled-variable branches can be emitted separately.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.ax11OfTemplate (x y : SemanticCore.Var) (p : SemanticCore.Wff) (hxy : y ≠ x) (template : (SemanticCore.Var → ℕ) → Fol.formula Foundation.LNF) (hSource : ∀ (rho : SemanticCore.Var → ℕ), GenericLogicalHandlers.ax11Inst (lowerWff (bindRho rho y) p) &(rho y) = template rho [Fol.liftTerm1 &(rho x) // 0]f) (hTarget : ∀ (rho : SemanticCore.Var → ℕ), template rho [&0 // 0]f = lowerWff (bindRho rho x) p) : NPrf ((SemanticCore.Wff.objEq x y).imp ((SemanticCore.Wff.all y p).imp (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp p))))

Metamath ax-11. The two equalities are the exact source-instantiation and target-binder identities for the chosen one-hole de-Bruijn template.

Equations

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