Arithmetization.Definability.Boldface

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.imp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {k : ℕ} {P : (Fin k → V) → Prop} {Q : (Fin k → V) → Prop} {m : ℕ} (h₁ : { Γ := Γ.alt, rank := m }.Boldface P) (h₂ : { Γ := Γ, rank := m }.Boldface Q) :

{ Γ := Γ, rank := m }.Boldface fun (v : Fin k → V) => P v → Q v

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.iff {V : Type u_2} [LO.ORingStruc V] {k : ℕ} {P : (Fin k → V) → Prop} {Q : (Fin k → V) → Prop} {m : ℕ} (h₁ : { Γ := 𝚫, rank := m }.Boldface P) (h₂ : { Γ := 𝚫, rank := m }.Boldface Q) {Γ : LO.SigmaPiDelta} :

{ Γ := Γ, rank := m }.Boldface fun (v : Fin k → V) => P v ↔ Q v

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.all {V : Type u_2} [LO.ORingStruc V] {k : ℕ} {s : ℕ} {P : (Fin k → V) → V → Prop} (h : { Γ := 𝚷, rank := s + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0)) :

{ Γ := 𝚷, rank := s + 1 }.Boldface fun (v : Fin k → V) => ∀ (x : V), P v x

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ex {V : Type u_2} [LO.ORingStruc V] {k : ℕ} {s : ℕ} {P : (Fin k → V) → V → Prop} (h : { Γ := 𝚺, rank := s + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0)) :

{ Γ := 𝚺, rank := s + 1 }.Boldface fun (v : Fin k → V) => ∃ (x : V), P v x

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.equal' {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : ℕ} (i : Fin k) (j : Fin k) :

ℌ.Boldface fun (v : Fin k → V) => v i = v j

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_sigma {V : Type u_2} [LO.ORingStruc V] {k : ℕ} {m : ℕ} {f : (Fin k → V) → V} (h : { Γ := 𝚺, rank := m }.BoldfaceFunction f) {Γ : LO.SigmaPiDelta} :

{ Γ := Γ, rank := m }.BoldfaceFunction f

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.exVec {V : Type u_2} [LO.ORingStruc V] {m : ℕ} {k : ℕ} {l : ℕ} {P : (Fin k → V) → (Fin l → V) → 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 k → V) => ∃ (ys : Fin l → V), P v ys

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.allVec {V : Type u_2} [LO.ORingStruc V] {m : ℕ} {k : ℕ} {l : ℕ} {P : (Fin k → V) → (Fin l → V) → 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 k → V) => ∀ (ys : Fin l → V), P v ys

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.substitution {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {k : ℕ} {P : (Fin k → V) → Prop} {l : ℕ} {m : ℕ} {f : Fin k → (Fin l → V) → V} (hP : { Γ := Γ, rank := m + 1 }.Boldface P) (hf : ∀ (i : Fin k), { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction (f i)) :

{ Γ := Γ, rank := m + 1 }.Boldface fun (z : Fin l → V) => P fun (i : Fin k) => f i z

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfacePred.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {P : V → Prop} {k : ℕ} {f : (Fin k → V) → V} (hP : { Γ := Γ, rank := m + 1 }-Predicate P) (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) :

{ Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin k → V) => P (f v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {P : V → V → Prop} {k : ℕ} {f : (Fin k → V) → V} {g : (Fin k → V) → 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 k → V) => P (f v) (g v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₃.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {P : V → V → V → Prop} {f₁ : (Fin k → V) → V} {f₂ : (Fin k → V) → V} {f₃ : (Fin k → V) → 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 k → V) => P (f₁ v) (f₂ v) (f₃ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₄.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {P : V → V → V → V → Prop} {f₁ : (Fin k → V) → V} {f₂ : (Fin k → V) → V} {f₃ : (Fin k → V) → V} {f₄ : (Fin k → V) → 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 k → V) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₅.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {P : V → V → V → V → V → Prop} {f₁ : (Fin k → V) → V} {f₂ : (Fin k → V) → V} {f₃ : (Fin k → V) → V} {f₄ : (Fin k → V) → V} {f₅ : (Fin k → V) → 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 k → V) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₁ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {P : V → Prop} {f : (Fin k → V) → V} [{ Γ := Γ, rank := m + 1 }-Predicate P] (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) :

{ Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin k → V) => P (f v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₂ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {P : V → V → Prop} {f : (Fin k → V) → V} {g : (Fin k → V) → 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 k → V) => P (f v) (g v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₃ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {P : V → V → V → Prop} {f₁ : (Fin k → V) → V} {f₂ : (Fin k → V) → V} {f₃ : (Fin k → V) → 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 k → V) => P (f₁ v) (f₂ v) (f₃ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₄ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {P : V → V → V → V → Prop} {f₁ : (Fin k → V) → V} {f₂ : (Fin k → V) → V} {f₃ : (Fin k → V) → V} {f₄ : (Fin k → V) → 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 k → V) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₅ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {P : V → V → V → V → V → Prop} {f₁ : (Fin k → V) → V} {f₂ : (Fin k → V) → V} {f₃ : (Fin k → V) → V} {f₄ : (Fin k → V) → V} {f₅ : (Fin k → V) → 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 k → V) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfacePred.of_iff {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {P : V → Prop} {Q : V → Prop} (H : ℌ-Predicate Q) (h : ∀ (x : V), P x ↔ Q x) :

ℌ-Predicate P

source

instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₁.graph {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {f : V → V} [h : ℌ-Function₁ f] :

ℌ-Relation Function.Graph f

Equations

⋯ = h

source

instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.graph {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {f : V → V → V} [h : ℌ-Function₂ f] :

ℌ-Relation₃ Function.Graph₂ f

Equations

⋯ = h

source

instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₃.graph {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {f : V → V → V → V} [h : ℌ-Function₃ f] :

ℌ-Relation₄ Function.Graph₃ f

Equations

⋯ = h

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.graph_delta {V : Type u_2} [LO.ORingStruc V] {m : ℕ} {k : ℕ} {f : (Fin k → V) → V} (h : { Γ := 𝚺, rank := m }.BoldfaceFunction f) :

{ Γ := 𝚫, rank := m }.BoldfaceFunction f

source

instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.instMkDeltaSigmaPiDeltaOfSigma {V : Type u_2} [LO.ORingStruc V] {m : ℕ} {k : ℕ} {f : (Fin k → V) → V} [h : { Γ := 𝚺, rank := m }.BoldfaceFunction f] :

{ Γ := 𝚫, rank := m }.BoldfaceFunction f

Equations

⋯ = ⋯

source

instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.instOfSigmaZero {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : ℕ} {f : (Fin k → V) → V} [𝚺₀.BoldfaceFunction f] :

ℌ.BoldfaceFunction f

Equations

⋯ = ⋯

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.of_sigmaOne {V : Type u_2} [LO.ORingStruc V] {k : ℕ} {f : (Fin k → V) → V} (h : 𝚺₁.BoldfaceFunction f) {Γ : LO.SigmaPiDelta} {m : ℕ} :

{ Γ := Γ, rank := m + 1 }.BoldfaceFunction f

source

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.var {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : ℕ} (i : Fin k) :

ℌ.BoldfaceFunction fun (v : Fin k → V) => v i

source

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.const {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {k : ℕ} (c : V) :

ℌ.BoldfaceFunction fun (x : Fin k → V) => c

source

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.term_retraction (n : ℕ) {V : Type u_2} [LO.ORingStruc V] {k : ℕ} {ℌ : LO.FirstOrder.Arith.HierarchySymbol} (t : LO.FirstOrder.Semiterm ℒₒᵣ V n) (e : Fin n → Fin k) :

ℌ.BoldfaceFunction fun (v : Fin k → V) => LO.FirstOrder.Semiterm.valm V (fun (x : Fin n) => v (e x)) id t

source

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.term {V : Type u_2} [LO.ORingStruc V] {k : ℕ} {ℌ : LO.FirstOrder.Arith.HierarchySymbol} (t : LO.FirstOrder.Semiterm ℒₒᵣ V k) :

ℌ.BoldfaceFunction fun (v : Fin k → V) => LO.FirstOrder.Semiterm.valm V v id t

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.of_eq {V : Type u_2} [LO.ORingStruc V] {k : ℕ} {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {f : (Fin k → V) → V} (g : (Fin k → V) → V) (h : ∀ (v : Fin k → V), f v = g v) (H : ℌ.BoldfaceFunction f) :

ℌ.BoldfaceFunction g

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.retraction {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {n : ℕ} {k : ℕ} {f : (Fin k → V) → V} (hf : ℌ.BoldfaceFunction f) (e : Fin k → Fin n) :

ℌ.BoldfaceFunction fun (v : Fin n → V) => f fun (i : Fin k) => v (e i)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.retractiont {V : Type u_2} [LO.ORingStruc V] {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {n : ℕ} {k : ℕ} {f : (Fin k → V) → V} (hf : ℌ.BoldfaceFunction f) (t : Fin k → LO.FirstOrder.Semiterm ℒₒᵣ V n) :

ℌ.BoldfaceFunction fun (v : Fin n → V) => f fun (i : Fin k) => LO.FirstOrder.Semiterm.valm V v id (t i)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.rel {V : Type u_2} [LO.ORingStruc V] {k : ℕ} {ℌ : LO.FirstOrder.Arith.HierarchySymbol} {f : (Fin k → V) → V} (h : ℌ.BoldfaceFunction f) :

ℌ.Boldface fun (v : Fin k.succ → V) => v 0 = f fun (x : Fin k) => v x.succ

source

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.nth {V : Type u_2} [LO.ORingStruc V] {k : ℕ} (ℌ : LO.FirstOrder.Arith.HierarchySymbol) (i : Fin k) :

ℌ.BoldfaceFunction fun (w : Fin k → V) => w i

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.substitution {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {k : ℕ} {l : ℕ} {m : ℕ} {F : (Fin k → V) → V} {f : Fin k → (Fin l → V) → V} (hF : { Γ := Γ, rank := m + 1 }.BoldfaceFunction F) (hf : ∀ (i : Fin k), { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction (f i)) :

{ Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (z : Fin l → V) => F fun (i : Fin k) => f i z

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₁.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {F : V → V} {f : (Fin k → V) → V} (hF : { Γ := Γ, rank := m + 1 }-Function₁ F) (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) :

{ Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin k → V) => F (f v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {F : V → V → V} {f₁ : (Fin k → V) → V} {f₂ : (Fin k → V) → 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 k → V) => F (f₁ v) (f₂ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₃.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {F : V → V → V → V} {f₁ : (Fin k → V) → V} {f₂ : (Fin k → V) → V} {f₃ : (Fin k → V) → 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 k → V) => F (f₁ v) (f₂ v) (f₃ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₄.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {F : V → V → V → V → V} {f₁ : (Fin k → V) → V} {f₂ : (Fin k → V) → V} {f₃ : (Fin k → V) → V} {f₄ : (Fin k → V) → 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 k → V) => F (f₁ v) (f₂ v) (f₃ v) (f₄ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₅.comp {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {F : V → V → V → V → V → V} {f₁ : (Fin k → V) → V} {f₂ : (Fin k → V) → V} {f₃ : (Fin k → V) → V} {f₄ : (Fin k → V) → V} {f₅ : (Fin k → V) → 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 k → V) => F (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₁ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {f : V → V} [{ Γ := Γ, rank := m + 1 }-Function₁ f] {g : (Fin k → V) → V} (hg : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g) :

{ Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin k → V) => f (g v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₂ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {f : V → V → V} [{ Γ := Γ, rank := m + 1 }-Function₂ f] {g₁ : (Fin k → V) → V} {g₂ : (Fin k → V) → V} (hg₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₁) (hg₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₂) :

{ Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin k → V) => f (g₁ v) (g₂ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₃ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {f : V → V → V → V} [{ Γ := Γ, rank := m + 1 }-Function₃ f] {g₁ : (Fin k → V) → V} {g₂ : (Fin k → V) → V} {g₃ : (Fin k → V) → 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 k → V) => f (g₁ v) (g₂ v) (g₃ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₄ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {f : V → V → V → V → V} [{ Γ := Γ, rank := m + 1 }-Function₄ f] {g₁ : (Fin k → V) → V} {g₂ : (Fin k → V) → V} {g₃ : (Fin k → V) → V} {g₄ : (Fin k → V) → 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 k → V) => f (g₁ v) (g₂ v) (g₃ v) (g₄ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₅ {V : Type u_2} [LO.ORingStruc V] {Γ : LO.SigmaPiDelta} {m : ℕ} {k : ℕ} {f : V → V → V → V → V → V} [{ Γ := Γ, rank := m + 1 }.BoldfaceFunction₅ f] {g₁ : (Fin k → V) → V} {g₂ : (Fin k → V) → V} {g₃ : (Fin k → V) → V} {g₄ : (Fin k → V) → V} {g₅ : (Fin k → V) → 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 k → V) => f (g₁ v) (g₂ v) (g₃ v) (g₄ v) (g₅ v)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_lt {V : Type u_2} [LO.ORingStruc V] {k : ℕ} {m : ℕ} {Γ : LO.SigmaPiDelta} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0)) :

{ Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin k → V) => ∀ x < f v, P v x

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_lt {V : Type u_2} [LO.ORingStruc V] {k : ℕ} {m : ℕ} {Γ : LO.SigmaPiDelta} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0)) :

{ Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin k → V) => ∃ x < f v, P v x

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_le {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} {m : ℕ} {Γ : LO.SigmaPiDelta} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0)) :

{ Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin k → V) => ∀ x ≤ f v, P v x

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_le {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} {m : ℕ} {Γ : LO.SigmaPiDelta} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0)) :

{ Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin k → V) => ∃ x ≤ f v, P v x

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_lt' {V : Type u_2} [LO.ORingStruc V] {k : ℕ} {m : ℕ} {Γ : LO.SigmaPiDelta} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0)) :

{ Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin k → V) => ∀ {x : V}, x < f v → P v x

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_le' {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} {m : ℕ} {Γ : LO.SigmaPiDelta} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0)) :

{ Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin k → V) => ∀ {x : V}, x ≤ f v → P v x