Documentation

LeanPool.PointwiseComposition.Foundation.FirstOrder.Arithmetic.Bootstrapping.DerivabilityCondition.EquationalTheory

Supporting results for pointwise provable equality.

Bootstrapping theory of equality #

source
@[simp]
theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.vec2_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {v : V} (h : len v = 2) :
?[nth v 0, nth v 1] = v
source
theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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₂] φ