Supporting results for pointwise provable equality.

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.substNumeral {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (φ x : V) : V

The subst Numeral construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.substNumerals {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {k : ℕ} (φ : V) (v : Fin k → V) : V

The subst Numerals construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.substNumeralParams {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (k : ℕ) (φ x : V) : V

The subst Numeral Params construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.ssnum : Σ₁.Semisentence 3

The ssnum construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.substNumeral.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ substNumeral via ssnum

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.substNumeral.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ substNumeral

@[irreducible]

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.ssnums {k : ℕ} : Σ₁.Semisentence (k + 2)

The ssnums construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.ssnumParams (k : ℕ) : Σ₁.Semisentence 3

The ssnum Params construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.ssnumParams.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {k : ℕ} : Σ₁-Function₂ substNumeralParams k via ssnumParams k

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

The diag construction in FFL.FirstOrder.Arithmetic.

Equations

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

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

The fixedpoint construction in FFL.FirstOrder.Arithmetic.

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.diagonal {T : ArithmeticTheory} [𝐈Σ₁ ≼ T] (θ : ArithmeticSemisentence 1) : T ⊢ fixedpoint θ ⇔ₗ θ/[⌜fixedpoint θ⌝]

noncomputable def PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.multifixedpoint {k : ℕ} (θ : Fin k → ArithmeticSemisentence k) (i : Fin k) : ArithmeticSentence

The multifixedpoint construction in FFL.FirstOrder.Arithmetic.

Equations

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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.exclusiveMultifixedpoint {k : ℕ} (θ : Fin k → ArithmeticSemisentence k) (i : Fin k) : ArithmeticSentence

The exclusive Multifixedpoint construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[simp]

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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.parameterizedDiag {k : ℕ} (θ : ArithmeticSemisentence (k + 1)) : ArithmeticSemisentence (k + 1)

The parameterized Diag construction in FFL.FirstOrder.Arithmetic.

Equations

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

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

The parameterized Fixedpoint construction in FFL.FirstOrder.Arithmetic.

Equations

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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.parameterized_diagonal₁ {T : ArithmeticTheory} [𝐈Σ₁ ≼ T] (θ : ArithmeticSemisentence 2) : T ⊢ ∀¹ (parameterizedFixedpoint θ ⇔ₗ θ/[⌜parameterizedFixedpoint θ⌝, Semiterm.bvar 0])