def LO.Arith.Bit {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) (a : V) : Prop

Equations

• LO.Arith.Bit i a = LO.Arith.LenBit (exp i) a

instance LO.Arith.instMembership_arithmetization {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : Membership V V

Equations

• LO.Arith.instMembership_arithmetization = { mem := LO.Arith.Bit }

def LO.FirstOrder.Arith.bitDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.bit_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Relation fun (x x_1 : V) => x ∈ x_1 via LO.FirstOrder.Arith.bitDef

@[simp]

theorem LO.Arith.bit_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.bitDef) ↔ v 0 ∈ v 1

instance LO.Arith.mem_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Relation fun (x x_1 : V) => x ∈ x_1

Equations

• ⋯ = ⋯

instance LO.Arith.mem_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Relation fun (x x_1 : V) => x ∈ x_1

Equations

• ⋯ = ⋯

theorem LO.Arith.mem_absolute {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (i : ℕ) (a : ℕ) : i ∈ a ↔ ↑i ∈ ↑a

theorem LO.Arith.mem_iff_bit {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} : i ∈ a ↔ LO.Arith.Bit i a

theorem LO.Arith.exp_le_of_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i ∈ a) : exp i ≤ a

theorem LO.Arith.lt_of_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i ∈ a) : i < a

theorem LO.Arith.not_mem_of_lt_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : a < exp i) : i ∉ a

theorem LO.Arith.HierarchySymbol.Boldface.ball_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} (Γ : LO.SigmaPiDelta) (m : ℕ) {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

theorem LO.Arith.HierarchySymbol.Boldface.bex_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : ℕ} (Γ : LO.SigmaPiDelta) (m : ℕ) {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

instance LO.FirstOrder.Arith.instMemORing_arithmetization : LO.FirstOrder.Semiformula.Operator.Mem ℒₒᵣ

Equations

• LO.FirstOrder.Arith.instMemORing_arithmetization = { mem := { sentence := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.bitDef } }

theorem LO.FirstOrder.Arith.operator_mem_def : op(∈).sentence = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.bitDef

def LO.FirstOrder.Arith.ballIn {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n) (p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)) : LO.FirstOrder.Semiformula ℒₒᵣ ξ n

Equations

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

def LO.FirstOrder.Arith.bexIn {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n) (p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)) : LO.FirstOrder.Semiformula ℒₒᵣ ξ n

Equations

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

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.bit {n : ℕ} {μ : Type u_2} {Γ : LO.Polarity} {s : ℕ} {t : LO.FirstOrder.Semiterm ℒₒᵣ μ n} {u : LO.FirstOrder.Semiterm ℒₒᵣ μ n} : LO.FirstOrder.Arith.Hierarchy Γ s (“!!t ∈ !!u”)

@[simp]

theorem LO.FirstOrder.Arith.Hieralchy.ballIn {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {m : ℕ} (t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n) (p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)) : LO.FirstOrder.Arith.Hierarchy Γ m (LO.FirstOrder.Arith.ballIn t p) ↔ LO.FirstOrder.Arith.Hierarchy Γ m p

@[simp]

theorem LO.FirstOrder.Arith.Hieralchy.bexIn {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {m : ℕ} (t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n) (p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)) : LO.FirstOrder.Arith.Hierarchy Γ m (LO.FirstOrder.Arith.bexIn t p) ↔ LO.FirstOrder.Arith.Hierarchy Γ m p

def LO.FirstOrder.Arith.memRel : 𝚺₀.Semisentence 3

Equations

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

def LO.FirstOrder.Arith.memRel₃ : 𝚺₀.Semisentence 4

Equations

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

def LO.FirstOrder.Arith.memRelOpr : LO.FirstOrder.Semiformula.Operator ℒₒᵣ 3

Equations

• LO.FirstOrder.Arith.memRelOpr = { sentence := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.memRel }

def LO.FirstOrder.Arith.memRel₃Opr : LO.FirstOrder.Semiformula.Operator ℒₒᵣ 4

Equations

• LO.FirstOrder.Arith.memRel₃Opr = { sentence := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.memRel₃ }

def LO.FirstOrder.Arith.«first_order_formula∀_∈'_,_» : Lean.ParserDescr

Equations

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

def LO.FirstOrder.Arith.«first_order_formula∃_∈'_,_» : Lean.ParserDescr

Equations

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

def LO.FirstOrder.Arith.«first_order_formula_∼[_]_» : Lean.ParserDescr

Equations

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

def LO.FirstOrder.Arith.«first_order_formula_≁[_]_» : Lean.ParserDescr

Equations

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

def LO.FirstOrder.Arith.«first_order_formula:⟪_,_⟫:∈_» : Lean.ParserDescr

Equations

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

def LO.FirstOrder.Arith.«first_order_formula:⟪_,_,_⟫:∈_» : Lean.ParserDescr

Equations

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

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.memRel {n : ℕ} {μ : Type u_2} {Γ : LO.Polarity} {s : ℕ} {t₁ : LO.FirstOrder.Semiterm ℒₒᵣ μ n} {t₂ : LO.FirstOrder.Semiterm ℒₒᵣ μ n} {u : LO.FirstOrder.Semiterm ℒₒᵣ μ n} : LO.FirstOrder.Arith.Hierarchy Γ s (LO.FirstOrder.Arith.memRelOpr.operator ![u, t₁, t₂])

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.memRel₃ {n : ℕ} {μ : Type u_2} {Γ : LO.Polarity} {s : ℕ} {t₁ : LO.FirstOrder.Semiterm ℒₒᵣ μ n} {t₂ : LO.FirstOrder.Semiterm ℒₒᵣ μ n} {t₃ : LO.FirstOrder.Semiterm ℒₒᵣ μ n} {u : LO.FirstOrder.Semiterm ℒₒᵣ μ n} : LO.FirstOrder.Arith.Hierarchy Γ s (LO.FirstOrder.Arith.memRel₃Opr.operator ![u, t₁, t₂, t₃])

def LO.FirstOrder.Arith.instMemORing_arithmetization_1 {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.FirstOrder.Structure.Mem ℒₒᵣ V

Equations

• ⋯ = ⋯

@[simp]

theorem LO.FirstOrder.Arith.eval_ballIn {ξ : Type u_1} {n : ℕ} {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n} {p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)} {e : Fin n → V} {ε : ξ → V} : (LO.FirstOrder.Semiformula.Evalm V e ε) (LO.FirstOrder.Arith.ballIn t p) ↔ ∀ x ∈ LO.FirstOrder.Semiterm.valm V e ε t, (LO.FirstOrder.Semiformula.Evalm V (x :> e) ε) p

@[simp]

theorem LO.FirstOrder.Arith.eval_bexIn {ξ : Type u_1} {n : ℕ} {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n} {p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)} {e : Fin n → V} {ε : ξ → V} : (LO.FirstOrder.Semiformula.Evalm V e ε) (LO.FirstOrder.Arith.bexIn t p) ↔ ∃ x ∈ LO.FirstOrder.Semiterm.valm V e ε t, (LO.FirstOrder.Semiformula.Evalm V (x :> e) ε) p

theorem LO.FirstOrder.Arith.memRel_defined {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Relation₃ fun (r x y : V) => ⟪x, y⟫ ∈ r via LO.FirstOrder.Arith.memRel

theorem LO.FirstOrder.Arith.memRel₃_defined {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Relation₄ fun (r x y z : V) => ⟪x, ⟪y, z⟫⟫ ∈ r via LO.FirstOrder.Arith.memRel₃

@[simp]

theorem LO.FirstOrder.Arith.eval_memRel {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {r : V} : LO.FirstOrder.Arith.memRelOpr.val ![r, x, y] ↔ ⟪x, y⟫ ∈ r

@[simp]

theorem LO.FirstOrder.Arith.eval_memRel₃ {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {z : V} {r : V} : LO.FirstOrder.Arith.memRel₃Opr.val ![r, x, y, z] ↔ ⟪x, ⟪y, z⟫⟫ ∈ r

theorem LO.Arith.mem_iff_mul_exp_add_exp_add {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} : i ∈ a ↔ ∃ (k : V), ∃ r < exp i, a = k * exp (i + 1) + exp i + r

theorem LO.Arith.not_mem_iff_mul_exp_add {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} : i ∉ a ↔ ∃ (k : V), ∃ r < exp i, a = k * exp (i + 1) + r

def LO.Arith.instEmptyCollection_arithmetization {V : Type u_1} [Zero V] : EmptyCollection V

Equations

• LO.Arith.instEmptyCollection_arithmetization = { emptyCollection := 0 }

theorem LO.Arith.emptyset_def {V : Type u_1} [Zero V] : ∅ = 0

@[simp]

theorem LO.Arith.not_mem_empty {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) : i ∉ ∅

@[simp]

theorem LO.Arith.not_mem_zero {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) : i ∉ 0

def LO.Arith.instSingleton_arithmetization {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] : Singleton V V

Equations

• LO.Arith.instSingleton_arithmetization = { singleton := fun (a : V) => exp a }

theorem LO.Arith.singleton_def {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : {a} = exp a

noncomputable def LO.Arith.bitInsert {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) (a : V) : V

Equations

• LO.Arith.bitInsert i a = if i ∈ a then a else a + exp i

noncomputable def LO.Arith.bitRemove {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) (a : V) : V

Equations

• LO.Arith.bitRemove i a = if i ∈ a then a - exp i else a

def LO.Arith.instInsert_arithmetization {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] : Insert V V

Equations

• LO.Arith.instInsert_arithmetization = { insert := LO.Arith.bitInsert }

theorem LO.Arith.insert_eq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} : insert i a = LO.Arith.bitInsert i a

theorem LO.Arith.singleton_eq_insert {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) : {i} = insert i ∅

instance LO.Arith.instLawfulSingleton_arithmetization {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] : LawfulSingleton V V

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.mem_bitInsert_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {j : V} {a : V} : i ∈ insert j a ↔ i = j ∨ i ∈ a

@[simp]

theorem LO.Arith.mem_bitRemove_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {j : V} {a : V} : i ∈ LO.Arith.bitRemove j a ↔ i ≠ j ∧ i ∈ a

@[simp]

theorem LO.Arith.not_mem_bitRemove_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) (a : V) : i ∉ LO.Arith.bitRemove i a

theorem LO.Arith.insert_graph {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (b : V) (i : V) (a : V) : b = insert i a ↔ i ∈ a ∧ b = a ∨ i ∉ a ∧ ∃ e ≤ b, e = exp i ∧ b = a + e

def LO.FirstOrder.Arith.insertDef : 𝚺₀.Semisentence 3

Equations

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

theorem LO.Arith.insert_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ insert via LO.FirstOrder.Arith.insertDef

@[simp]

theorem LO.Arith.insert_defined_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.insertDef) ↔ v 0 = insert (v 1) (v 2)

instance LO.Arith.insert_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ insert

Equations

• ⋯ = ⋯

instance LO.Arith.insert_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.FirstOrder.Arith.HierarchySymbol) : Γ-Function₂ insert

Equations

• ⋯ = ⋯

theorem LO.Arith.insert_le_of_le_of_le {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {j : V} {a : V} {b : V} (hij : i ≤ j) (hab : a ≤ b) : insert i a ≤ b + exp j

theorem LO.Arith.one_eq_singleton {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] : 1 = {∅}

@[simp]

theorem LO.Arith.mem_singleton_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {j : V} : i ∈ {j} ↔ i = j

theorem LO.Arith.bitRemove_lt_of_mem {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i ∈ a) : LO.Arith.bitRemove i a < a

theorem LO.Arith.pos_of_nonempty {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i ∈ a) : 0 < a

@[simp]

theorem LO.Arith.mem_insert {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) (a : V) : i ∈ insert i a

theorem LO.Arith.insert_eq_self_of_mem {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i ∈ a) : insert i a = a

theorem LO.Arith.log_mem_of_pos {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} (h : 0 < a) : LO.Arith.log a ∈ a

theorem LO.Arith.le_log_of_mem {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i ∈ a) : i ≤ LO.Arith.log a

theorem LO.Arith.succ_mem_iff_mem_div_two {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} : i + 1 ∈ a ↔ i ∈ a / 2

theorem LO.Arith.lt_length_of_mem {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i ∈ a) : i < ‖a‖

theorem LO.Arith.lt_exp_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {i : V} : a < exp i ↔ ∀ j ∈ a, j < i

instance LO.Arith.instHasSubset_arithmetization {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] : HasSubset V

Equations

• LO.Arith.instHasSubset_arithmetization = { Subset := fun (a b : V) => ∀ ⦃i : V⦄, i ∈ a → i ∈ b }

def LO.FirstOrder.Arith.bitSubsetDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.bitSubset_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Relation fun (x x_1 : V) => x ⊆ x_1 via LO.FirstOrder.Arith.bitSubsetDef

@[simp]

theorem LO.Arith.bitSubset_defined_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.bitSubsetDef) ↔ v 0 ⊆ v 1

instance LO.Arith.bitSubset_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Relation fun (x x_1 : V) => x ⊆ x_1

Equations

• ⋯ = ⋯

@[simp]

instance LO.Arith.bitSubset_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Relation fun (x x_1 : V) => x ⊆ x_1

Equations

• ⋯ = ⋯

theorem LO.Arith.subset_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} : a ⊆ b ↔ ∀ x ∈ a, x ∈ b

@[simp]

theorem LO.Arith.subset_refl {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : a ⊆ a

theorem LO.Arith.subset_trans {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} {c : V} (hab : a ⊆ b) (hbc : b ⊆ c) : a ⊆ c

theorem LO.Arith.mem_exp_add_succ_sub_one {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) (j : V) : i ∈ exp (i + j + 1) - 1

def LO.Arith.under {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : V

under a = {0, 1, 2, ..., a - 1}

Equations

• LO.Arith.under a = exp a - 1

@[simp]

theorem LO.Arith.le_under {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : a ≤ LO.Arith.under a

@[simp]

theorem LO.Arith.mem_under_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {j : V} : i ∈ LO.Arith.under j ↔ i < j

@[simp]

theorem LO.Arith.not_mem_under_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) : i ∉ LO.Arith.under i

def LO.FirstOrder.Arith.underDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.under_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.under via LO.FirstOrder.Arith.underDef

@[simp]

theorem LO.Arith.under_defined_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.underDef) ↔ v 0 = LO.Arith.under (v 1)

instance LO.Arith.under_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.under

Equations

• ⋯ = ⋯

instance LO.Arith.under_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.FirstOrder.Arith.HierarchySymbol) : Γ-Function₁ LO.Arith.under

Equations

• ⋯ = ⋯

theorem LO.Arith.eq_zero_of_subset_zero {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} : a ⊆ 0 → a = 0

theorem LO.Arith.subset_div_two {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} : a ⊆ b → a / 2 ⊆ b / 2

theorem LO.Arith.zero_mem_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} : 0 ∉ a ↔ 2 ∣ a

@[simp]

theorem LO.Arith.zero_not_mem {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : 0 ∉ 2 * a

@[simp]

theorem LO.Arith.zero_mem_double_add_one {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : 0 ∈ 2 * a + 1

@[simp]

theorem LO.Arith.succ_mem_two_mul_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} : i + 1 ∈ 2 * a ↔ i ∈ a

@[simp]

theorem LO.Arith.succ_mem_two_mul_succ_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} : i + 1 ∈ 2 * a + 1 ↔ i ∈ a

theorem LO.Arith.le_of_subset {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (h : a ⊆ b) : a ≤ b

theorem LO.Arith.mem_ext {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (h : ∀ (i : V), i ∈ a ↔ i ∈ b) : a = b

theorem LO.Arith.pos_iff_nonempty {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} : 0 < s ↔ s ≠ ∅

theorem LO.Arith.nonempty_of_pos {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} (h : 0 < a) : ∃ (i : V), i ∈ a

theorem LO.Arith.eq_empty_or_nonempty {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : a = ∅ ∨ ∃ (i : V), i ∈ a

theorem LO.Arith.nonempty_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} : s ≠ ∅ ↔ ∃ (x : V), x ∈ s

theorem LO.Arith.isempty_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} : s = ∅ ↔ ∀ (x : V), x ∉ s

@[simp]

theorem LO.Arith.empty_subset {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : ∅ ⊆ s

theorem LO.Arith.lt_of_lt_log {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (pos : 0 < b) (h : ∀ i ∈ a, i < LO.Arith.log b) : a < b

@[simp]

theorem LO.Arith.under_inj {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {j : V} : LO.Arith.under i = LO.Arith.under j ↔ i = j

@[simp]

theorem LO.Arith.under_zero {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.under 0 = ∅

@[simp]

theorem LO.Arith.under_succ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) : LO.Arith.under (i + 1) = insert i (LO.Arith.under i)

theorem LO.Arith.insert_remove {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i ∈ a) : insert i (LO.Arith.bitRemove i a) = a

theorem LO.Arith.finset_comprehension {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] {m : ℕ} [Fact (1 ≤ m)] [V ⊧ₘ* 𝐈𝐍𝐃𝚺 m] {Γ : LO.SigmaPiDelta} {P : V → Prop} (hP : { Γ := Γ, rank := m }-Predicate P) (a : V) : ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i

theorem LO.Arith.finset_comprehension_exists_unique {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] {m : ℕ} [Fact (1 ≤ m)] [V ⊧ₘ* 𝐈𝐍𝐃𝚺 m] {Γ : LO.SigmaPiDelta} {P : V → Prop} (hP : { Γ := Γ, rank := m }-Predicate P) (a : V) : ∃! s : V, s < exp a ∧ ∀ i < a, i ∈ s ↔ P i

instance LO.Arith.instFactLeOfNat_arithmetization : Fact (1 ≤ 1)

Equations

• LO.Arith.instFactLeOfNat_arithmetization = ⋯

theorem LO.Arith.finset_comprehension₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (a : V) : ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i

theorem LO.Arith.finset_comprehension₁! {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (a : V) : ∃! s : V, s < exp a ∧ ∀ i < a, i ∈ s ↔ P i

theorem LO.Arith.finite_comprehension₁! {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (fin : ∃ (m : V), ∀ (i : V), P i → i < m) : ∃! s : V, ∀ (i : V), i ∈ s ↔ P i