Bootstrapping theory $\mathsf{PA}^-$, $\mathsf{R_0}$ in $\mathsf{I}\Sigma_1$

theorem LO.FirstOrder.Arithmetic.lt_add_self_add_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (a b : V) : a < b + a + 1

theorem LO.FirstOrder.Arithmetic.lt_succ_iff_eq_or_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} : a < b + 1 ↔ a = b ∨ a < b

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiom (T : ArithmeticTheory) [𝗣𝗔⁻ ⪯ T] : 𝗘𝗤 ℒₒᵣ ⪯ T

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.term_add_assoc {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] (t₁ t₂ t₃ : Term V ℒₒᵣ) : Theory.internalize V T ⊢ Semiterm.equals (t₁ + (t₂ + t₃)) (t₁ + t₂ + t₃)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] (n m : V) : Theory.internalize V T ⊢ (typedNumeral n + typedNumeral m).equals (typedNumeral (n + m))

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] (n m : V) : Theory.internalize V T ⊢ (typedNumeral n * typedNumeral m).equals (typedNumeral (n * m))

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] {n m : V} : n = m → Theory.internalize V T ⊢ (typedNumeral n).equals (typedNumeral m)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] {n m : V} : n < m → Theory.internalize V T ⊢ (typedNumeral n).lessThan (typedNumeral m)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_ne {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] {n m : V} : n ≠ m → Theory.internalize V T ⊢ (typedNumeral n).notEquals (typedNumeral m)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.numeral_nlt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] {n m : V} : n ≥ m → Theory.internalize V T ⊢ (typedNumeral n).notLessThan (typedNumeral m)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.lt_iff_substItrDisj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] (t : Term V ℒₒᵣ) (m : V) : Theory.internalize V T ⊢ Semiterm.lessThan t (typedNumeral m) 🡘 Semiformula.substItrDisj ![t] ((Semiterm.bvar 1).equals (Semiterm.bvar 0)) m

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.ball_intro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] (φ : Semiformula V ℒₒᵣ 1) (n : V) (bs : ∀ i < n, Theory.internalize V T ⊢ Semiformula.subst ![typedNumeral i] φ) : Theory.internalize V T ⊢ Semiformula.ball (typedNumeral n) φ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.bexs_intro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] (φ : Semiformula V ℒₒᵣ 1) (n : V) {i : V} (hi : i < n) (b : Theory.internalize V T ⊢ Semiformula.subst ![typedNumeral i] φ) : Theory.internalize V T ⊢ Semiformula.bexs (typedNumeral n) φ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.ball_replace {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] (φ : Semiformula V ℒₒᵣ 1) (t u : Term V ℒₒᵣ) : Theory.internalize V T ⊢ Semiterm.equals t u 🡒 Semiformula.ball t φ 🡒 Semiformula.ball u φ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.bexs_replace {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗣𝗔⁻ ⪯ T] (φ : Semiformula V ℒₒᵣ 1) (t u : Term V ℒₒᵣ) : Theory.internalize V T ⊢ Semiterm.equals t u 🡒 Semiformula.bexs t φ 🡒 Semiformula.bexs u φ