Arithmetization.Definability.Boldface

source

def LO.FirstOrder.Defined {V : Type u_1} {L : Language} {k : ℕ} (R : (Fin k → V) → Prop) [Structure L V] (φ : Semisentence L k) :

Prop

Equations

LO.FirstOrder.Defined R φ = ∀ (v : Fin k → V), R v ↔ V ⊧/v φ

source

def LO.FirstOrder.DefinedWithParam {V : Type u_1} {L : Language} {k : ℕ} (R : (Fin k → V) → Prop) [Structure L V] (φ : Semiformula L V k) :

Prop

Equations

LO.FirstOrder.DefinedWithParam R φ = ∀ (v : Fin k → V), R v ↔ (LO.FirstOrder.Semiformula.Evalm V v id) φ

source

theorem LO.FirstOrder.Defined.iff {L : Language} {V : Type u_2} [Structure L V] {k : ℕ} {R : (Fin k → V) → Prop} {φ : Semisentence L k} (h : Defined R φ) (v : Fin k → V) :

V ⊧/v φ ↔ R v

source

theorem LO.FirstOrder.DefinedWithParam.iff {L : Language} {V : Type u_2} [Structure L V] {k : ℕ} {R : (Fin k → V) → Prop} {φ : Semiformula L V k} (h : DefinedWithParam R φ) (v : Fin k → V) :

(Semiformula.Evalm V v id) φ ↔ R v

source

def LO.FirstOrder.Arith.HierarchySymbol.Defined {V : Type u_2} [ORingStruc V] {k : ℕ} (R : (Fin k → V) → Prop) {ℌ : HierarchySymbol} :

ℌ.Semisentence k → Prop

Equations

One or more equations did not get rendered due to their size.
LO.FirstOrder.Arith.HierarchySymbol.Defined R φ = LO.FirstOrder.Defined R (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ)
LO.FirstOrder.Arith.HierarchySymbol.Defined R φ = LO.FirstOrder.Defined R (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ)

source

def LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam {V : Type u_2} [ORingStruc V] {k : ℕ} (R : (Fin k → V) → Prop) {ℌ : HierarchySymbol} :

HierarchySymbol.Semiformula V k ℌ → Prop

Equations

LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam R φ = LO.FirstOrder.DefinedWithParam R φ.val
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam R φ = LO.FirstOrder.DefinedWithParam R φ.val
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam R φ = (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn V φ ∧ LO.FirstOrder.DefinedWithParam R φ.val)

source

class LO.FirstOrder.Arith.HierarchySymbol.Lightface {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) {k : ℕ} (P : (Fin k → V) → Prop) :

Prop

definable : ∃ (φ : ℌ.Semisentence k), Defined P φ

Instances

source

class LO.FirstOrder.Arith.HierarchySymbol.Boldface {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) {k : ℕ} (P : (Fin k → V) → Prop) :

Prop

definable : ∃ (φ : HierarchySymbol.Semiformula V k ℌ), DefinedWithParam P φ

Instances

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedPred {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (P : V → Prop) (φ : ℌ.Semisentence 1) :

Prop

Equations

(ℌ-Predicate P via φ) = LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 1 → V) => P (v 0)) φ

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedRel {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (R : V → V → Prop) (φ : ℌ.Semisentence 2) :

Prop

Equations

(ℌ-Relation R via φ) = LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 2 → V) => R (v 0) (v 1)) φ

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedRel₃ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (R : V → V → V → Prop) (φ : ℌ.Semisentence 3) :

Prop

Equations

(ℌ-Relation₃ R via φ) = LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 3 → V) => R (v 0) (v 1) (v 2)) φ

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedRel₄ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (R : V → V → V → V → Prop) (φ : ℌ.Semisentence 4) :

Prop

Equations

(ℌ-Relation₄ R via φ) = LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 4 → V) => R (v 0) (v 1) (v 2) (v 3)) φ

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} (f : (Fin k → V) → V) (φ : ℌ.Semisentence (k + 1)) :

Prop

Equations

LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction f φ = LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin (k + 1) → V) => v 0 = f fun (x : Fin k) => v x.succ) φ

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₀ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (c : V) (φ : ℌ.Semisentence 1) :

Prop

Equations

(ℌ-Function₀ c via φ) = LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (x : Fin 0 → V) => c) φ

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₁ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : V → V) (φ : ℌ.Semisentence 2) :

Prop

Equations

(ℌ-Function₁ f via φ) = LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 1 → V) => f (v 0)) φ

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₂ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : V → V → V) (φ : ℌ.Semisentence 3) :

Prop

Equations

(ℌ-Function₂ f via φ) = LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 2 → V) => f (v 0) (v 1)) φ

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₃ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : V → V → V → V) (φ : ℌ.Semisentence 4) :

Prop

Equations

(ℌ-Function₃ f via φ) = LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 3 → V) => f (v 0) (v 1) (v 2)) φ

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₄ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : V → V → V → V → V) (φ : ℌ.Semisentence 5) :

Prop

Equations

(ℌ-Function₄ f via φ) = LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 4 → V) => f (v 0) (v 1) (v 2) (v 3)) φ

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₅ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : V → V → V → V → V → V) (φ : ℌ.Semisentence 6) :

Prop

Equations

(ℌ-Function₅ f via φ) = LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 5 → V) => f (v 0) (v 1) (v 2) (v 3) (v 4)) φ

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfacePred {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (P : V → Prop) :

Prop

Equations

(ℌ-Predicate P) = ℌ.Boldface fun (v : Fin 1 → V) => P (v 0)

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (P : V → V → Prop) :

Prop

Equations

(ℌ-Relation P) = ℌ.Boldface fun (v : Fin 2 → V) => P (v 0) (v 1)

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₃ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (P : V → V → V → Prop) :

Prop

Equations

(ℌ-Relation₃ P) = ℌ.Boldface fun (v : Fin 3 → V) => P (v 0) (v 1) (v 2)

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₄ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (P : V → V → V → V → Prop) :

Prop

Equations

(ℌ-Relation₄ P) = ℌ.Boldface fun (v : Fin 4 → V) => P (v 0) (v 1) (v 2) (v 3)

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₅ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (P : V → V → V → V → V → Prop) :

Prop

Equations

(ℌ-Relation₅ P) = ℌ.Boldface fun (v : Fin 5 → V) => P (v 0) (v 1) (v 2) (v 3) (v 4)

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₆ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (P : V → V → V → V → V → V → Prop) :

Prop

Equations

ℌ.BoldfaceRel₆ P = ℌ.Boldface fun (v : Fin 6 → V) => P (v 0) (v 1) (v 2) (v 3) (v 4) (v 5)

source

@[reducible, inline]

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

Prop

Equations

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

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₀ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (c : V) :

Prop

Equations

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

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₁ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : V → V) :

Prop

Equations

(ℌ-Function₁ f) = ℌ.BoldfaceFunction fun (v : Fin 1 → V) => f (v 0)

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : V → V → V) :

Prop

Equations

(ℌ-Function₂ f) = ℌ.BoldfaceFunction fun (v : Fin 2 → V) => f (v 0) (v 1)

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₃ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : V → V → V → V) :

Prop

Equations

(ℌ-Function₃ f) = ℌ.BoldfaceFunction fun (v : Fin 3 → V) => f (v 0) (v 1) (v 2)

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₄ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : V → V → V → V → V) :

Prop

Equations

(ℌ-Function₄ f) = ℌ.BoldfaceFunction fun (v : Fin 4 → V) => f (v 0) (v 1) (v 2) (v 3)

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₅ {V : Type u_2} [ORingStruc V] (ℌ : HierarchySymbol) (f : V → V → V → V → V → V) :

Prop

Equations

ℌ.BoldfaceFunction₅ f = ℌ.BoldfaceFunction fun (v : Fin 5 → V) => f (v 0) (v 1) (v 2) (v 3) (v 4)

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Predicate_Via_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Relation_Via_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Relation₃_Via_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Relation₄_Via_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Function₀_Via_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Function₁_Via_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Function₂_Via_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Function₃_Via_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Function₄_Via_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Function₅_Via_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Predicate_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Relation_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Relation₃_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Relation₄_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Relation₅_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Function₁_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Function₂_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Function₃_» :

Lean.TrailingParserDescr

Equations

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

source

def LO.FirstOrder.Arith.HierarchySymbol.«term_-Function₄_» :

Lean.TrailingParserDescr

Equations

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

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.df {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {R : (Fin k → V) → Prop} {φ : ℌ.Semisentence k} (h : Defined R φ) :

FirstOrder.Defined R (Semiformula.val φ)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.proper {V : Type u_2} [ORingStruc V] {k : ℕ} {R : (Fin k → V) → Prop} {m : ℕ} {φ : { Γ := 𝚫, rank := m }.Semisentence k} (h : Defined R φ) :

Semiformula.ProperOn V φ

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.of_zero {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {R : (Fin k → V) → Prop} {φ : 𝚺₀.Semisentence k} (h : Defined R φ) :

Defined R (Semiformula.ofZero φ ℌ)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.emb {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {R : (Fin k → V) → Prop} {φ : ℌ.Semisentence k} (h : Defined R φ) :

Defined R (Semiformula.emb φ)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.of_iff {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P Q : (Fin k → V) → Prop} (h : ∀ (x : Fin k → V), P x ↔ Q x) {φ : ℌ.Semisentence k} (H : Defined Q φ) :

Defined P φ

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.to_definable {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} (φ : ℌ.Semisentence k) (hP : Defined P φ) :

ℌ.Boldface P

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.to_definable₀ {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} {φ : 𝚺₀.Semisentence k} (hP : Defined P φ) :

ℌ.Boldface P

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.to_definable_oRing {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} (φ : ℌ.Semisentence k) (hP : Defined P φ) :

ℌ.Boldface P

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Defined.to_definable_oRing₀ {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} (φ : 𝚺₀.Semisentence k) (hP : Defined P φ) :

ℌ.Boldface P

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction.of_eq {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {f g : (Fin k → V) → V} (h : ∀ (x : Fin k → V), f x = g x) {φ : ℌ.Semisentence (k + 1)} (H : DefinedFunction f φ) :

DefinedFunction g φ

source

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

DefinedFunction f (Semiformula.graphDelta φ)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.df {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {R : (Fin k → V) → Prop} {φ : HierarchySymbol.Semiformula V k ℌ} (h : DefinedWithParam R φ) :

FirstOrder.DefinedWithParam R φ.val

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.proper {V : Type u_2} [ORingStruc V] {k : ℕ} {R : (Fin k → V) → Prop} {m : ℕ} {φ : HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }} (h : DefinedWithParam R φ) :

Semiformula.ProperWithParamOn V φ

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.of_zero {V : Type u_2} [ORingStruc V] {k : ℕ} {R : (Fin k → V) → Prop} {Γ' : SigmaPiDelta} {φ : HierarchySymbol.Semiformula V k { Γ := Γ', rank := 0 }} (h : DefinedWithParam R φ) {Γ : HierarchySymbol} :

DefinedWithParam R (φ.ofZero Γ)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.of_deltaOne {V : Type u_2} [ORingStruc V] {k : ℕ} {R : (Fin k → V) → Prop} {Γ : SigmaPiDelta} {m : ℕ} {φ : HierarchySymbol.Semiformula V k 𝚫₁} (h : DefinedWithParam R φ) :

DefinedWithParam R (φ.ofDeltaOne Γ m)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.emb {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {R : (Fin k → V) → Prop} {φ : HierarchySymbol.Semiformula V k ℌ} (h : DefinedWithParam R φ) :

DefinedWithParam R φ.emb

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.of_iff {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P Q : (Fin k → V) → Prop} (h : ∀ (x : Fin k → V), P x ↔ Q x) {φ : HierarchySymbol.Semiformula V k ℌ} (H : DefinedWithParam Q φ) :

DefinedWithParam P φ

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.to_definable {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} {φ : HierarchySymbol.Semiformula V k ℌ} (h : DefinedWithParam P φ) :

ℌ.Boldface P

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.to_definable₀ {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} {Γ' : SigmaPiDelta} {φ : HierarchySymbol.Semiformula V k { Γ := Γ', rank := 0 }} (h : DefinedWithParam P φ) :

ℌ.Boldface P

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.to_definable_deltaOne {V : Type u_2} [ORingStruc V] {k : ℕ} {P : (Fin k → V) → Prop} {φ : HierarchySymbol.Semiformula V k 𝚫₁} {Γ : SigmaPiDelta} {m : ℕ} (h : DefinedWithParam P φ) :

{ Γ := Γ, rank := m + 1 }.Boldface P

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.retraction {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} {l : ℕ} {φ : HierarchySymbol.Semiformula V k ℌ} (hp : DefinedWithParam P φ) (f : Fin k → Fin l) :

DefinedWithParam (fun (v : Fin l → V) => P fun (i : Fin k) => v (f i)) (Semiformula.rew (Rew.substs fun (x : Fin k) => Semiterm.bvar (f x)) φ)

source

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.verum {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} :

DefinedWithParam (fun (x : Fin k → V) => True) ⊤

source

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.falsum {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} :

DefinedWithParam (fun (x : Fin k → V) => False) ⊥

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.and {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P Q : (Fin k → V) → Prop} {φ ψ : HierarchySymbol.Semiformula V k ℌ} (hp : DefinedWithParam P φ) (hq : DefinedWithParam Q ψ) :

DefinedWithParam (fun (x : Fin k → V) => P x ∧ Q x) (φ ⋏ ψ)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.or {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P Q : (Fin k → V) → Prop} {φ ψ : HierarchySymbol.Semiformula V k ℌ} (hp : DefinedWithParam P φ) (hq : DefinedWithParam Q ψ) :

DefinedWithParam (fun (x : Fin k → V) => P x ∨ Q x) (φ ⋎ ψ)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.negSigma {V : Type u_2} [ORingStruc V] {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} {φ : HierarchySymbol.Semiformula V k { Γ := 𝚺, rank := m }} (hp : DefinedWithParam P φ) :

DefinedWithParam (fun (x : Fin k → V) => ¬P x) φ.negSigma

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.negPi {V : Type u_2} [ORingStruc V] {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} {φ : HierarchySymbol.Semiformula V k { Γ := 𝚷, rank := m }} (hp : DefinedWithParam P φ) :

DefinedWithParam (fun (x : Fin k → V) => ¬P x) φ.negPi

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.not {V : Type u_2} [ORingStruc V] {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} {φ : HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }} (hp : DefinedWithParam P φ) :

DefinedWithParam (fun (x : Fin k → V) => ¬P x) (∼φ)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.imp {V : Type u_2} [ORingStruc V] {k : ℕ} {P Q : (Fin k → V) → Prop} {m : ℕ} {φ ψ : HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }} (hp : DefinedWithParam P φ) (hq : DefinedWithParam Q ψ) :

DefinedWithParam (fun (x : Fin k → V) => P x → Q x) (φ ➝ ψ)

source

theorem LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.iff {V : Type u_2} [ORingStruc V] {k : ℕ} {P Q : (Fin k → V) → Prop} {m : ℕ} {φ ψ : HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }} (hp : DefinedWithParam P φ) (hq : DefinedWithParam Q ψ) :

DefinedWithParam (fun (x : Fin k → V) => P x ↔ Q x) (φ ⭤ ψ)

source

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 k → V) => ∀ x < Semiterm.valm V v id t, P (x :> v)) (Semiformula.ball t φ)

source

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 k → V) => ∃ x < Semiterm.valm V v id t, P (x :> v)) (Semiformula.bex t φ)

source

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 k → V) => ∃ (x : V), P (x :> v)) φ.ex

source

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 k → V) => ∀ (x : V), P (x :> v)) φ.all

source

@[simp]

instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel.eq {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} :

ℌ-Relation Eq

source

@[simp]

instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel.lt {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} :

ℌ-Relation LT.lt

source

@[simp]

instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel.le {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} [V ⊧ₘ* 𝐏𝐀⁻] :

ℌ-Relation LE.le

source

@[simp]

instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.add {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} :

ℌ-Function₂ fun (x1 x2 : V) => x1 + x2

source

@[simp]

instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.mul {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} :

ℌ-Function₂ fun (x1 x2 : V) => x1 * x2

source

@[simp]

instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.hAdd {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} :

ℌ-Function₂ HAdd.hAdd

source

@[simp]

instance LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.hMul {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} :

ℌ-Function₂ HMul.hMul

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.mkPolarity {V : Type u_2} [ORingStruc V] {k m : ℕ} {P : (Fin k → V) → Prop} {Γ : Polarity} (φ : Semiformula ℒₒᵣ V k) (hp : Hierarchy Γ m φ) (hP : ∀ (v : Fin k → V), P v ↔ (Semiformula.Evalm V v id) φ) :

{ Γ := Γ.coe, rank := m }.Boldface P

source

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

ℌ.Boldface P

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_oRing {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} (h : ℌ.Boldface P) :

ℌ.Boldface P

source

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

{ Γ := Γ, rank := m }.Boldface P

source

instance LO.FirstOrder.Arith.HierarchySymbol.Boldface.instMkOfDeltaSigmaPiDelta {V : Type u_2} [ORingStruc V] {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} [{ Γ := 𝚫, rank := m }.Boldface P] (Γ : SigmaPiDelta) :

{ Γ := Γ, rank := m }.Boldface P

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_sigma_of_pi {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {k : ℕ} {P : (Fin k → V) → Prop} {m : ℕ} (hσ : { Γ := 𝚺, rank := m }.Boldface P) (hπ : { Γ := 𝚷, rank := m }.Boldface P) :

{ Γ := Γ, rank := m }.Boldface P

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_zero {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} {Γ' : SigmaPiDelta} (h : { Γ := Γ', rank := 0 }.Boldface P) :

ℌ.Boldface P

source

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

{ Γ := Γ, rank := m + 1 }.Boldface P

source

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

ℌ.Boldface P

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.retraction {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P : (Fin k → V) → Prop} (h : ℌ.Boldface P) {n : ℕ} (f : Fin k → Fin n) :

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

source

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

ℌ.Boldface fun (v : Fin n → V) => P fun (i : Fin k) => Semiterm.valm V v id (f i)

source

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.const {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P : Prop} :

ℌ.Boldface fun (x : Fin k → V) => P

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.and {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P Q : (Fin k → V) → Prop} (h₁ : ℌ.Boldface P) (h₂ : ℌ.Boldface Q) :

ℌ.Boldface fun (v : Fin k → V) => P v ∧ Q v

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.conj {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k l : ℕ} {P : Fin l → (Fin k → V) → Prop} (h : ∀ (i : Fin l), ℌ.Boldface fun (w : Fin k → V) => P i w) :

ℌ.Boldface fun (v : Fin k → V) => ∀ (i : Fin l), P i v

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.or {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {P Q : (Fin k → V) → Prop} (h₁ : ℌ.Boldface P) (h₂ : ℌ.Boldface Q) :

ℌ.Boldface fun (v : Fin k → V) => P v ∨ Q v

source

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

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

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.imp {V : Type u_2} [ORingStruc V] {Γ : SigmaPiDelta} {k : ℕ} {P 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} [ORingStruc V] {k : ℕ} {P Q : (Fin k → V) → Prop} {m : ℕ} (h₁ : { Γ := 𝚫, rank := m }.Boldface P) (h₂ : { Γ := 𝚫, rank := m }.Boldface Q) {Γ : 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} [ORingStruc V] {k s : ℕ} {P : (Fin k → V) → V → Prop} (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 k → V) => ∀ (x : V), P v x

source

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

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.equal' {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} (i 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} [ORingStruc V] {k m : ℕ} {f : (Fin k → V) → V} (h : { Γ := 𝚺, rank := m }.BoldfaceFunction f) {Γ : SigmaPiDelta} :

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

source

theorem LO.FirstOrder.Arith.HierarchySymbol.Boldface.exVec {V : Type u_2} [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} [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} [ORingStruc V] {Γ : 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} [ORingStruc V] {Γ : 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} [ORingStruc V] {Γ : SigmaPiDelta} {m : ℕ} {P : V → V → Prop} {k : ℕ} {f 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → V → Prop} {f₁ f₂ 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → V → V → Prop} {f₁ f₂ f₃ 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → V → V → V → Prop} {f₁ f₂ f₃ f₄ 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} [ORingStruc V] {Γ : 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → Prop} {f 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → V → Prop} {f₁ f₂ 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → V → V → Prop} {f₁ f₂ f₃ 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {P : V → V → V → V → V → Prop} {f₁ f₂ f₃ f₄ 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} [ORingStruc V] {ℌ : HierarchySymbol} {P 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} [ORingStruc V] {ℌ : HierarchySymbol} {f : V → V} [h : ℌ-Function₁ f] :

ℌ-Relation Function.Graph f

source

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

ℌ-Relation₃ Function.Graph₂ f

source

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

ℌ-Relation₄ Function.Graph₃ f

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.graph_delta {V : Type u_2} [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} [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.instOfSigmaZero {V : Type u_2} [ORingStruc V] {ℌ : HierarchySymbol} {k : ℕ} {f : (Fin k → V) → V} [𝚺₀.BoldfaceFunction f] :

ℌ.BoldfaceFunction f

source

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

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

source

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.var {V : Type u_2} [ORingStruc V] {ℌ : 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} [ORingStruc V] {ℌ : 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} [ORingStruc V] {k : ℕ} {ℌ : HierarchySymbol} (t : Semiterm ℒₒᵣ V n) (e : Fin n → Fin k) :

ℌ.BoldfaceFunction fun (v : Fin k → V) => 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} [ORingStruc V] {k : ℕ} {ℌ : HierarchySymbol} (t : Semiterm ℒₒᵣ V k) :

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

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.of_eq {V : Type u_2} [ORingStruc V] {k : ℕ} {ℌ : 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} [ORingStruc V] {ℌ : 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} [ORingStruc V] {ℌ : HierarchySymbol} {n k : ℕ} {f : (Fin k → V) → V} (hf : ℌ.BoldfaceFunction f) (t : Fin k → Semiterm ℒₒᵣ V n) :

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

source

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

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

source

@[simp]

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

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

source

theorem LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.substitution {V : Type u_2} [ORingStruc V] {Γ : 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} [ORingStruc V] {Γ : 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {F : V → V → V} {f₁ 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {F : V → V → V → V} {f₁ f₂ 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {F : V → V → V → V → V} {f₁ f₂ f₃ 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {F : V → V → V → V → V → V} {f₁ f₂ f₃ f₄ 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} [ORingStruc V] {Γ : 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {f : V → V → V} [{ Γ := Γ, rank := m + 1 }-Function₂ f] {g₁ 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {f : V → V → V → V} [{ Γ := Γ, rank := m + 1 }-Function₃ f] {g₁ g₂ 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {f : V → V → V → V → V} [{ Γ := Γ, rank := m + 1 }-Function₄ f] {g₁ g₂ g₃ 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} [ORingStruc V] {Γ : SigmaPiDelta} {m k : ℕ} {f : V → V → V → V → V → V} [{ Γ := Γ, rank := m + 1 }.BoldfaceFunction₅ f] {g₁ g₂ g₃ g₄ 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} [ORingStruc V] {k m : ℕ} {Γ : 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 + 1) → 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} [ORingStruc V] {k m : ℕ} {Γ : 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 + 1) → 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} [ORingStruc V] {k m : ℕ} [V ⊧ₘ* 𝐏𝐀⁻] {Γ : 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 + 1) → 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} [ORingStruc V] {k m : ℕ} [V ⊧ₘ* 𝐏𝐀⁻] {Γ : 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 + 1) → 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} [ORingStruc V] {k m : ℕ} {Γ : 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 + 1) → 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} [ORingStruc V] {k m : ℕ} [V ⊧ₘ* 𝐏𝐀⁻] {Γ : 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 + 1) → 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