Arithmetization.ISigmaOne.Bit

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

source

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

source

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 } }

source

theorem LO.FirstOrder.Arith.operator_mem_def :

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

source

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.

source

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.

source

@[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”)

source

@[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

source

@[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

source

def LO.FirstOrder.Arith.memRel :

𝚺₀.Semisentence 3

Equations

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

source

def LO.FirstOrder.Arith.memRel₃ :

𝚺₀.Semisentence 4

Equations

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

source

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 }

source

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₃ }

source

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

Lean.ParserDescr

Equations

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

source

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

Lean.ParserDescr

Equations

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

source

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

Lean.ParserDescr

Equations

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

source

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

Lean.ParserDescr

Equations

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

source

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

Lean.ParserDescr

Equations

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

source

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

Lean.ParserDescr

Equations

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

source

@[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₂])

source

@[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₃])

source

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

LO.FirstOrder.Structure.Mem ℒₒᵣ V

Equations

⋯ = ⋯

source

@[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

source

@[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

source

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

source

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₃

source

@[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

source

@[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

source

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

source

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

source

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

EmptyCollection V

Equations

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

source

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

∅ = 0

source

@[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 ∉ ∅

source

@[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

source

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 }

source

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

source

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

Equations

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

source

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

Equations

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

source

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 }

source

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

source

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 ∅

source

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

LawfulSingleton V V

Equations

⋯ = ⋯

source

@[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

source

@[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

source

@[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

source

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

source

def LO.FirstOrder.Arith.insertDef :

𝚺₀.Semisentence 3

Equations

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

source

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

source

@[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)

source

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

𝚺₀ -Function₂ insert

Equations

⋯ = ⋯

source

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

⋯ = ⋯

source

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

source

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

1 = {∅}

source

@[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

source

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

source

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

source

@[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

source

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

source

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

source

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

source

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

source

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‖

source

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

source

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 }

source

def LO.FirstOrder.Arith.bitSubsetDef :

𝚺₀.Semisentence 2

Equations

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

source

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

source

@[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

source

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

⋯ = ⋯

source

@[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

⋯ = ⋯

source

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

source

@[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

source

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

source

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

source

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

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

Equations

LO.Arith.under a = exp a - 1

Instances For

source

@[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

source

@[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

source

@[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

source

def LO.FirstOrder.Arith.underDef :

𝚺₀.Semisentence 2

Equations

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

source

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

source

@[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)

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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

source

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

source

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

source

@[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

source

@[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

source

@[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

source

@[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

source

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

source

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

source

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 ≠ ∅

source

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

source

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

source

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

source

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

source

@[simp]

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

∅ ⊆ s

source

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

source

@[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

source

@[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 = ∅

source

@[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)

source

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

source

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

source

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

source

instance LO.Arith.instFactLeOfNat_arithmetization :

Fact (1 ≤ 1)

Equations

LO.Arith.instFactLeOfNat_arithmetization = ⋯

source

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

source

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

source

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