Documentation

Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.EquationalTheory

Bootstrapping theory of equality #

source
@[simp]
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.eq_refl {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t : Term V ℒₒᵣ) :
Theory.internalize V T ⊢ Semiterm.equals t t
source
@[simp]
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.eq_symm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t u : Term V ℒₒᵣ) :
Theory.internalize V T ⊢ Semiterm.equals t u 🡒 Semiterm.equals u t
source
@[simp]
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.ne_symm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t u : Term V ℒₒᵣ) :
Theory.internalize V T ⊢ Semiterm.notEquals t u 🡒 Semiterm.notEquals u t
source
@[simp]
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.eq_uniform_trans {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₂ 🡒 Semiterm.equals t₂ t₃ 🡒 Semiterm.equals t₁ t₃
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.eq_comm_ctx {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {T : ArithmeticTheory} [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] {Γ : List (Semiformula V ℒₒᵣ 0)} {t u : Term V ℒₒᵣ} :
Γ ⊢[Theory.internalize V T] Semiterm.equals t u → Γ ⊢[Theory.internalize V T] Semiterm.equals u t
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.eq_trans {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₂ → Theory.internalize V T ⊢ Semiterm.equals t₂ t₃ → Theory.internalize V T ⊢ Semiterm.equals t₁ t₃
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.subst_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t₁ t₂ u₁ u₂ : Term V ℒₒᵣ) :
Theory.internalize V T ⊢ Semiterm.equals t₁ t₂ 🡒 Semiterm.equals u₁ u₂ 🡒 Semiterm.equals t₁ u₁ 🡒 Semiterm.equals t₂ u₂
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.subst_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t₁ t₂ u₁ u₂ : Term V ℒₒᵣ) :
Theory.internalize V T ⊢ Semiterm.equals t₁ t₂ 🡒 Semiterm.equals u₁ u₂ 🡒 Semiterm.lessThan t₁ u₁ 🡒 Semiterm.lessThan t₂ u₂
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.subst_ne {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t₁ t₂ u₁ u₂ : Term V ℒₒᵣ) :
Theory.internalize V T ⊢ Semiterm.equals t₁ t₂ 🡒 Semiterm.equals u₁ u₂ 🡒 Semiterm.notEquals t₁ u₁ 🡒 Semiterm.notEquals t₂ u₂
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.subst_nlt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t₁ t₂ u₁ u₂ : Term V ℒₒᵣ) :
Theory.internalize V T ⊢ Semiterm.equals t₁ t₂ 🡒 Semiterm.equals u₁ u₂ 🡒 Semiterm.notLessThan t₁ u₁ 🡒 Semiterm.notLessThan t₂ u₂
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.subst_add_eq_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t₁ t₂ u₁ u₂ : Term V ℒₒᵣ) :
Theory.internalize V T ⊢ Semiterm.equals t₁ t₂ 🡒 Semiterm.equals u₁ u₂ 🡒 Semiterm.equals (t₁ + u₁) (t₂ + u₂)
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.subst_mul_eq_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t₁ t₂ u₁ u₂ : Term V ℒₒᵣ) :
Theory.internalize V T ⊢ Semiterm.equals t₁ t₂ 🡒 Semiterm.equals u₁ u₂ 🡒 Semiterm.equals (t₁ * u₁) (t₂ * u₂)
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.vec2_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {v : V} (h : len v = 2) :
?[nth v 0, nth v 1] = v
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.term_replace_aux {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t : V) :
IsSemiterm ℒₒᵣ 1 t → Provable T (qqAll (qqAll (imp ℒₒᵣ (qqBvar 1 ^= qqBvar 0) (termSubst ℒₒᵣ ?[qqBvar 1] t ^= termSubst ℒₒᵣ ?[qqBvar 0] t))))
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.term_replace {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t : Semiterm V ℒₒᵣ 1) :
Theory.internalize V T ⊢ ∀¹ ∀¹ ((Semiterm.bvar 1).equals (Semiterm.bvar 0) 🡒 (Semiterm.subst ![Semiterm.bvar 1] t).equals (Semiterm.subst ![Semiterm.bvar 0] t))
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.term_replace' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t : Semiterm V ℒₒᵣ 1) (u₁ u₂ : Term V ℒₒᵣ) :
Theory.internalize V T ⊢ Semiterm.equals u₁ u₂ 🡒 (Semiterm.subst ![u₁] t).equals (Semiterm.subst ![u₂] t)
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.replace_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t u : Semiterm V ℒₒᵣ 1) :
Theory.internalize V T ⊢ ∀¹ ∀¹ ((Semiterm.bvar 1).equals (Semiterm.bvar 0) 🡒 Semiformula.subst ![Semiterm.bvar 1] (t.equals u) 🡒 Semiformula.subst ![Semiterm.bvar 0] (t.equals u))
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.replace_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t u : Semiterm V ℒₒᵣ 1) :
Theory.internalize V T ⊢ ∀¹ ∀¹ ((Semiterm.bvar 1).equals (Semiterm.bvar 0) 🡒 Semiformula.subst ![Semiterm.bvar 1] (t.lessThan u) 🡒 Semiformula.subst ![Semiterm.bvar 0] (t.lessThan u))
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.replace_ne {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t u : Semiterm V ℒₒᵣ 1) :
Theory.internalize V T ⊢ ∀¹ ∀¹ ((Semiterm.bvar 1).equals (Semiterm.bvar 0) 🡒 Semiformula.subst ![Semiterm.bvar 1] (t.notEquals u) 🡒 Semiformula.subst ![Semiterm.bvar 0] (t.notEquals u))
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.replace_nlt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (t u : Semiterm V ℒₒᵣ 1) :
Theory.internalize V T ⊢ ∀¹ ∀¹ ((Semiterm.bvar 1).equals (Semiterm.bvar 0) 🡒 Semiformula.subst ![Semiterm.bvar 1] (t.notLessThan u) 🡒 Semiformula.subst ![Semiterm.bvar 0] (t.notLessThan u))
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.replace_aux {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (φ : V) :
IsSemiformula ℒₒᵣ 1 φ → Provable T (qqAll (qqAll (imp ℒₒᵣ (qqBvar 1 ^= qqBvar 0) (imp ℒₒᵣ (subst ℒₒᵣ ?[qqBvar 1] φ) (subst ℒₒᵣ ?[qqBvar 0] φ)))))
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.replace' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (φ : Semiformula V ℒₒᵣ 1) :
Theory.internalize V T ⊢ ∀¹ ∀¹ ((Semiterm.bvar 1).equals (Semiterm.bvar 0) 🡒 Semiformula.subst ![Semiterm.bvar 1] φ 🡒 Semiformula.subst ![Semiterm.bvar 0] φ)
source
theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.replace {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (T : ArithmeticTheory) [Theory.Δ₁ T] [𝗘𝗤 ℒₒᵣ ⪯ T] (φ : Semiformula V ℒₒᵣ 1) (u₁ u₂ : Term V ℒₒᵣ) :
Theory.internalize V T ⊢ Semiterm.equals u₁ u₂ 🡒 Semiformula.subst ![u₁] φ 🡒 Semiformula.subst ![u₂] φ