Documentation

Arithmetization.Definability.Boldface

def LO.FirstOrder.Defined {V : Type u_1} {L : Language} {k : } (R : (Fin kV)Prop) [Structure L V] (φ : Semisentence L k) :
Equations
Instances For
    def LO.FirstOrder.DefinedWithParam {V : Type u_1} {L : Language} {k : } (R : (Fin kV)Prop) [Structure L V] (φ : Semiformula L V k) :
    Equations
    Instances For
      theorem LO.FirstOrder.Defined.iff {L : Language} {V : Type u_2} [Structure L V] {k : } {R : (Fin kV)Prop} {φ : Semisentence L k} (h : Defined R φ) (v : Fin kV) :
      V ⊧/v φ R v
      theorem LO.FirstOrder.DefinedWithParam.iff {L : Language} {V : Type u_2} [Structure L V] {k : } {R : (Fin kV)Prop} {φ : Semiformula L V k} (h : DefinedWithParam R φ) (v : Fin kV) :
      (Semiformula.Evalm V v id) φ R v
      class LO.FirstOrder.Arith.HierarchySymbol.Lightface {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) {k : } (P : (Fin kV)Prop) :
      • definable : ∃ (φ : .Semisentence k), Defined P φ
      Instances
        class LO.FirstOrder.Arith.HierarchySymbol.Boldface {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) {k : } (P : (Fin kV)Prop) :
        Instances
          @[reducible, inline]
          abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedPred {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (P : VProp) (φ : .Semisentence 1) :
          Equations
          Instances For
            @[reducible, inline]
            abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedRel {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (R : VVProp) (φ : .Semisentence 2) :
            Equations
            Instances For
              @[reducible, inline]
              abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedRel₃ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (R : VVVProp) (φ : .Semisentence 3) :
              Equations
              Instances For
                @[reducible, inline]
                abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedRel₄ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (R : VVVVProp) (φ : .Semisentence 4) :
                Equations
                Instances For
                  @[reducible, inline]
                  abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } (f : (Fin kV)V) (φ : .Semisentence (k + 1)) :
                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₀ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (c : V) (φ : .Semisentence 1) :
                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₁ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : VV) (φ : .Semisentence 2) :
                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₂ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : VVV) (φ : .Semisentence 3) :
                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₃ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : VVVV) (φ : .Semisentence 4) :
                          Equations
                          Instances For
                            @[reducible, inline]
                            abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₄ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : VVVVV) (φ : .Semisentence 5) :
                            Equations
                            Instances For
                              @[reducible, inline]
                              abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₅ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : VVVVVV) (φ : .Semisentence 6) :
                              Equations
                              Instances For
                                @[reducible, inline]
                                Equations
                                Instances For
                                  @[reducible, inline]
                                  Equations
                                  • (-Relation P) = .Boldface fun (v : Fin 2V) => P (v 0) (v 1)
                                  Instances For
                                    @[reducible, inline]
                                    abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₃ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (P : VVVProp) :
                                    Equations
                                    Instances For
                                      @[reducible, inline]
                                      abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₄ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (P : VVVVProp) :
                                      Equations
                                      • (-Relation₄ P) = .Boldface fun (v : Fin 4V) => P (v 0) (v 1) (v 2) (v 3)
                                      Instances For
                                        @[reducible, inline]
                                        abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₅ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (P : VVVVVProp) :
                                        Equations
                                        • (-Relation₅ P) = .Boldface fun (v : Fin 5V) => P (v 0) (v 1) (v 2) (v 3) (v 4)
                                        Instances For
                                          @[reducible, inline]
                                          abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₆ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (P : VVVVVVProp) :
                                          Equations
                                          • .BoldfaceRel₆ P = .Boldface fun (v : Fin 6V) => P (v 0) (v 1) (v 2) (v 3) (v 4) (v 5)
                                          Instances For
                                            @[reducible, inline]
                                            abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) {k : } (f : (Fin kV)V) :
                                            Equations
                                            • .BoldfaceFunction f = .Boldface fun (v : Fin (k + 1)V) => v 0 = f fun (x : Fin k) => v x.succ
                                            Instances For
                                              @[reducible, inline]
                                              Equations
                                              • .BoldfaceFunction₀ c = .BoldfaceFunction fun (x : Fin 0V) => c
                                              Instances For
                                                @[reducible, inline]
                                                Equations
                                                Instances For
                                                  @[reducible, inline]
                                                  Equations
                                                  • (-Function₂ f) = .BoldfaceFunction fun (v : Fin 2V) => f (v 0) (v 1)
                                                  Instances For
                                                    @[reducible, inline]
                                                    abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₃ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : VVVV) :
                                                    Equations
                                                    • (-Function₃ f) = .BoldfaceFunction fun (v : Fin 3V) => f (v 0) (v 1) (v 2)
                                                    Instances For
                                                      @[reducible, inline]
                                                      abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₄ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : VVVVV) :
                                                      Equations
                                                      • (-Function₄ f) = .BoldfaceFunction fun (v : Fin 4V) => f (v 0) (v 1) (v 2) (v 3)
                                                      Instances For
                                                        @[reducible, inline]
                                                        abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₅ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : VVVVVV) :
                                                        Equations
                                                        • .BoldfaceFunction₅ f = .BoldfaceFunction fun (v : Fin 5V) => f (v 0) (v 1) (v 2) (v 3) (v 4)
                                                        Instances For
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.df {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {R : (Fin kV)Prop} {φ : .Semisentence k} (h : Defined R φ) :
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.proper {V : Type u_2} [ORingStruc V] {k : } {R : (Fin kV)Prop} {m : } {φ : { Γ := 𝚫, rank := m }.Semisentence k} (h : Defined R φ) :
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.of_zero {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {R : (Fin kV)Prop} {φ : 𝚺₀.Semisentence k} (h : Defined R φ) :
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.emb {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {R : (Fin kV)Prop} {φ : .Semisentence k} (h : Defined R φ) :
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.of_iff {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P Q : (Fin kV)Prop} (h : ∀ (x : Fin kV), P x Q x) {φ : .Semisentence k} (H : Defined Q φ) :
                                                                                                Defined P φ
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.to_definable {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : (Fin kV)Prop} (φ : .Semisentence k) (hP : Defined P φ) :
                                                                                                .Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.to_definable₀ {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : (Fin kV)Prop} {φ : 𝚺₀.Semisentence k} (hP : Defined P φ) :
                                                                                                .Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.to_definable_oRing {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : (Fin kV)Prop} (φ : .Semisentence k) (hP : Defined P φ) :
                                                                                                .Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.to_definable_oRing₀ {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : (Fin kV)Prop} (φ : 𝚺₀.Semisentence k) (hP : Defined P φ) :
                                                                                                .Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction.of_eq {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {f g : (Fin kV)V} (h : ∀ (x : Fin kV), f x = g x) {φ : .Semisentence (k + 1)} (H : DefinedFunction f φ) :
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction.graph_delta {V : Type u_2} [ORingStruc V] {k m : } {f : (Fin kV)V} {φ : { Γ := 𝚺, rank := m }.Semisentence (k + 1)} (h : DefinedFunction f φ) :
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.proper {V : Type u_2} [ORingStruc V] {k : } {R : (Fin kV)Prop} {m : } {φ : HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }} (h : DefinedWithParam R φ) :
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.of_zero {V : Type u_2} [ORingStruc V] {k : } {R : (Fin kV)Prop} {Γ' : SigmaPiDelta} {φ : HierarchySymbol.Semiformula V k { Γ := Γ', rank := 0 }} (h : DefinedWithParam R φ) {Γ : HierarchySymbol} :
                                                                                                DefinedWithParam R (φ.ofZero Γ)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.of_deltaOne {V : Type u_2} [ORingStruc V] {k : } {R : (Fin kV)Prop} {Γ : SigmaPiDelta} {m : } {φ : HierarchySymbol.Semiformula V k 𝚫₁} (h : DefinedWithParam R φ) :
                                                                                                DefinedWithParam R (φ.ofDeltaOne Γ m)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.of_iff {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P Q : (Fin kV)Prop} (h : ∀ (x : Fin kV), P x Q x) {φ : HierarchySymbol.Semiformula V k } (H : DefinedWithParam Q φ) :
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.to_definable {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : (Fin kV)Prop} {φ : HierarchySymbol.Semiformula V k } (h : DefinedWithParam P φ) :
                                                                                                .Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.to_definable₀ {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : (Fin kV)Prop} {Γ' : SigmaPiDelta} {φ : HierarchySymbol.Semiformula V k { Γ := Γ', rank := 0 }} (h : DefinedWithParam P φ) :
                                                                                                .Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.to_definable_deltaOne {V : Type u_2} [ORingStruc V] {k : } {P : (Fin kV)Prop} {φ : HierarchySymbol.Semiformula V k 𝚫₁} {Γ : SigmaPiDelta} {m : } (h : DefinedWithParam P φ) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.retraction {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : (Fin kV)Prop} {l : } {φ : HierarchySymbol.Semiformula V k } (hp : DefinedWithParam P φ) (f : Fin kFin l) :
                                                                                                DefinedWithParam (fun (v : Fin lV) => P fun (i : Fin k) => v (f i)) (Semiformula.rew (Rew.substs fun (x : Fin k) => Semiterm.bvar (f x)) φ)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.and {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P Q : (Fin kV)Prop} {φ ψ : HierarchySymbol.Semiformula V k } (hp : DefinedWithParam P φ) (hq : DefinedWithParam Q ψ) :
                                                                                                DefinedWithParam (fun (x : Fin kV) => P x Q x) (φ ψ)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.or {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P Q : (Fin kV)Prop} {φ ψ : HierarchySymbol.Semiformula V k } (hp : DefinedWithParam P φ) (hq : DefinedWithParam Q ψ) :
                                                                                                DefinedWithParam (fun (x : Fin kV) => P x Q x) (φ ψ)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.negSigma {V : Type u_2} [ORingStruc V] {k : } {P : (Fin kV)Prop} {m : } {φ : HierarchySymbol.Semiformula V k { Γ := 𝚺, rank := m }} (hp : DefinedWithParam P φ) :
                                                                                                DefinedWithParam (fun (x : Fin kV) => ¬P x) φ.negSigma
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.negPi {V : Type u_2} [ORingStruc V] {k : } {P : (Fin kV)Prop} {m : } {φ : HierarchySymbol.Semiformula V k { Γ := 𝚷, rank := m }} (hp : DefinedWithParam P φ) :
                                                                                                DefinedWithParam (fun (x : Fin kV) => ¬P x) φ.negPi
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.not {V : Type u_2} [ORingStruc V] {k : } {P : (Fin kV)Prop} {m : } {φ : HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }} (hp : DefinedWithParam P φ) :
                                                                                                DefinedWithParam (fun (x : Fin kV) => ¬P x) (φ)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.imp {V : Type u_2} [ORingStruc V] {k : } {P Q : (Fin kV)Prop} {m : } {φ ψ : HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }} (hp : DefinedWithParam P φ) (hq : DefinedWithParam Q ψ) :
                                                                                                DefinedWithParam (fun (x : Fin kV) => P xQ x) (φ ψ)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.iff {V : Type u_2} [ORingStruc V] {k : } {P Q : (Fin kV)Prop} {m : } {φ ψ : HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }} (hp : DefinedWithParam P φ) (hq : DefinedWithParam Q ψ) :
                                                                                                DefinedWithParam (fun (x : Fin kV) => P x Q x) (φ ψ)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.ball {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : (Fin (k + 1)V)Prop} {φ : HierarchySymbol.Semiformula V (k + 1) } (hp : DefinedWithParam P φ) (t : Semiterm ℒₒᵣ V k) :
                                                                                                DefinedWithParam (fun (v : Fin kV) => x < Semiterm.valm V v id t, P (x :> v)) (Semiformula.ball t φ)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.bex {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : (Fin (k + 1)V)Prop} {φ : HierarchySymbol.Semiformula V (k + 1) } (hp : DefinedWithParam P φ) (t : Semiterm ℒₒᵣ V k) :
                                                                                                DefinedWithParam (fun (v : Fin kV) => x < Semiterm.valm V v id t, P (x :> v)) (Semiformula.bex t φ)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.ex {V : Type u_2} [ORingStruc V] {k m : } {P : (Fin (k + 1)V)Prop} {φ : HierarchySymbol.Semiformula V (k + 1) { Γ := 𝚺, rank := m + 1 }} (hp : DefinedWithParam P φ) :
                                                                                                DefinedWithParam (fun (v : Fin kV) => ∃ (x : V), P (x :> v)) φ.ex
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.all {V : Type u_2} [ORingStruc V] {k m : } {P : (Fin (k + 1)V)Prop} {φ : HierarchySymbol.Semiformula V (k + 1) { Γ := 𝚷, rank := m + 1 }} (hp : DefinedWithParam P φ) :
                                                                                                DefinedWithParam (fun (v : Fin kV) => ∀ (x : V), P (x :> v)) φ.all
                                                                                                @[simp]
                                                                                                @[simp]
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.mkPolarity {V : Type u_2} [ORingStruc V] {k m : } {P : (Fin kV)Prop} {Γ : Polarity} (φ : Semiformula ℒₒᵣ V k) (hp : Hierarchy Γ m φ) (hP : ∀ (v : Fin kV), P v (Semiformula.Evalm V v id) φ) :
                                                                                                { Γ := Γ.coe, rank := m }.Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_iff {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P Q : (Fin kV)Prop} (H : .Boldface Q) (h : ∀ (x : Fin kV), P x Q x) :
                                                                                                .Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_oRing {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : (Fin kV)Prop} (h : .Boldface P) :
                                                                                                .Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_delta {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {k : } {P : (Fin kV)Prop} {m : } (h : { Γ := 𝚫, rank := m }.Boldface P) :
                                                                                                { Γ := Γ, rank := m }.Boldface P
                                                                                                instance LO.FirstOrder.Arith.HierarchySymbol.Boldface.instMkOfDeltaSigmaPiDelta {V : Type u_2} [ORingStruc V] {k : } {P : (Fin kV)Prop} {m : } [{ Γ := 𝚫, rank := m }.Boldface P] (Γ : SigmaPiDelta) :
                                                                                                { Γ := Γ, rank := m }.Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_sigma_of_pi {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {k : } {P : (Fin kV)Prop} {m : } (hσ : { Γ := 𝚺, rank := m }.Boldface P) (hπ : { Γ := 𝚷, rank := m }.Boldface P) :
                                                                                                { Γ := Γ, rank := m }.Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_zero {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : (Fin kV)Prop} {Γ' : SigmaPiDelta} (h : { Γ := Γ', rank := 0 }.Boldface P) :
                                                                                                .Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_deltaOne {V : Type u_2} [ORingStruc V] {k : } {P : (Fin kV)Prop} (h : 𝚫₁.Boldface P) {Γ : SigmaPiDelta} {m : } :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface P
                                                                                                instance LO.FirstOrder.Arith.HierarchySymbol.Boldface.instOfSigmaZero {V : Type u_2} [ORingStruc V] {k : } {P : (Fin kV)Prop} [𝚺₀.Boldface P] (ℌ : HierarchySymbol) :
                                                                                                .Boldface P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.retraction {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : (Fin kV)Prop} (h : .Boldface P) {n : } (f : Fin kFin n) :
                                                                                                .Boldface fun (v : Fin nV) => P fun (i : Fin k) => v (f i)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.retractiont (n : ) {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : (Fin kV)Prop} (h : .Boldface P) (f : Fin kSemiterm ℒₒᵣ V n) :
                                                                                                .Boldface fun (v : Fin nV) => P fun (i : Fin k) => Semiterm.valm V v id (f i)
                                                                                                @[simp]
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.const {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P : Prop} :
                                                                                                .Boldface fun (x : Fin kV) => P
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.and {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P Q : (Fin kV)Prop} (h₁ : .Boldface P) (h₂ : .Boldface Q) :
                                                                                                .Boldface fun (v : Fin kV) => P v Q v
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.conj {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k l : } {P : Fin l(Fin kV)Prop} (h : ∀ (i : Fin l), .Boldface fun (w : Fin kV) => P i w) :
                                                                                                .Boldface fun (v : Fin kV) => ∀ (i : Fin l), P i v
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.or {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {P Q : (Fin kV)Prop} (h₁ : .Boldface P) (h₂ : .Boldface Q) :
                                                                                                .Boldface fun (v : Fin kV) => P v Q v
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.not {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {k : } {P : (Fin kV)Prop} {m : } (h : { Γ := Γ.alt, rank := m }.Boldface P) :
                                                                                                { Γ := Γ, rank := m }.Boldface fun (v : Fin kV) => ¬P v
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.imp {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {k : } {P Q : (Fin kV)Prop} {m : } (h₁ : { Γ := Γ.alt, rank := m }.Boldface P) (h₂ : { Γ := Γ, rank := m }.Boldface Q) :
                                                                                                { Γ := Γ, rank := m }.Boldface fun (v : Fin kV) => P vQ v
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.iff {V : Type u_2} [ORingStruc V] {k : } {P Q : (Fin kV)Prop} {m : } (h₁ : { Γ := 𝚫, rank := m }.Boldface P) (h₂ : { Γ := 𝚫, rank := m }.Boldface Q) {Γ : SigmaPiDelta} :
                                                                                                { Γ := Γ, rank := m }.Boldface fun (v : Fin kV) => P v Q v
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.all {V : Type u_2} [ORingStruc V] {k s : } {P : (Fin kV)VProp} (h : { Γ := 𝚷, rank := s + 1 }.Boldface fun (w : Fin (k + 1)V) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                { Γ := 𝚷, rank := s + 1 }.Boldface fun (v : Fin kV) => ∀ (x : V), P v x
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ex {V : Type u_2} [ORingStruc V] {k s : } {P : (Fin kV)VProp} (h : { Γ := 𝚺, rank := s + 1 }.Boldface fun (w : Fin (k + 1)V) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                { Γ := 𝚺, rank := s + 1 }.Boldface fun (v : Fin kV) => ∃ (x : V), P v x
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.equal' {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } (i j : Fin k) :
                                                                                                .Boldface fun (v : Fin kV) => v i = v j
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_sigma {V : Type u_2} [ORingStruc V] {k m : } {f : (Fin kV)V} (h : { Γ := 𝚺, rank := m }.BoldfaceFunction f) {Γ : SigmaPiDelta} :
                                                                                                { Γ := Γ, rank := m }.BoldfaceFunction f
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.exVec {V : Type u_2} [ORingStruc V] {m k l : } {P : (Fin kV)(Fin lV)Prop} (h : { Γ := 𝚺, rank := m + 1 }.Boldface fun (w : Fin (k + l)V) => P (fun (i : Fin k) => w (Fin.castAdd l i)) fun (j : Fin l) => w (Fin.natAdd k j)) :
                                                                                                { Γ := 𝚺, rank := m + 1 }.Boldface fun (v : Fin kV) => ∃ (ys : Fin lV), P v ys
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.allVec {V : Type u_2} [ORingStruc V] {m k l : } {P : (Fin kV)(Fin lV)Prop} (h : { Γ := 𝚷, rank := m + 1 }.Boldface fun (w : Fin (k + l)V) => P (fun (i : Fin k) => w (Fin.castAdd l i)) fun (j : Fin l) => w (Fin.natAdd k j)) :
                                                                                                { Γ := 𝚷, rank := m + 1 }.Boldface fun (v : Fin kV) => ∀ (ys : Fin lV), P v ys
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.substitution {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {k : } {P : (Fin kV)Prop} {l m : } {f : Fin k(Fin lV)V} (hP : { Γ := Γ, rank := m + 1 }.Boldface P) (hf : ∀ (i : Fin k), { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction (f i)) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (z : Fin lV) => P fun (i : Fin k) => f i z
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfacePred.comp {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m : } {P : VProp} {k : } {f : (Fin kV)V} (hP : { Γ := Γ, rank := m + 1 }-Predicate P) (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel.comp {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m : } {P : VVProp} {k : } {f g : (Fin kV)V} (hP : { Γ := Γ, rank := m + 1 }-Relation P) (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (hg : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f v) (g v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₃.comp {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {P : VVVProp} {f₁ f₂ f₃ : (Fin kV)V} (hP : { Γ := Γ, rank := m + 1 }-Relation₃ P) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f₁ v) (f₂ v) (f₃ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₄.comp {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {P : VVVVProp} {f₁ f₂ f₃ f₄ : (Fin kV)V} (hP : { Γ := Γ, rank := m + 1 }-Relation₄ P) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₅.comp {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {P : VVVVVProp} {f₁ f₂ f₃ f₄ f₅ : (Fin kV)V} (hP : { Γ := Γ, rank := m + 1 }-Relation₅ P) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄) (hf₅ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₅) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₁ {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {P : VProp} {f : (Fin kV)V} [{ Γ := Γ, rank := m + 1 }-Predicate P] (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₂ {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {P : VVProp} {f g : (Fin kV)V} [{ Γ := Γ, rank := m + 1 }-Relation P] (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (hg : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f v) (g v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₃ {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {P : VVVProp} {f₁ f₂ f₃ : (Fin kV)V} [{ Γ := Γ, rank := m + 1 }-Relation₃ P] (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f₁ v) (f₂ v) (f₃ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₄ {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {P : VVVVProp} {f₁ f₂ f₃ f₄ : (Fin kV)V} [{ Γ := Γ, rank := m + 1 }-Relation₄ P] (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₅ {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {P : VVVVVProp} {f₁ f₂ f₃ f₄ f₅ : (Fin kV)V} [{ Γ := Γ, rank := m + 1 }-Relation₅ P] (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄) (hf₅ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₅) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfacePred.of_iff {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {P Q : VProp} (H : -Predicate Q) (h : ∀ (x : V), P x Q x) :
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.graph_delta {V : Type u_2} [ORingStruc V] {m k : } {f : (Fin kV)V} (h : { Γ := 𝚺, rank := m }.BoldfaceFunction f) :
                                                                                                { Γ := 𝚫, rank := m }.BoldfaceFunction f
                                                                                                instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.instMkDeltaSigmaPiDeltaOfSigma {V : Type u_2} [ORingStruc V] {m k : } {f : (Fin kV)V} [h : { Γ := 𝚺, rank := m }.BoldfaceFunction f] :
                                                                                                { Γ := 𝚫, rank := m }.BoldfaceFunction f
                                                                                                instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.instOfSigmaZero {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } {f : (Fin kV)V} [𝚺₀.BoldfaceFunction f] :
                                                                                                .BoldfaceFunction f
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.of_sigmaOne {V : Type u_2} [ORingStruc V] {k : } {f : (Fin kV)V} (h : 𝚺₁.BoldfaceFunction f) {Γ : SigmaPiDelta} {m : } :
                                                                                                { Γ := Γ, rank := m + 1 }.BoldfaceFunction f
                                                                                                @[simp]
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.var {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } (i : Fin k) :
                                                                                                .BoldfaceFunction fun (v : Fin kV) => v i
                                                                                                @[simp]
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.const {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : } (c : V) :
                                                                                                .BoldfaceFunction fun (x : Fin kV) => c
                                                                                                @[simp]
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.term_retraction (n : ) {V : Type u_2} [ORingStruc V] {k : } {ℌ : HierarchySymbol} (t : Semiterm ℒₒᵣ V n) (e : Fin nFin k) :
                                                                                                .BoldfaceFunction fun (v : Fin kV) => Semiterm.valm V (fun (x : Fin n) => v (e x)) id t
                                                                                                @[simp]
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.term {V : Type u_2} [ORingStruc V] {k : } {ℌ : HierarchySymbol} (t : Semiterm ℒₒᵣ V k) :
                                                                                                .BoldfaceFunction fun (v : Fin kV) => Semiterm.valm V v id t
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.of_eq {V : Type u_2} [ORingStruc V] {k : } {ℌ : HierarchySymbol} {f : (Fin kV)V} (g : (Fin kV)V) (h : ∀ (v : Fin kV), f v = g v) (H : .BoldfaceFunction f) :
                                                                                                .BoldfaceFunction g
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.retraction {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {n k : } {f : (Fin kV)V} (hf : .BoldfaceFunction f) (e : Fin kFin n) :
                                                                                                .BoldfaceFunction fun (v : Fin nV) => f fun (i : Fin k) => v (e i)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.retractiont {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {n k : } {f : (Fin kV)V} (hf : .BoldfaceFunction f) (t : Fin kSemiterm ℒₒᵣ V n) :
                                                                                                .BoldfaceFunction fun (v : Fin nV) => f fun (i : Fin k) => Semiterm.valm V v id (t i)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.rel {V : Type u_2} [ORingStruc V] {k : } {ℌ : HierarchySymbol} {f : (Fin kV)V} (h : .BoldfaceFunction f) :
                                                                                                .Boldface fun (v : Fin (k + 1)V) => v 0 = f fun (x : Fin k) => v x.succ
                                                                                                @[simp]
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.nth {V : Type u_2} [ORingStruc V] {k : } (ℌ : HierarchySymbol) (i : Fin k) :
                                                                                                .BoldfaceFunction fun (w : Fin kV) => w i
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.substitution {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {k l m : } {F : (Fin kV)V} {f : Fin k(Fin lV)V} (hF : { Γ := Γ, rank := m + 1 }.BoldfaceFunction F) (hf : ∀ (i : Fin k), { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction (f i)) :
                                                                                                { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (z : Fin lV) => F fun (i : Fin k) => f i z
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₁.comp {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {F : VV} {f : (Fin kV)V} (hF : { Γ := Γ, rank := m + 1 }-Function₁ F) (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) :
                                                                                                { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => F (f v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.comp {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {F : VVV} {f₁ f₂ : (Fin kV)V} (hF : { Γ := Γ, rank := m + 1 }-Function₂ F) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) :
                                                                                                { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => F (f₁ v) (f₂ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₃.comp {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {F : VVVV} {f₁ f₂ f₃ : (Fin kV)V} (hF : { Γ := Γ, rank := m + 1 }-Function₃ F) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) :
                                                                                                { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => F (f₁ v) (f₂ v) (f₃ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₄.comp {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {F : VVVVV} {f₁ f₂ f₃ f₄ : (Fin kV)V} (hF : { Γ := Γ, rank := m + 1 }-Function₄ F) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄) :
                                                                                                { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => F (f₁ v) (f₂ v) (f₃ v) (f₄ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₅.comp {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {F : VVVVVV} {f₁ f₂ f₃ f₄ f₅ : (Fin kV)V} (hF : { Γ := Γ, rank := m + 1 }.BoldfaceFunction₅ F) (hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁) (hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂) (hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃) (hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄) (hf₅ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₅) :
                                                                                                { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => F (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₁ {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {f : VV} [{ Γ := Γ, rank := m + 1 }-Function₁ f] {g : (Fin kV)V} (hg : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g) :
                                                                                                { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => f (g v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₂ {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {f : VVV} [{ Γ := Γ, rank := m + 1 }-Function₂ f] {g₁ g₂ : (Fin kV)V} (hg₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₁) (hg₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₂) :
                                                                                                { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => f (g₁ v) (g₂ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₃ {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {f : VVVV} [{ Γ := Γ, rank := m + 1 }-Function₃ f] {g₁ g₂ g₃ : (Fin kV)V} (hg₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₁) (hg₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₂) (hg₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₃) :
                                                                                                { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => f (g₁ v) (g₂ v) (g₃ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₄ {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {f : VVVVV} [{ Γ := Γ, rank := m + 1 }-Function₄ f] {g₁ g₂ g₃ g₄ : (Fin kV)V} (hg₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₁) (hg₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₂) (hg₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₃) (hg₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₄) :
                                                                                                { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => f (g₁ v) (g₂ v) (g₃ v) (g₄ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₅ {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {m k : } {f : VVVVVV} [{ Γ := Γ, rank := m + 1 }.BoldfaceFunction₅ f] {g₁ g₂ g₃ g₄ g₅ : (Fin kV)V} (hg₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₁) (hg₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₂) (hg₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₃) (hg₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₄) (hg₅ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₅) :
                                                                                                { Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin kV) => f (g₁ v) (g₂ v) (g₃ v) (g₄ v) (g₅ v)
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_lt {V : Type u_2} [ORingStruc V] {k m : } {Γ : SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin (k + 1)V) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => x < f v, P v x
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_lt {V : Type u_2} [ORingStruc V] {k m : } {Γ : SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin (k + 1)V) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => x < f v, P v x
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_le {V : Type u_2} [ORingStruc V] {k m : } [V ⊧ₘ* 𝐏𝐀⁻] {Γ : SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin (k + 1)V) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => xf v, P v x
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_le {V : Type u_2} [ORingStruc V] {k m : } [V ⊧ₘ* 𝐏𝐀⁻] {Γ : SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin (k + 1)V) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => xf v, P v x
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_lt' {V : Type u_2} [ORingStruc V] {k m : } {Γ : SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin (k + 1)V) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => ∀ {x : V}, x < f vP v x
                                                                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_le' {V : Type u_2} [ORingStruc V] {k m : } [V ⊧ₘ* 𝐏𝐀⁻] {Γ : SigmaPiDelta} {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin (k + 1)V) => P (fun (x : Fin k) => w x.succ) (w 0)) :
                                                                                                { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => ∀ {x : V}, x f vP v x