$\mathrm{Bit}$ predicate

def FFL.FirstOrder.Arithmetic.Bit {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (i a : V) : Prop

Equations

• FFL.FirstOrder.Arithmetic.Bit i a = FFL.FirstOrder.Arithmetic.LenBit (FFL.Exp.exp i) a

@[instance_reducible]

instance FFL.FirstOrder.Arithmetic.instMembership_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Membership V V

Support for ∈ notation over a model of arithmetic, implemented by binary encoding.

Equations

• FFL.FirstOrder.Arithmetic.instMembership_foundation = { mem := fun (a i : V) => FFL.FirstOrder.Arithmetic.Bit i a }

def FFL.FirstOrder.Arithmetic.bitDef : 𝚺₀.Semisentence 2

Equations

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

instance FFL.FirstOrder.Arithmetic.bit_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Relation fun (x1 x2 : V) => x1 ∈ x2 via bitDef

instance FFL.FirstOrder.Arithmetic.mem_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Relation fun (x1 x2 : V) => x1 ∈ x2

instance FFL.FirstOrder.Arithmetic.mem_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Relation fun (x1 x2 : V) => x1 ∈ x2

instance FFL.FirstOrder.Arithmetic.mem_definable'' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Relation Membership.mem

theorem FFL.FirstOrder.Arithmetic.mem_absolute {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (i a : ℕ) : i ∈ a ↔ ↑i ∈ ↑a

theorem FFL.FirstOrder.Arithmetic.mem_iff_bit {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} : i ∈ a ↔ Bit i a

theorem FFL.FirstOrder.Arithmetic.exp_le_of_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} (h : i ∈ a) : Exp.exp i ≤ a

theorem FFL.FirstOrder.Arithmetic.lt_of_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} (h : i ∈ a) : i < a

theorem FFL.FirstOrder.Arithmetic.not_mem_of_lt_exp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} (h : a < Exp.exp i) : i ∉ a

theorem FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.ball_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {k : ℕ} (Γ : SigmaPiDelta) (m : ℕ) {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f) (h : { Γ := Γ, rank := m + 1 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => ∀ x ∈ f v, P v x

theorem FFL.FirstOrder.Arithmetic.HierarchySymbol.Definable.bexs_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {k : ℕ} (Γ : SigmaPiDelta) (m : ℕ) {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V} (hf : { Γ := 𝚺, rank := m + 1 }.DefinableFunction f) (h : { Γ := Γ, rank := m + 1 }.Definable fun (w : Fin (k + 1) → V) => P (fun (x : Fin k) => w x.succ) (w 0)) : { Γ := Γ, rank := m + 1 }.Definable fun (v : Fin k → V) => ∃ x ∈ f v, P v x

@[instance_reducible]

instance FFL.FirstOrder.Arithmetic.instMemORing : Semiformula.Operator.Mem ℒₒᵣ

Equations

• FFL.FirstOrder.Arithmetic.instMemORing = { mem := { sentence := ↑FFL.FirstOrder.Arithmetic.bitDef } }

theorem FFL.FirstOrder.Arithmetic.operator_mem_def : op(∈).sentence = ↑bitDef

def FFL.FirstOrder.Arithmetic.ballIn {ξ : Type u_2} {n : ℕ} (t : ArithmeticSemiterm ξ n) (p : ArithmeticSemiformula ξ (n + 1)) : ArithmeticSemiformula ξ n

Equations

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

def FFL.FirstOrder.Arithmetic.bexsIn {ξ : Type u_2} {n : ℕ} (t : ArithmeticSemiterm ξ n) (p : ArithmeticSemiformula ξ (n + 1)) : ArithmeticSemiformula ξ n

Equations

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

@[simp]

theorem FFL.FirstOrder.Arithmetic.Hierarchy.bit {n : ℕ} {μ : Type u_3} {Γ : Polarity} {s : ℕ} {t u : ArithmeticSemiterm μ n} : Hierarchy Γ s (“!!t ∈ !!u”)

@[simp]

theorem FFL.FirstOrder.Arithmetic.Hieralchy.ballIn {ξ : Type u_2} {n : ℕ} {Γ : Polarity} {m : ℕ} (t : ArithmeticSemiterm ξ n) (p : ArithmeticSemiformula ξ (n + 1)) : Hierarchy Γ m (Arithmetic.ballIn t p) ↔ Hierarchy Γ m p

@[simp]

theorem FFL.FirstOrder.Arithmetic.Hieralchy.bexsIn {ξ : Type u_2} {n : ℕ} {Γ : Polarity} {m : ℕ} (t : ArithmeticSemiterm ξ n) (p : ArithmeticSemiformula ξ (n + 1)) : Hierarchy Γ m (Arithmetic.bexsIn t p) ↔ Hierarchy Γ m p

def FFL.FirstOrder.Arithmetic.memRel : 𝚺₀.Semisentence 3

Equations

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

def FFL.FirstOrder.Arithmetic.memRel₃ : 𝚺₀.Semisentence 4

Equations

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

def FFL.FirstOrder.Arithmetic.memRelOpr : Semiformula.Operator ℒₒᵣ 3

The relation ⟪x, y⟫ ∈ R in arithmetic, implemented by binary coding, as an operator.

Equations

• FFL.FirstOrder.Arithmetic.memRelOpr = { sentence := ↑FFL.FirstOrder.Arithmetic.memRel }

def FFL.FirstOrder.Arithmetic.memRel₃Opr : Semiformula.Operator ℒₒᵣ 4

Equations

• FFL.FirstOrder.Arithmetic.memRel₃Opr = { sentence := ↑FFL.FirstOrder.Arithmetic.memRel₃ }

def FFL.FirstOrder.Arithmetic.«first_order_formula∀_∈'_,_» : Lean.ParserDescr

Equations

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

def FFL.FirstOrder.Arithmetic.«first_order_formula∃_∈'_,_» : Lean.ParserDescr

Equations

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

def FFL.FirstOrder.Arithmetic.«first_order_formula_∼[_]_» : Lean.ParserDescr

x ~[m] y states that ⟪x, y⟫ is in m, where the notion of "in" is implemented by binary coding.

Equations

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

def FFL.FirstOrder.Arithmetic.«first_order_formula_≁[_]_» : Lean.ParserDescr

Equations

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

def FFL.FirstOrder.Arithmetic.«first_order_formula:⟪_,_⟫:∈_» : Lean.ParserDescr

Equations

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

def FFL.FirstOrder.Arithmetic.«first_order_formula:⟪_,_,_⟫:∈_» : Lean.ParserDescr

Equations

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

@[simp]

theorem FFL.FirstOrder.Arithmetic.Hierarchy.memRel {n : ℕ} {μ : Type u_3} {Γ : Polarity} {s : ℕ} {t₁ t₂ u : ArithmeticSemiterm μ n} : Hierarchy Γ s (memRelOpr.operator ![u, t₁, t₂])

@[simp]

theorem FFL.FirstOrder.Arithmetic.Hierarchy.memRel₃ {n : ℕ} {μ : Type u_3} {Γ : Polarity} {s : ℕ} {t₁ t₂ t₃ u : ArithmeticSemiterm μ n} : Hierarchy Γ s (memRel₃Opr.operator ![u, t₁, t₂, t₃])

theorem FFL.FirstOrder.Arithmetic.instMemORing_1 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Tarski.Structure.Mem ℒₒᵣ V

@[simp]

theorem FFL.FirstOrder.Arithmetic.eval_ballIn {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {ξ : Type u_2} {n : ℕ} {t : ArithmeticSemiterm ξ n} {φ : ArithmeticSemiformula ξ (n + 1)} {bv : Fin n → V} {fv : ξ → V} : (Semiformula.Eval bv fv) (ballIn t φ) ↔ ∀ x ∈ Semiterm.val bv fv t, (Semiformula.Eval (x :> bv) fv) φ

@[simp]

theorem FFL.FirstOrder.Arithmetic.eval_bexsIn {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {ξ : Type u_2} {n : ℕ} {t : ArithmeticSemiterm ξ n} {φ : ArithmeticSemiformula ξ (n + 1)} {bv : Fin n → V} {fv : ξ → V} : (Semiformula.Eval bv fv) (bexsIn t φ) ↔ ∃ x ∈ Semiterm.val bv fv t, (Semiformula.Eval (x :> bv) fv) φ

instance FFL.FirstOrder.Arithmetic.memRel_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Relation₃ fun (r x y : V) => ⟪x, y⟫ ∈ r via memRel

instance FFL.FirstOrder.Arithmetic.memRel₃_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Relation₄ fun (r x y z : V) => ⟪x, ⟪y, z⟫⟫ ∈ r via memRel₃

@[simp]

theorem FFL.FirstOrder.Arithmetic.eval_memRel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x y r : V} : Semiformula.Operator.val ![r, x, y] memRelOpr ↔ ⟪x, y⟫ ∈ r

@[simp]

theorem FFL.FirstOrder.Arithmetic.eval_memRel₃ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x y z r : V} : Semiformula.Operator.val ![r, x, y, z] memRel₃Opr ↔ ⟪x, ⟪y, z⟫⟫ ∈ r

theorem FFL.FirstOrder.Arithmetic.mem_iff_mul_exp_add_exp_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} : i ∈ a ↔ ∃ (k : V), ∃ r < Exp.exp i, a = k * Exp.exp (i + 1) + Exp.exp i + r

theorem FFL.FirstOrder.Arithmetic.not_mem_iff_mul_exp_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} : i ∉ a ↔ ∃ (k : V), ∃ r < Exp.exp i, a = k * Exp.exp (i + 1) + r

@[instance_reducible]

def FFL.FirstOrder.Arithmetic.instEmptyCollection_foundation {V : Type u_1} [ORingStructure V] : EmptyCollection V

Equations

• FFL.FirstOrder.Arithmetic.instEmptyCollection_foundation = { emptyCollection := 0 }

theorem FFL.FirstOrder.Arithmetic.emptyset_def {V : Type u_1} [ORingStructure V] : ∅ = 0

@[simp]

theorem FFL.FirstOrder.Arithmetic.not_mem_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (i : V) : i ∉ ∅

@[simp]

theorem FFL.FirstOrder.Arithmetic.not_mem_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (i : V) : i ∉ 0

@[instance_reducible]

noncomputable def FFL.FirstOrder.Arithmetic.instSingleton_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Singleton V V

Equations

• FFL.FirstOrder.Arithmetic.instSingleton_foundation = { singleton := fun (a : V) => FFL.Exp.exp a }

theorem FFL.FirstOrder.Arithmetic.singleton_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : {a} = Exp.exp a

@[simp]

theorem FFL.FirstOrder.Arithmetic.singleton_injective {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) : {a} = {b} ↔ a = b

noncomputable def FFL.FirstOrder.Arithmetic.bitInsert {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (i a : V) : V

Equations

• FFL.FirstOrder.Arithmetic.bitInsert i a = if i ∈ a then a else a + FFL.Exp.exp i

noncomputable def FFL.FirstOrder.Arithmetic.bitRemove {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (i a : V) : V

Equations

• FFL.FirstOrder.Arithmetic.bitRemove i a = if i ∈ a then a - FFL.Exp.exp i else a

@[instance_reducible]

noncomputable def FFL.FirstOrder.Arithmetic.instInsert_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Insert V V

Equations

• FFL.FirstOrder.Arithmetic.instInsert_foundation = { insert := FFL.FirstOrder.Arithmetic.bitInsert }

theorem FFL.FirstOrder.Arithmetic.insert_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} : insert i a = bitInsert i a

theorem FFL.FirstOrder.Arithmetic.singleton_eq_insert {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (i : V) : {i} = insert i ∅

instance FFL.FirstOrder.Arithmetic.instLawfulSingleton_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : LawfulSingleton V V

@[simp]

theorem FFL.FirstOrder.Arithmetic.mem_bitInsert_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i j a : V} : i ∈ insert j a ↔ i = j ∨ i ∈ a

@[simp]

theorem FFL.FirstOrder.Arithmetic.mem_bitRemove_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i j a : V} : i ∈ bitRemove j a ↔ i ≠ j ∧ i ∈ a

@[simp]

theorem FFL.FirstOrder.Arithmetic.not_mem_bitRemove_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (i a : V) : i ∉ bitRemove i a

theorem FFL.FirstOrder.Arithmetic.insert_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (b i a : V) : b = insert i a ↔ i ∈ a ∧ b = a ∨ i ∉ a ∧ ∃ e ≤ b, e = Exp.exp i ∧ b = a + e

def FFL.FirstOrder.Arithmetic.insertDef : 𝚺₀.Semisentence 3

Equations

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

instance FFL.FirstOrder.Arithmetic.insert_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₂ insert via insertDef

instance FFL.FirstOrder.Arithmetic.insert_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₂ insert

instance FFL.FirstOrder.Arithmetic.insert_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (Γ : HierarchySymbol) : Γ-Function₂ insert

theorem FFL.FirstOrder.Arithmetic.insert_le_of_le_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i j a b : V} (hij : i ≤ j) (hab : a ≤ b) : insert i a ≤ b + Exp.exp j

theorem FFL.FirstOrder.Arithmetic.insert_absolute {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x s : ℕ) : ↑(insert x s) = insert ↑x ↑s

theorem FFL.FirstOrder.Arithmetic.one_eq_singleton {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 1 = {∅}

@[simp]

theorem FFL.FirstOrder.Arithmetic.mem_singleton_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i j : V} : i ∈ {j} ↔ i = j

theorem FFL.FirstOrder.Arithmetic.bitRemove_lt_of_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} (h : i ∈ a) : bitRemove i a < a

theorem FFL.FirstOrder.Arithmetic.pos_of_nonempty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} (h : i ∈ a) : 0 < a

@[simp]

theorem FFL.FirstOrder.Arithmetic.mem_insert {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (i a : V) : i ∈ insert i a

theorem FFL.FirstOrder.Arithmetic.insert_eq_self_of_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} (h : i ∈ a) : insert i a = a

theorem FFL.FirstOrder.Arithmetic.log_mem_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a : V} (h : 0 < a) : log a ∈ a

theorem FFL.FirstOrder.Arithmetic.le_log_of_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} (h : i ∈ a) : i ≤ log a

theorem FFL.FirstOrder.Arithmetic.succ_mem_iff_mem_div_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} : i + 1 ∈ a ↔ i ∈ a / 2

theorem FFL.FirstOrder.Arithmetic.lt_length_of_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} (h : i ∈ a) : i < ‖a‖

theorem FFL.FirstOrder.Arithmetic.lt_exp_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a i : V} : a < Exp.exp i ↔ ∀ j ∈ a, j < i

@[instance_reducible]

instance FFL.FirstOrder.Arithmetic.instHasSubset_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : HasSubset V

Equations

• FFL.FirstOrder.Arithmetic.instHasSubset_foundation = { Subset := fun (a b : V) => ∀ ⦃i : V⦄, i ∈ a → i ∈ b }

def FFL.FirstOrder.Arithmetic.bitSubsetDef : 𝚺₀.Semisentence 2

Equations

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

instance FFL.FirstOrder.Arithmetic.bitSubset_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Relation Subset via bitSubsetDef

instance FFL.FirstOrder.Arithmetic.bitSubset_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Relation Subset

@[simp]

instance FFL.FirstOrder.Arithmetic.bitSubset_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Relation Subset

theorem FFL.FirstOrder.Arithmetic.subset_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} : a ⊆ b ↔ ∀ x ∈ a, x ∈ b

@[simp]

theorem FFL.FirstOrder.Arithmetic.subset_refl {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : a ⊆ a

theorem FFL.FirstOrder.Arithmetic.subset_trans {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b c : V} (hab : a ⊆ b) (hbc : b ⊆ c) : a ⊆ c

theorem FFL.FirstOrder.Arithmetic.mem_exp_add_succ_sub_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (i j : V) : i ∈ Exp.exp (i + j + 1) - 1

noncomputable def FFL.FirstOrder.Arithmetic.under {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : V

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

Equations

• FFL.FirstOrder.Arithmetic.under a = FFL.Exp.exp a - 1

@[simp]

theorem FFL.FirstOrder.Arithmetic.le_under {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : a ≤ under a

@[simp]

theorem FFL.FirstOrder.Arithmetic.mem_under_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i j : V} : i ∈ under j ↔ i < j

@[simp]

theorem FFL.FirstOrder.Arithmetic.not_mem_under_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (i : V) : i ∉ under i

def FFL.FirstOrder.Arithmetic.underDef : 𝚺₀.Semisentence 2

Equations

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

instance FFL.FirstOrder.Arithmetic.under_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ under via underDef

instance FFL.FirstOrder.Arithmetic.under_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ under

instance FFL.FirstOrder.Arithmetic.under_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (Γ : HierarchySymbol) : Γ-Function₁ under

theorem FFL.FirstOrder.Arithmetic.eq_zero_of_subset_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a : V} : a ⊆ 0 → a = 0

theorem FFL.FirstOrder.Arithmetic.subset_div_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} : a ⊆ b → a / 2 ⊆ b / 2

theorem FFL.FirstOrder.Arithmetic.zero_mem_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a : V} : 0 ∉ a ↔ 2 ∣ a

@[simp]

theorem FFL.FirstOrder.Arithmetic.zero_not_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : 0 ∉ 2 * a

@[simp]

theorem FFL.FirstOrder.Arithmetic.zero_mem_double_add_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : 0 ∈ 2 * a + 1

@[simp]

theorem FFL.FirstOrder.Arithmetic.succ_mem_two_mul_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} : i + 1 ∈ 2 * a ↔ i ∈ a

@[simp]

theorem FFL.FirstOrder.Arithmetic.succ_mem_two_mul_succ_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} : i + 1 ∈ 2 * a + 1 ↔ i ∈ a

theorem FFL.FirstOrder.Arithmetic.le_of_subset {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} (h : a ⊆ b) : a ≤ b

theorem FFL.FirstOrder.Arithmetic.mem_ext {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} (h : ∀ (i : V), i ∈ a ↔ i ∈ b) : a = b

theorem FFL.FirstOrder.Arithmetic.mem_ext_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} : a = b ↔ ∀ (i : V), i ∈ a ↔ i ∈ b

theorem FFL.FirstOrder.Arithmetic.pos_iff_nonempty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {s : V} : 0 < s ↔ s ≠ ∅

theorem FFL.FirstOrder.Arithmetic.nonempty_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a : V} (h : 0 < a) : ∃ (i : V), i ∈ a

theorem FFL.FirstOrder.Arithmetic.eq_empty_or_nonempty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : a = ∅ ∨ ∃ (i : V), i ∈ a

theorem FFL.FirstOrder.Arithmetic.nonempty_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {s : V} : s ≠ ∅ ↔ ∃ (x : V), x ∈ s

theorem FFL.FirstOrder.Arithmetic.isempty_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {s : V} : s = ∅ ↔ ∀ (x : V), x ∉ s

@[simp]

theorem FFL.FirstOrder.Arithmetic.empty_subset {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : V) : ∅ ⊆ s

theorem FFL.FirstOrder.Arithmetic.lt_of_lt_log {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} (pos : 0 < b) (h : ∀ i ∈ a, i < log b) : a < b

@[simp]

theorem FFL.FirstOrder.Arithmetic.under_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i j : V} : under i = under j ↔ i = j

@[simp]

theorem FFL.FirstOrder.Arithmetic.under_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : under 0 = ∅

@[simp]

theorem FFL.FirstOrder.Arithmetic.under_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (i : V) : under (i + 1) = insert i (under i)

theorem FFL.FirstOrder.Arithmetic.insert_remove {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} (h : i ∈ a) : insert i (bitRemove i a) = a

theorem FFL.FirstOrder.Arithmetic.finset_comprehension_aux {V : Type u_1} [ORingStructure V] {m : ℕ} [Fact (1 ≤ m)] [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 𝚺 m] (Γ : Polarity) {P : V → Prop} (hP : { Γ := Γ.coe, rank := m }-Predicate P) (a : V) : ∃ s < Exp.exp a, ∀ i < a, i ∈ s ↔ P i

theorem FFL.FirstOrder.Arithmetic.finset_comprehension {V : Type u_1} [ORingStructure V] {m : ℕ} [Fact (1 ≤ m)] [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 𝚺 m] {Γ : SigmaPiDelta} {P : V → Prop} (hP : { Γ := Γ, rank := m }-Predicate P) (a : V) : ∃ s < Exp.exp a, ∀ i < a, i ∈ s ↔ P i

theorem FFL.FirstOrder.Arithmetic.finset_comprehension_exists_unique {V : Type u_1} [ORingStructure V] {m : ℕ} [Fact (1 ≤ m)] [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 𝚺 m] {Γ : SigmaPiDelta} {P : V → Prop} (hP : { Γ := Γ, rank := m }-Predicate P) (a : V) : ∃! s : V, s < Exp.exp a ∧ ∀ i < a, i ∈ s ↔ P i

instance FFL.FirstOrder.Arithmetic.instFactLeOfNat_foundation : Fact (1 ≤ 1)

theorem FFL.FirstOrder.Arithmetic.finset_comprehension₁ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : SigmaPiDelta} {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (a : V) : ∃ s < Exp.exp a, ∀ i < a, i ∈ s ↔ P i

theorem FFL.FirstOrder.Arithmetic.finset_comprehension₁! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : SigmaPiDelta} {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (a : V) : ∃! s : V, s < Exp.exp a ∧ ∀ i < a, i ∈ s ↔ P i

theorem FFL.FirstOrder.Arithmetic.finite_comprehension₁! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : 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