Equations
- LO.Arith.Bit i a = LO.Arith.LenBit (exp i) a
Instances For
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 }
Equations
- One or more equations did not get rendered due to their size.
Instances For
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]
Equations
- ⋯ = ⋯
instance
LO.Arith.mem_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
Equations
- ⋯ = ⋯
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)
:
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))
:
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))
:
def
LO.FirstOrder.Arith.ballIn
{ξ : Type u_1}
{n : ℕ}
(t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n)
(p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.FirstOrder.Arith.bexIn
{ξ : Type u_1}
{n : ℕ}
(t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n)
(p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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))
:
@[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))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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 ⊧ₘ* 𝐈𝚺₁]
:
Equations
- ⋯ = ⋯
Instances For
@[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
Equations
- LO.Arith.instEmptyCollection_arithmetization = { emptyCollection := 0 }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.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
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
- ⋯ = ⋯
@[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_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)