Documentation

LeanPool.NFWeakPartition.SemanticCore.Basic

NF weak partition development: SemanticCore.Basic.

This is a nominal semantic front end for replaying the nf.mm proof. Metamath set variables are natural-number names. A class denotes a unary predicate on the carrier of an arbitrary membership-only first-order structure.

The object/class distinction is retained at atomic formulas. In particular, object equality and membership have their ordinary first-order meanings. Generic class equality and membership always use the standard extensional and representative semantics, including when both arguments happen to be set-variable classes. Transport from those generic atoms to primitive object atoms is therefore explicit and requires extensionality, just as df-cleq and df-clel require at the NF boundary.

source
@[reducible, inline]
abbrev NFChoice.SemanticCore.Var :
Type

Proof-translation construction identified upstream as Var.

Equations
Instances For
    source
    inductive NFChoice.SemanticCore.Class :
    Type

    The primitive class fragment needed before expanding defined symbols.

    Instances For
      source
      def NFChoice.SemanticCore.instDecidableEqClass.decEq_2 (x✝ x✝¹ : Wff) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        def NFChoice.SemanticCore.instDecidableEqClass.decEq_1 (x✝ x✝¹ : Class) :
        Decidable (x✝ = x✝¹)
        Equations
        Instances For
          source
          def NFChoice.SemanticCore.instDecidableEqWff.decEq_2 (x✝ x✝¹ : Wff) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            @[instance_reducible]
            instance NFChoice.SemanticCore.instDecidableEqWff :
            DecidableEq Wff
            Equations
            source
            def NFChoice.SemanticCore.instDecidableEqWff.decEq_1 (x✝ x✝¹ : Class) :
            Decidable (x✝ = x✝¹)
            Equations
            Instances For
              source
              @[instance_reducible]
              instance NFChoice.SemanticCore.instDecidableEqClass :
              DecidableEq Class
              Equations
              source
              @[instance_reducible]
              instance NFChoice.SemanticCore.instReprWff :
              Repr Wff
              Equations
              source
              partial def NFChoice.SemanticCore.instReprClass.repr_2 :
              Wff → ℕ → Std.Format
              source
              partial def NFChoice.SemanticCore.instReprClass.repr_1 :
              Class → ℕ → Std.Format
              source
              @[instance_reducible]
              instance NFChoice.SemanticCore.instReprClass :
              Repr Class
              Equations
              source
              partial def NFChoice.SemanticCore.instReprWff.repr_1 :
              Class → ℕ → Std.Format
              source
              partial def NFChoice.SemanticCore.instReprWff.repr_2 :
              Wff → ℕ → Std.Format
              source
              inductive NFChoice.SemanticCore.Wff :
              Type

              The primitive nominal wff fragment used by the semantic replay.

              Instances For

                vars records every nominal variable name occurring in an expression, while fv removes names bound by all and cab. The compiler uses vars to validate Metamath $d substitutions and fv to discharge semantic freshness.

                source
                def NFChoice.SemanticCore.Class.vars :
                Class → Finset Var

                Proof-translation construction identified upstream as Class.vars.

                Equations
                Instances For
                  source
                  def NFChoice.SemanticCore.Wff.vars :
                  Wff → Finset Var

                  Proof-translation construction identified upstream as Wff.vars.

                  Equations
                  Instances For
                    source
                    def NFChoice.SemanticCore.Class.fv :
                    Class → Finset Var

                    Proof-translation construction identified upstream as Class.fv.

                    Equations
                    Instances For
                      source
                      def NFChoice.SemanticCore.Wff.fv :
                      Wff → Finset Var

                      Proof-translation construction identified upstream as Wff.fv.

                      Equations
                      Instances For
                        source
                        theorem NFChoice.SemanticCore.Class.mem_vars_of_mem_fv (A : Class) {x : Var} (hx : x ∈ A.fv) :
                        x ∈ A.vars
                        source
                        theorem NFChoice.SemanticCore.Wff.mem_vars_of_mem_fv (p : Wff) {x : Var} (hx : x ∈ p.fv) :
                        x ∈ p.vars
                        source
                        theorem NFChoice.SemanticCore.Class.fv_subset_vars (A : Class) :
                        A.fv ⊆ A.vars
                        source
                        theorem NFChoice.SemanticCore.Wff.fv_subset_vars (p : Wff) :
                        p.fv ⊆ p.vars
                        source
                        theorem NFChoice.SemanticCore.Wff.not_mem_fv_of_not_mem_vars (p : Wff) {x : Var} (hx : x ∉ p.vars) :
                        x ∉ p.fv
                        source
                        def NFChoice.SemanticCore.update {α : Sort u_1} (v : Var → α) (x : Var) (a : α) :
                        Var → α

                        Update a named set-variable valuation.

                        Equations
                        Instances For
                          source
                          @[simp]
                          theorem NFChoice.SemanticCore.update_same {α : Sort u_1} (v : Var → α) (x : Var) (a : α) :
                          update v x a x = a
                          source
                          @[simp]
                          theorem NFChoice.SemanticCore.update_noteq {α : Sort u_1} (v : Var → α) {x y : Var} (h : y ≠ x) (a : α) :
                          update v x a y = v y
                          source
                          @[simp]
                          theorem NFChoice.SemanticCore.update_overwrite {α : Sort u_1} (v : Var → α) (x : Var) (a b : α) :
                          update (update v x a) x b = update v x b
                          source
                          def NFChoice.SemanticCore.Mem (S : Fol.Structure Foundation.LNF) (a b : S.carrier) :
                          Prop

                          The sole relation of an LNF structure, in source argument order.

                          Equations
                          Instances For
                            source
                            theorem NFChoice.SemanticCore.realize_mem_argument_order (S : Fol.Structure Foundation.LNF) (a b : S.carrier) :
                            Fol.realizeBoundedFormula (DVec.cons a (DVec.cons b DVec.nil)) (Foundation.Formula.mem 0 1).toFlypitch DVec.nil ↔ Mem S a b

                            Kernel check of the relation argument order: bounded variables [a,b] in the front-end atom 0 e. 1 realize to the relation vector [a,b].

                            source
                            def NFChoice.SemanticCore.Class.Holds (S : Fol.Structure Foundation.LNF) (v : Var → S.carrier) :
                            Class → S.carrier → Prop

                            Membership in the class denoted by a class expression.

                            Equations
                            Instances For
                              source
                              def NFChoice.SemanticCore.Wff.Holds (S : Fol.Structure Foundation.LNF) (v : Var → S.carrier) :
                              Wff → Prop

                              Truth of a nominal wff under a named valuation.

                              Equations
                              Instances For
                                source
                                def NFChoice.SemanticCore.AgreesOn {α : Sort u_1} (s : Finset Var) (v v' : Var → α) :
                                Prop

                                Two named valuations agree on a finite support.

                                Equations
                                Instances For
                                  source
                                  theorem NFChoice.SemanticCore.Class.holds_congr_fv {S : Fol.Structure Foundation.LNF} (A : Class) (v v' : Var → S.carrier) (h : AgreesOn A.fv v v') (a : S.carrier) :
                                  Holds S v A a ↔ Holds S v' A a

                                  A class denotation depends only on the free variables of the class.

                                  source
                                  theorem NFChoice.SemanticCore.Wff.holds_congr_fv {S : Fol.Structure Foundation.LNF} (p : Wff) (v v' : Var → S.carrier) (h : AgreesOn p.fv v v') :
                                  Holds S v p ↔ Holds S v' p

                                  A wff's truth value depends only on its free variables.

                                  source
                                  theorem NFChoice.SemanticCore.Wff.holds_update_fresh {S : Fol.Structure Foundation.LNF} (p : Wff) (v : Var → S.carrier) {x : Var} (hx : x ∉ p.fv) (a : S.carrier) :
                                  Holds S (update v x a) p ↔ Holds S v p

                                  Updating a variable fresh for a wff cannot change its truth value.

                                  source
                                  def NFChoice.SemanticCore.Wff.Valid (S : Fol.Structure Foundation.LNF) (p : Wff) :
                                  Prop

                                  A nominal wff is valid in a fixed structure.

                                  Equations
                                  Instances For
                                    source
                                    def NFChoice.SemanticCore.Wff.neg (p : Wff) :
                                    Wff

                                    Negation in the primitive implication/falsity basis.

                                    Equations
                                    Instances For
                                      source
                                      def NFChoice.SemanticCore.Wff.conj (p q : Wff) :
                                      Wff

                                      Classical conjunction in the primitive implication/falsity basis.

                                      Equations
                                      Instances For
                                        source
                                        def NFChoice.SemanticCore.Wff.disj (p q : Wff) :
                                        Wff

                                        Classical disjunction in the primitive implication/falsity basis.

                                        Equations
                                        Instances For
                                          source
                                          def NFChoice.SemanticCore.Wff.biimp (p q : Wff) :
                                          Wff

                                          Biconditional in the primitive implication/falsity basis.

                                          Equations
                                          Instances For
                                            source
                                            def NFChoice.SemanticCore.Wff.ex (x : Var) (p : Wff) :
                                            Wff

                                            Existential quantification in the primitive implication/falsity basis.

                                            Equations
                                            Instances For
                                              source
                                              @[simp]
                                              theorem NFChoice.SemanticCore.Wff.holds_neg {S : Fol.Structure Foundation.LNF} {v : Var → S.carrier} {p : Wff} :
                                              Holds S v p.neg ↔ ¬Holds S v p
                                              source
                                              @[simp]
                                              theorem NFChoice.SemanticCore.Wff.holds_conj {S : Fol.Structure Foundation.LNF} {v : Var → S.carrier} {p q : Wff} :
                                              Holds S v (p.conj q) ↔ Holds S v p ∧ Holds S v q
                                              source
                                              @[simp]
                                              theorem NFChoice.SemanticCore.Wff.holds_disj {S : Fol.Structure Foundation.LNF} {v : Var → S.carrier} {p q : Wff} :
                                              Holds S v (p.disj q) ↔ Holds S v p ∨ Holds S v q
                                              source
                                              @[simp]
                                              theorem NFChoice.SemanticCore.Wff.holds_biimp {S : Fol.Structure Foundation.LNF} {v : Var → S.carrier} {p q : Wff} :
                                              Holds S v (p.biimp q) ↔ (Holds S v p ↔ Holds S v q)
                                              source
                                              @[simp]
                                              theorem NFChoice.SemanticCore.Wff.holds_ex {S : Fol.Structure Foundation.LNF} {v : Var → S.carrier} {x : Var} {p : Wff} :
                                              Holds S v (ex x p) ↔ ∃ (a : S.carrier), Holds S (update v x a) p
                                              source
                                              theorem NFChoice.SemanticCore.Wff.holds_mp {S : Fol.Structure Foundation.LNF} {v : Var → S.carrier} {p q : Wff} (hpq : Holds S v (p.imp q)) (hp : Holds S v p) :
                                              Holds S v q

                                              Semantic modus ponens for the replay checker.

                                              source
                                              theorem NFChoice.SemanticCore.Wff.valid_mp {S : Fol.Structure Foundation.LNF} {p q : Wff} (hp : Valid S p) (hpq : Valid S (p.imp q)) :
                                              Valid S q

                                              Global semantic modus ponens, matching source rule ax-mp.

                                              source
                                              theorem NFChoice.SemanticCore.Wff.holds_ax1 {S : Fol.Structure Foundation.LNF} (v : Var → S.carrier) (p q : Wff) :
                                              Holds S v (p.imp (q.imp p))

                                              The semantic form of propositional axiom ax-1.

                                              source
                                              theorem NFChoice.SemanticCore.Wff.valid_ax1 {S : Fol.Structure Foundation.LNF} (p q : Wff) :
                                              Valid S (p.imp (q.imp p))

                                              Global semantic form of source axiom ax-1.

                                              source
                                              theorem NFChoice.SemanticCore.Wff.valid_generalization {S : Fol.Structure Foundation.LNF} {p : Wff} (hp : Valid S p) (x : Var) :
                                              Valid S (all x p)

                                              Generalization preserves validity, exactly matching source rule ax-gen.

                                              source
                                              theorem NFChoice.SemanticCore.Wff.valid_ax17 {S : Fol.Structure Foundation.LNF} (p : Wff) (x : Var) (hx : x ∉ p.fv) :
                                              Valid S (p.imp (all x p))

                                              Semantic form of source axiom ax-17, using free-variable freshness.

                                              source
                                              theorem NFChoice.SemanticCore.Wff.valid_ax17_of_not_mem_vars {S : Fol.Structure Foundation.LNF} (p : Wff) (x : Var) (hx : x ∉ p.vars) :
                                              Valid S (p.imp (all x p))

                                              The source $d x ph condition is stronger than the freshness ax-17 needs.

                                              source
                                              def NFChoice.SemanticCore.Extensional (S : Fol.Structure Foundation.LNF) :
                                              Prop

                                              Extensionality of the sole membership relation of a structure.

                                              Equations
                                              Instances For
                                                source
                                                def NFChoice.SemanticCore.Represents (S : Fol.Structure Foundation.LNF) (v : Var → S.carrier) (A : Class) (a : S.carrier) :
                                                Prop

                                                A set a represents the class A under valuation v.

                                                Equations
                                                Instances For
                                                  source
                                                  def NFChoice.SemanticCore.ExtClassEq (S : Fol.Structure Foundation.LNF) (v : Var → S.carrier) (A B : Class) :
                                                  Prop

                                                  Uniform extensional equality of two class denotations.

                                                  Equations
                                                  Instances For
                                                    source
                                                    def NFChoice.SemanticCore.ExtClassMem (S : Fol.Structure Foundation.LNF) (v : Var → S.carrier) (A B : Class) :
                                                    Prop

                                                    Uniform representative semantics for membership between two classes.

                                                    Equations
                                                    Instances For
                                                      source
                                                      theorem NFChoice.SemanticCore.cv_eq_iff_extensional {S : Fol.Structure Foundation.LNF} (hExt : Extensional S) (v : Var → S.carrier) (x y : Var) :
                                                      v x = v y ↔ ExtClassEq S v (Class.cv x) (Class.cv y)

                                                      Under extensionality, actual equality of set variables is extensional equality.

                                                      source
                                                      theorem NFChoice.SemanticCore.cv_mem_iff_extensional {S : Fol.Structure Foundation.LNF} (hExt : Extensional S) (v : Var → S.carrier) (x y : Var) :
                                                      Mem S (v x) (v y) ↔ ExtClassMem S v (Class.cv x) (Class.cv y)

                                                      Under extensionality, actual membership is representative class membership.

                                                      source
                                                      theorem NFChoice.SemanticCore.classEq_iff_extensional {S : Fol.Structure Foundation.LNF} (v : Var → S.carrier) (A B : Class) :
                                                      Wff.Holds S v (Wff.classEq A B) ↔ ExtClassEq S v A B

                                                      Generic class equality is definitionally its uniform extensional reading.

                                                      source
                                                      theorem NFChoice.SemanticCore.classMem_iff_extensional {S : Fol.Structure Foundation.LNF} (v : Var → S.carrier) (A B : Class) :
                                                      Wff.Holds S v (Wff.classMem A B) ↔ ExtClassMem S v A B

                                                      Generic class membership definitionally has representative semantics.

                                                      source
                                                      theorem NFChoice.SemanticCore.objEq_iff_classEq {S : Fol.Structure Foundation.LNF} (hExt : Extensional S) (v : Var → S.carrier) (x y : Var) :
                                                      Wff.Holds S v (Wff.objEq x y) ↔ Wff.Holds S v (Wff.classEq (Class.cv x) (Class.cv y))

                                                      Explicit df-cleq transport from primitive equality to generic equality.

                                                      source
                                                      theorem NFChoice.SemanticCore.objMem_iff_classMem {S : Fol.Structure Foundation.LNF} (hExt : Extensional S) (v : Var → S.carrier) (x y : Var) :
                                                      Wff.Holds S v (Wff.objMem x y) ↔ Wff.Holds S v (Wff.classMem (Class.cv x) (Class.cv y))

                                                      Explicit df-clel transport from primitive membership to generic membership.

                                                      The following theorem pins the nominal extensionality assumption to the exact closed first-order sentence placed in HailperinNF by the foundation.

                                                      source
                                                      theorem NFChoice.SemanticCore.extensional_iff_foundation_axExt (S : Fol.Structure Foundation.LNF) :
                                                      Extensional S ↔ Fol.realizeSentence S (Foundation.axiomFormula Foundation.HailperinAxiomName.axExt)

                                                      Semantics of the three source definitions most sensitive to binding.

                                                      source
                                                      def NFChoice.SemanticCore.notFree (x : Var) (p : Wff) :
                                                      Wff

                                                      The source definiens of F/ x ph.

                                                      Equations
                                                      Instances For
                                                        source
                                                        theorem NFChoice.SemanticCore.df_nf_semantics {S : Fol.Structure Foundation.LNF} (v : Var → S.carrier) (x : Var) (p : Wff) :
                                                        Wff.Holds S v (notFree x p) ↔ ∀ (a : S.carrier), Wff.Holds S (update v x a) p → ∀ (b : S.carrier), Wff.Holds S (update v x b) p

                                                        Semantic unfolding of source definition df-nf.

                                                        source
                                                        def NFChoice.SemanticCore.SubstHolds (S : Fol.Structure Foundation.LNF) (v : Var → S.carrier) (y x : Var) (p : Wff) :
                                                        Prop

                                                        Semantic proper substitution of set variable y for free x.

                                                        Equations
                                                        Instances For
                                                          source
                                                          def NFChoice.SemanticCore.sbDefiniens (y x : Var) (p : Wff) :
                                                          Wff

                                                          The right-hand side of source definition df-sb.

                                                          Equations
                                                          Instances For
                                                            source
                                                            theorem NFChoice.SemanticCore.df_sb_semantics {S : Fol.Structure Foundation.LNF} (v : Var → S.carrier) (y x : Var) (p : Wff) :
                                                            SubstHolds S v y x p ↔ Wff.Holds S v (sbDefiniens y x p)

                                                            Semantic soundness of the unrestricted proper-substitution definition df-sb.

                                                            source
                                                            def NFChoice.SemanticCore.CvSubstHolds (S : Fol.Structure Foundation.LNF) (v : Var → S.carrier) (x y : Var) (p : Wff) :
                                                            Prop

                                                            Semantic right-hand side of [ x / y ] ph.

                                                            Equations
                                                            Instances For
                                                              source
                                                              theorem NFChoice.SemanticCore.df_clab_semantics {S : Fol.Structure Foundation.LNF} (hExt : Extensional S) (v : Var → S.carrier) (x y : Var) (p : Wff) :
                                                              Wff.Holds S v (Wff.classMem (Class.cv x) (Class.cab y p)) ↔ CvSubstHolds S v x y p

                                                              df-clab: membership of a set variable in an abstraction is proper substitution.