noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substNumeral {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (φ x : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substNumeral φ x = LO.FirstOrder.Arithmetic.Bootstrapping.subst ℒₒᵣ ?[LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral x] φ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substNumeral_app_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (σ π : ArithmeticSemisentence 1) : substNumeral ⌜σ⌝ ⌜π⌝ = ⌜σ/[⌜π⌝]⌝

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substNumerals {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {k : ℕ} (φ : V) (v : Fin k → V) : V

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substNumerals_app_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {k : ℕ} (σ : ArithmeticSemisentence k) (v : Fin k → ℕ) : (substNumerals ⌜σ⌝ fun (x : Fin k) => ↑(v x)) = ⌜(Rewriting.app (Rew.subst fun (i : Fin k) => ↑(v i))) σ⌝

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substNumerals_app_quote_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {k : ℕ} (σ : ArithmeticSemisentence k) (π : Fin k → ArithmeticSemisentence k) : (substNumerals ⌜σ⌝ fun (i : Fin k) => ⌜π i⌝) = ⌜(Rewriting.app (Rew.subst fun (i : Fin k) => ⌜π i⌝)) σ⌝

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substNumeralParams {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k : ℕ) (φ x : V) : V

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substNumeralParams_app_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {k : ℕ} (σ τ : ArithmeticSemisentence (k + 1)) : substNumeralParams k ⌜σ⌝ ⌜τ⌝ = ⌜(Rewriting.app (Rew.subst (⌜τ⌝ :> fun (i : Fin k) => FirstOrder.Semiterm.bvar i))) σ⌝

@[irreducible]

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.ssnum : 𝚺₁.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substNumeral.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₂ substNumeral via ssnum

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substNumeral.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₂ substNumeral

@[irreducible]

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.ssnums {k : ℕ} : 𝚺₁.Semisentence (k + 2)

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substNumerals.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {k : ℕ} : HierarchySymbol.DefinedFunction (fun (v : Fin (k + 1) → V) => substNumerals (v 0) fun (x : Fin k) => v x.succ) ssnums

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.ssnumParams (k : ℕ) : 𝚺₁.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.ssnumParams.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {k : ℕ} : 𝚺₁-Function₂ substNumeralParams k via ssnumParams k

noncomputable def LO.FirstOrder.Arithmetic.diag (θ : ArithmeticSemisentence 1) : ArithmeticSemisentence 1

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.fixedpoint (θ : ArithmeticSemisentence 1) : ArithmeticSentence

Equations

• LO.FirstOrder.Arithmetic.fixedpoint θ = (LO.FirstOrder.Arithmetic.diag θ)/[⌜LO.FirstOrder.Arithmetic.diag θ⌝]

theorem LO.FirstOrder.Arithmetic.diagonal {T : ArithmeticTheory} [𝗜𝚺₁ ⪯ T] (θ : ArithmeticSemisentence 1) : T ⊢ fixedpoint θ 🡘 θ/[⌜fixedpoint θ⌝]

noncomputable def LO.FirstOrder.Arithmetic.multidiag {k : ℕ} (θ : ArithmeticSemisentence k) : ArithmeticSemisentence k

$\mathrm{diag}_i(\vec{x}) := (\forall \vec{y})\left[ \left(\bigwedge_j \mathrm{ssnums}(y_j, x_j, \vec{x})\right) \to \theta_i(\vec{y}) \right]$

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.multifixedpoint {k : ℕ} (θ : Fin k → ArithmeticSemisentence k) (i : Fin k) : ArithmeticSentence

Equations

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

theorem LO.FirstOrder.Arithmetic.multidiagonal {T : ArithmeticTheory} [𝗜𝚺₁ ⪯ T] {k : ℕ} {i : Fin k} (θ : Fin k → ArithmeticSemisentence k) : T ⊢ multifixedpoint θ i 🡘 (Rewriting.app (Rew.subst fun (j : Fin k) => ⌜multifixedpoint θ j⌝)) (θ i)

noncomputable def LO.FirstOrder.Arithmetic.exclusiveMultifixedpoint {k : ℕ} (θ : Fin k → ArithmeticSemisentence k) (i : Fin k) : ArithmeticSentence

Equations

• LO.FirstOrder.Arithmetic.exclusiveMultifixedpoint θ i = LO.FirstOrder.Arithmetic.multifixedpoint (fun (j : Fin k) => LO.FirstOrder.Semiformula.padding (θ j) ↑j) i

@[simp]

theorem LO.FirstOrder.Arithmetic.exclusiveMultifixedpoint_inj_iff {k : ℕ} {i j : Fin k} (θ : Fin k → ArithmeticSemisentence k) : exclusiveMultifixedpoint θ i = exclusiveMultifixedpoint θ j ↔ i = j

theorem LO.FirstOrder.Arithmetic.exclusiveMultidiagonal {T : ArithmeticTheory} [𝗜𝚺₁ ⪯ T] {k : ℕ} {i : Fin k} (θ : Fin k → ArithmeticSemisentence k) : T ⊢ exclusiveMultifixedpoint θ i 🡘 (Rewriting.app (Rew.subst fun (j : Fin k) => ⌜exclusiveMultifixedpoint θ j⌝)) (θ i)

theorem LO.FirstOrder.Arithmetic.multifixedpoint_pi {k m : ℕ} {i : Fin k} {θ : Fin k → ArithmeticSemisentence k} (h : ∀ (i : Fin k), Hierarchy 𝚷 (m + 1) (θ i)) : Hierarchy 𝚷 (m + 1) (multifixedpoint θ i)

theorem LO.FirstOrder.Arithmetic.exclusiveMultifixedpoint_pi {k m : ℕ} {i : Fin k} {θ : Fin k → ArithmeticSemisentence k} (h : ∀ (i : Fin k), Hierarchy 𝚷 (m + 1) (θ i)) : Hierarchy 𝚷 (m + 1) (exclusiveMultifixedpoint θ i)

noncomputable def LO.FirstOrder.Arithmetic.parameterizedDiag {k : ℕ} (θ : ArithmeticSemisentence (k + 1)) : ArithmeticSemisentence (k + 1)

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.parameterizedFixedpoint {k : ℕ} (θ : ArithmeticSemisentence (k + 1)) : ArithmeticSemisentence k

Equations

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

theorem LO.FirstOrder.Arithmetic.parameterized_diagonal {T : ArithmeticTheory} [𝗜𝚺₁ ⪯ T] {k : ℕ} (θ : ArithmeticSemisentence (k + 1)) : T ⊢ ∀¹* (parameterizedFixedpoint θ 🡘 θ ⇜ (⌜parameterizedFixedpoint θ⌝ :> fun (x : Fin k) => Semiterm.bvar (BinderNotation.finSuccItr x 0)))

theorem LO.FirstOrder.Arithmetic.parameterized_diagonal₁ {T : ArithmeticTheory} [𝗜𝚺₁ ⪯ T] (θ : ArithmeticSemisentence 2) : T ⊢ ∀¹ (parameterizedFixedpoint θ 🡘 θ/[⌜parameterizedFixedpoint θ⌝, Semiterm.bvar 0])