Documentation

Arithmetization.ISigmaOne.Metamath.Language

Instances For
    structure LO.Arith.Language (V : Type u_1) :
    Type u_1
    • Func : VVProp
    • Rel : VVProp
    Instances For
      Instances
        theorem LO.Arith.Language.Defined.func {V : Type u_1} [LO.ORingStruc V] {L : LO.Arith.Language V} {pL : outParam LO.FirstOrder.Arith.LDef} [self : L.Defined pL] :
        𝚺₀-Relation L.Func via pL.func
        theorem LO.Arith.Language.Defined.rel {V : Type u_1} [LO.ORingStruc V] {L : LO.Arith.Language V} {pL : outParam LO.FirstOrder.Arith.LDef} [self : L.Defined pL] :
        𝚺₀-Relation L.Rel via pL.rel
        @[simp]
        theorem LO.Arith.Language.Defined.eval_func {V : Type u_1} [LO.ORingStruc V] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (v : Fin 2V) :
        @[simp]
        theorem LO.Arith.Language.Defined.eval_rel_iff {V : Type u_1} [LO.ORingStruc V] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (v : Fin 2V) :
        Equations
        • =
        Equations
        • =
        @[simp]
        Equations
        • =
        @[simp]
        Equations
        • =
        class LO.Arith.DefinableLanguage (L : LO.FirstOrder.Language) [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] extends LO.FirstOrder.Arith.LDef :
        Instances
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem LO.FirstOrder.Language.codeIn_func_def (L : LO.FirstOrder.Language) [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (V : Type u_1) [LO.ORingStruc V] :
            (L.codeIn V).Func = fun (x y : V) => V ⊧/![x, y] (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val L.lDef.func)
            instance LO.Arith.instDefinedCodeInLDef {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {V : Type u_1} [LO.ORingStruc V] :
            (L.codeIn V).Defined L.lDef
            Equations
            • LO.Arith.instDefinedCodeInLDef = { func := , rel := }
            Equations
            • LO.Arith.instGoedelQuoteFunc_arithmetization = { quote := fun (f : L.Func k) => (Encodable.encode f) }
            Equations
            • LO.Arith.instGoedelQuoteRel_arithmetization = { quote := fun (R : L.Rel k) => (Encodable.encode R) }
            theorem LO.Arith.quote_func_def {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } (f : L.Func k) :
            theorem LO.Arith.quote_rel_def {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Rel k)] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } (R : L.Rel k) :
            theorem LO.Arith.codeIn_func_quote_iff {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } {x : } :
            (L.codeIn V).Func k x ∃ (f : L.Func k), Encodable.encode f = x
            theorem LO.Arith.codeIn_rel_quote_iff {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } {x : } :
            (L.codeIn V).Rel k x ∃ (R : L.Rel k), Encodable.encode R = x
            @[simp]
            theorem LO.Arith.codeIn_func_quote {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } (f : L.Func k) :
            (L.codeIn V).Func k f
            @[simp]
            theorem LO.Arith.codeIn_rel_quote {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] [(k : ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } (r : L.Rel k) :
            (L.codeIn V).Rel k r
            @[simp]
            theorem LO.Arith.quote_func_inj {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } (f₁ : L.Func k) (f₂ : L.Func k) :
            f₁ = f₂ f₁ = f₂
            @[simp]
            theorem LO.Arith.quote_rel_inj {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Rel k)] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } (R₁ : L.Rel k) (R₂ : L.Rel k) :
            R₁ = R₂ R₁ = R₂
            @[simp]
            theorem LO.Arith.coe_quote_func_nat {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Func k)] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } (f : L.Func k) :
            @[simp]
            theorem LO.Arith.coe_quote_rel_nat {L : LO.FirstOrder.Language} [(k : ) → Encodable (L.Rel k)] {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : } (R : L.Rel k) :
            theorem LO.FirstOrder.Language.ORing.of_mem_range_encode_func {k : } {f : } :
            f Set.range Encodable.encode k = 0 f = 0 k = 0 f = 1 k = 2 f = 0 k = 2 f = 1

            TODO: move to Basic/Syntax/Language.lean

            theorem LO.FirstOrder.Language.ORing.of_mem_range_encode_rel {k : } {r : } :
            r Set.range Encodable.encode k = 2 r = 0 k = 2 r = 1

            TODO: move to Basic/Syntax/Language.lean

            Equations
            • One or more equations did not get rendered due to their size.
            @[reducible, inline]
            Equations
            Instances For
              @[reducible, inline]
              Equations
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  Instances For
                    Equations
                    Instances For
                      Equations
                      Instances For
                        Equations
                        Instances For