Supporting results for pointwise provable equality.

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

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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiom (T : ArithmeticTheory) [𝐏𝐀⁻ ≼ T] : 𝐄𝐐 ℒₒᵣ ≼ T

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 φ