add(FirstOrder/Arith): EA

Logic.lean

@@ -60,7 +60,7 @@ import Logic.FirstOrder.Arith.StrictHierarchy
 import Logic.FirstOrder.Arith.Theory
 import Logic.FirstOrder.Arith.Model
 import Logic.FirstOrder.Arith.Nonstandard
-import Logic.FirstOrder.Arith.PAminus
+import Logic.FirstOrder.Arith.EA.Basic
 
 import Logic.FirstOrder.Incompleteness.FirstIncompleteness
 import Logic.FirstOrder.Incompleteness.SelfReference

Logic/FirstOrder/Arith/Basic.lean

@@ -56,6 +56,65 @@ def oringEmb : ℒₒᵣ →ᵥ L where
 
 end Language
 
+section
+
+variable {L : Language} [L.ORing]
+
+namespace Semiterm
+
+instance : Coe (Semiterm ℒₒᵣ ξ n) (Semiterm L ξ n) := ⟨lMap Language.oringEmb⟩
+
+@[simp] lemma oringEmb_zero :
+    Semiterm.lMap (Language.oringEmb : ℒₒᵣ →ᵥ L) (Operator.Zero.zero.const : Semiterm ℒₒᵣ ξ n) = Operator.Zero.zero.const := by
+  simp [Operator.const, lMap_func, Operator.operator, Operator.Zero.term_eq, Matrix.empty_eq]
+
+@[simp] lemma oringEmb_one :
+    Semiterm.lMap (Language.oringEmb : ℒₒᵣ →ᵥ L) (Operator.One.one.const : Semiterm ℒₒᵣ ξ n) = Operator.One.one.const := by
+  simp [Operator.const, lMap_func, Operator.operator, Operator.One.term_eq, Matrix.empty_eq]
+
+@[simp] lemma oringEmb_add (v : Fin 2 → Semiterm ℒₒᵣ ξ n) :
+    Semiterm.lMap (Language.oringEmb : ℒₒᵣ →ᵥ L) (Operator.Add.add.operator v) = Operator.Add.add.operator ![(v 0 : Semiterm L ξ n), (v 1 : Semiterm L ξ n)] := by
+  simp [lMap_func, Rew.func, Operator.operator, Operator.Add.term_eq, Matrix.empty_eq]
+  funext i; cases i using Fin.cases <;> simp [Fin.eq_zero]
+
+@[simp] lemma oringEmb_mul (v : Fin 2 → Semiterm ℒₒᵣ ξ n) :
+    Semiterm.lMap (Language.oringEmb : ℒₒᵣ →ᵥ L) (Operator.Mul.mul.operator v) = Operator.Mul.mul.operator ![(v 0 : Semiterm L ξ n), (v 1 : Semiterm L ξ n)] := by
+  simp [lMap_func, Rew.func, Operator.operator, Operator.Mul.term_eq, Matrix.empty_eq]
+  funext i; cases i using Fin.cases <;> simp [Fin.eq_zero]
+
+@[simp] lemma oringEmb_numeral (z : ℕ) :
+    Semiterm.lMap (Language.oringEmb : ℒₒᵣ →ᵥ L) ((Operator.numeral ℒₒᵣ z).const : Semiterm ℒₒᵣ ξ n) = (Operator.numeral L z).const := by
+  match z with
+  | 0     => exact oringEmb_zero
+  | 1     => exact oringEmb_one
+  | z + 2 =>
+    simp [Operator.numeral_add_two]
+    congr; funext i; cases i using Fin.cases
+    · exact oringEmb_numeral (z + 1)
+    · simp
+
+end Semiterm
+
+namespace Semiformula
+
+instance : Coe (Semiformula ℒₒᵣ ξ n) (Semiformula L ξ n) := ⟨Semiformula.lMap Language.oringEmb⟩
+
+instance : Coe (Theory ℒₒᵣ) (Theory L) := ⟨(Semiformula.lMap Language.oringEmb '' ·)⟩
+
+@[simp] lemma oringEmb_eq (v : Fin 2 → Semiterm ℒₒᵣ ξ n) :
+    Semiformula.lMap (Language.oringEmb : ℒₒᵣ →ᵥ L) (op(=).operator v) = op(=).operator ![(v 0 : Semiterm L ξ n), (v 1 : Semiterm L ξ n)] := by
+  simp [lMap_rel, Rew.rel, Operator.operator, Operator.Eq.sentence_eq]
+  funext i; cases i using Fin.cases <;> simp [Fin.eq_zero]
+
+@[simp] lemma oringEmb_lt (v : Fin 2 → Semiterm ℒₒᵣ ξ n) :
+    Semiformula.lMap (Language.oringEmb : ℒₒᵣ →ᵥ L) (op(<).operator v) = op(<).operator ![(v 0 : Semiterm L ξ n), (v 1 : Semiterm L ξ n)] := by
+  simp [lMap_rel, Rew.rel, Operator.operator, Operator.LT.sentence_eq]
+  funext i; cases i using Fin.cases <;> simp [Fin.eq_zero]
+
+end Semiformula
+
+end
+
 open Semiterm Semiformula
 
 abbrev Polynomial (n : ℕ) : Type := Semiterm ℒₒᵣ Empty n

Logic/FirstOrder/Arith/EA/Basic.lean

@@ -0,0 +1,158 @@
+import Logic.FirstOrder.Arith.Model
+
+namespace LO.FirstOrder
+
+namespace Arith
+
+variable {L : Language} [L.ORing] (T : Theory L) [𝐄𝐪 ≾ T] [L.Exp]
+
+instance : Language.ORing ℒₒᵣ(exp) := Language.ORing.mk
+
+lemma consequence_of_exp (σ : Sentence L)
+  (H : ∀ (M : Type u)
+         [Zero M] [One M] [Add M] [Mul M] [Exp M] [LT M]
+         [Structure L M]
+         [Structure.ORing L M]
+         [Structure.Exp L M]
+         [Theory.Mod M T],
+         M ⊧ₘ σ) :
+    T ⊨ σ := consequence_iff_eq.mpr fun M _ _ _ hT =>
+  letI : Theory.Mod (Structure.Model L M) T :=
+    ⟨((Structure.ElementaryEquiv.modelsTheory (Structure.Model.elementaryEquiv L M)).mp hT)⟩
+  (Structure.ElementaryEquiv.models (Structure.Model.elementaryEquiv L M)).mpr
+    (H (Structure.Model L M))
+
+namespace Theory
+
+variable (L)
+
+notation "𝐈open(exp)" => IOpen ℒₒᵣ(exp)
+
+notation "𝐈𝚫₀(exp)" => ISigma ℒₒᵣ(exp) 0
+
+inductive Exponential : Theory L
+  | zero : Exponential “exp 0 = 1”
+  | succ : Exponential “∀ exp (#0 + 1) = 2 * exp #0”
+
+notation "𝐄𝐗𝐏" => Exponential ℒₒᵣ(exp)
+
+abbrev ElementaryArithmetic : Theory L := Semiformula.lMap Language.oringEmb '' 𝐏𝐀⁻ + Exponential L + ISigma L 0
+
+notation "𝐄𝐀" => ElementaryArithmetic ℒₒᵣ(exp)
+
+end Theory
+
+section model
+
+variable (M : Type*) [Zero M] [One M] [Add M] [Exp M] [Mul M] [LT M]
+
+instance standardModelExp : Structure ℒₒᵣ(exp) M where
+  func := fun _ f =>
+    match f with
+    | Language.ORingExp.Func.zero => fun _ => 0
+    | Language.ORingExp.Func.one  => fun _ => 1
+    | Language.ORingExp.Func.exp  => fun v => Exp.exp (v 0)
+    | Language.ORingExp.Func.add  => fun v => v 0 + v 1
+    | Language.ORingExp.Func.mul  => fun v => v 0 * v 1
+  rel := fun _ r =>
+    match r with
+    | Language.ORingExp.Rel.eq => fun v => v 0 = v 1
+    | Language.ORingExp.Rel.lt => fun v => v 0 < v 1
+
+instance : Structure.Eq ℒₒᵣ(exp) M :=
+  ⟨by intro a b; simp[standardModelExp, Semiformula.Operator.val, Semiformula.Operator.Eq.sentence_eq, Semiformula.eval_rel]⟩
+
+instance : Structure.Zero ℒₒᵣ(exp) M := ⟨rfl⟩
+
+instance : Structure.One ℒₒᵣ(exp) M := ⟨rfl⟩
+
+instance : Structure.Add ℒₒᵣ(exp) M := ⟨fun _ _ => rfl⟩
+
+instance : Structure.Mul ℒₒᵣ(exp) M := ⟨fun _ _ => rfl⟩
+
+instance : Structure.Exp ℒₒᵣ(exp) M := ⟨fun _ => rfl⟩
+
+instance : Structure.Eq ℒₒᵣ(exp) M := ⟨fun _ _ => iff_of_eq rfl⟩
+
+instance : Structure.LT ℒₒᵣ(exp) M := ⟨fun _ _ => iff_of_eq rfl⟩
+
+lemma standardModelExp_unique' (s : Structure ℒₒᵣ(exp) M)
+    (hZero : Structure.Zero ℒₒᵣ(exp) M) (hOne : Structure.One ℒₒᵣ(exp) M)
+    (hAdd : Structure.Add ℒₒᵣ(exp) M) (hMul : Structure.Mul ℒₒᵣ(exp) M) (hExp : Structure.Exp ℒₒᵣ(exp) M)
+    (hEq : Structure.Eq ℒₒᵣ(exp) M) (hLT : Structure.LT ℒₒᵣ(exp) M) : s = standardModelExp M := Structure.ext _ _
+  (funext₃ fun k f _ =>
+    match k, f with
+    | _, Language.Zero.zero => by simp[Matrix.empty_eq]
+    | _, Language.One.one   => by simp[Matrix.empty_eq]
+    | _, Language.Add.add   => by simp
+    | _, Language.Mul.mul   => by simp
+    | _, Language.Exp.exp   => by simp)
+  (funext₃ fun k r _ =>
+    match k, r with
+    | _, Language.Eq.eq => by simp
+    | _, Language.LT.lt => by simp)
+
+lemma standardModelExp_unique (s : Structure ℒₒᵣ(exp) M)
+    [hZero : Structure.Zero ℒₒᵣ(exp) M] [hOne : Structure.One ℒₒᵣ(exp) M]
+    [hAdd : Structure.Add ℒₒᵣ(exp) M] [hMul : Structure.Mul ℒₒᵣ(exp) M] [hExp : Structure.Exp ℒₒᵣ(exp) M]
+    [hEq : Structure.Eq ℒₒᵣ(exp) M] [hLT : Structure.LT ℒₒᵣ(exp) M] : s = standardModelExp M :=
+  standardModelExp_unique' M s hZero hOne hAdd hMul hExp hEq hLT
+
+namespace Standard
+
+lemma modelsTheoryExponential : ℕ ⊧ₘ* 𝐄𝐗𝐏 := by
+  intro σ h
+  rcases h <;> simp[models_def, Structure.Exp.exp, Nat.exp_succ]
+
+lemma modelsSuccInd_exp (p : Semiformula ℒₒᵣ(exp) ℕ 1) : ℕ ⊧ₘ (∀ᶠ* succInd p) := by
+  simp [Empty.eq_elim, succInd, models_iff, Matrix.constant_eq_singleton, Matrix.comp_vecCons',
+    Semiformula.eval_substs, Semiformula.eval_rew_q Rew.toS, Function.comp]
+  intro e hzero hsucc x; induction' x with x ih
+  · exact hzero
+  · exact hsucc x ih
+
+lemma modelsTheoryElementaryArithmetic : ℕ ⊧ₘ* 𝐄𝐀 := by
+  simp [Theory.ElementaryArithmetic, Theory.add_def, Theory.ISigma, Theory.IndScheme]
+  exact ⟨⟨by intro σ hσ; simpa [models_iff] using modelsTheoryPAminus hσ, modelsTheoryExponential⟩,
+    by rintro σ p _ rfl; exact modelsSuccInd_exp p⟩
+
+end Standard
+
+end model
+
+noncomputable section
+
+variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [Exp M] [LT M] [𝐄𝐀.Mod M]
+
+open Language
+
+namespace Model
+
+instance : 𝐏𝐀⁻.Mod M :=
+  haveI : Theory.Mod M (Semiformula.lMap Language.oringEmb '' 𝐏𝐀⁻ : Theory ℒₒᵣ(exp)) :=
+    Theory.Mod.of_add_left_left M (Semiformula.lMap Language.oringEmb '' 𝐏𝐀⁻) 𝐄𝐗𝐏 𝐈𝚫₀(exp)
+  ⟨by intro σ hσ;
+      simpa [models_iff] using
+        @Theory.Mod.models ℒₒᵣ(exp) M _ _ _ this _ (Set.mem_image_of_mem (Semiformula.lMap Language.oringEmb) hσ)⟩
+
+instance : 𝐄𝐗𝐏.Mod M := Theory.Mod.of_add_left_right M (Semiformula.lMap Language.oringEmb '' 𝐏𝐀⁻) 𝐄𝐗𝐏 𝐈𝚫₀(exp)
+
+instance : 𝐈𝚫₀(exp).Mod M := Theory.Mod.of_add_right M (Semiformula.lMap Language.oringEmb '' 𝐏𝐀⁻ + 𝐄𝐗𝐏) 𝐈𝚫₀(exp)
+
+lemma ISigma₀_subset_IDelta₀Exp : (𝐈𝚺₀ : Theory ℒₒᵣ(exp)) ⊆ 𝐈𝚫₀(exp) :=
+  Theory.coe_IHierarchy_subset_IHierarchy
+
+instance : 𝐈𝚺₀.Mod M := ⟨by
+  intro σ hσ
+  have : (𝐈𝚺₀ : Theory ℒₒᵣ(exp)) ⊆ 𝐈𝚫₀(exp) := Theory.coe_IHierarchy_subset_IHierarchy
+  have : M ⊧ₘ (σ : Sentence ℒₒᵣ(exp)) :=
+    Theory.Mod.models M (show (σ : Sentence ℒₒᵣ(exp)) ∈ 𝐈𝚫₀(exp) from this (Set.mem_image_of_mem _ hσ))
+  simpa [models_iff] using this⟩
+
+end Model
+
+end
+
+end Arith
+
+end LO.FirstOrder

Logic/FirstOrder/Arith/Hierarchy.lean

@@ -295,6 +295,16 @@ lemma of_open {p : Semiformula L μ n} : p.Open → Hierarchy Γ s p := by
   case hand ihp ihq => intro hp hq; exact ⟨ihp hp, ihq hq⟩
   case hor ihp ihq => intro hp hq; exact ⟨ihp hp, ihq hq⟩
 
+variable {L : Language} [L.ORing]
+
+lemma oringEmb {p : Semiformula ℒₒᵣ μ n} : Hierarchy Γ s p → Hierarchy Γ s (Semiformula.lMap (Language.oringEmb : ℒₒᵣ →ᵥ L) p) := by
+  intro h; induction h <;> try simp [*, Semiformula.lMap_rel, Semiformula.lMap_nrel]
+  case sigma ih => exact ih.accum _
+  case pi ih => exact ih.accum _
+  case dummy_pi ih => exact ih.dummy_pi
+  case dummy_sigma ih => exact ih.dummy_sigma
+
+
 end Hierarchy
 
 section

Logic/FirstOrder/Arith/Model.lean

@@ -141,7 +141,7 @@ variable {μ : Type v} (e : Fin n → ℕ) (ε : μ → ℕ)
 
 lemma modelsTheoryPAminus : ℕ ⊧ₘ* 𝐏𝐀⁻ := by
   intro σ h
-  rcases h <;> simp[models_def, ←le_iff_eq_or_lt]
+  rcases h <;> simp [models_def, ←le_iff_eq_or_lt]
   case addAssoc => intro l m n; exact add_assoc l m n
   case addComm  => intro m n; exact add_comm m n
   case mulAssoc => intro l m n; exact mul_assoc l m n

Logic/FirstOrder/Arith/Nonstandard.lean

@@ -82,7 +82,7 @@ lemma trueArith : ℕ⋆ ⊧ₘ* 𝐓𝐀 := by
 
 instance : Theory.Mod ℕ⋆ 𝐓𝐀 := ⟨trueArith⟩
 
-instance : Theory.Mod ℕ⋆ (Theory.PAminus ℒₒᵣ) :=
+instance : Theory.Mod ℕ⋆ 𝐏𝐀⁻ :=
   Theory.Mod.of_ss (T₁ := 𝐓𝐀) _ (Structure.subset_of_models.mpr $ Arith.Standard.modelsTheoryPAminus)
 
 lemma star_unbounded (n : ℕ) : n < ⋆ := by

Logic/FirstOrder/Arith/PAminus.lean

@@ -23,55 +23,55 @@ instance : LE M := ⟨fun x y => x = y ∨ x < y⟩
 lemma le_def {x y : M} : x ≤ y ↔ x = y ∨ x < y := iff_of_eq rfl
 
 protected lemma add_zero : ∀ x : M, x + 0 = x := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.addZero oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.addZero
 
 protected lemma add_assoc : ∀ x y z : M, (x + y) + z = x + (y + z) := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.addAssoc oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.addAssoc
 
 protected lemma add_comm : ∀ x y : M, x + y = y + x := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.addComm oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.addComm
 
 lemma add_eq_of_lt : ∀ x y : M, x < y → ∃ z, x + z = y := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.addEqOfLt oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.addEqOfLt
 
 @[simp] lemma zero_le : ∀ x : M, 0 ≤ x := by
-  simpa[models_iff, Structure.le_iff_of_eq_of_lt] using Theory.Mod.models M (@Theory.PAminus.zeroLe oRing _)
+  simpa[models_iff, Structure.le_iff_of_eq_of_lt] using Theory.Mod.models M Theory.PAminus.zeroLe
 
 lemma zero_lt_one : (0 : M) < 1 := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.zeroLtOne oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.zeroLtOne
 
 lemma one_le_of_zero_lt : ∀ x : M, 0 < x → 1 ≤ x := by
-  simpa[models_iff, Structure.le_iff_of_eq_of_lt] using Theory.Mod.models M (@Theory.PAminus.oneLeOfZeroLt oRing _)
+  simpa[models_iff, Structure.le_iff_of_eq_of_lt] using Theory.Mod.models M Theory.PAminus.oneLeOfZeroLt
 
 lemma add_lt_add : ∀ x y z : M, x < y → x + z < y + z := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.addLtAdd oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.addLtAdd
 
 protected lemma mul_zero : ∀ x : M, x * 0 = 0 := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.mulZero oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.mulZero
 
 protected lemma mul_one : ∀ x : M, x * 1 = x := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.mulOne oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.mulOne
 
 protected lemma mul_assoc : ∀ x y z : M, (x * y) * z = x * (y * z) := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.mulAssoc oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.mulAssoc
 
 protected lemma mul_comm : ∀ x y : M, x * y = y * x := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.mulComm oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.mulComm
 
 lemma mul_lt_mul : ∀ x y z : M, x < y → 0 < z → x * z < y * z := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.mulLtMul oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.mulLtMul
 
 lemma distr : ∀ x y z : M, x * (y + z) = x * y + x * z := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.distr oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.distr
 
 lemma lt_irrefl : ∀ x : M, ¬x < x := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.ltIrrefl oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.ltIrrefl
 
 lemma lt_trans : ∀ x y z : M, x < y → y < z → x < z := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.ltTrans oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.ltTrans
 
 lemma lt_tri : ∀ x y : M, x < y ∨ x = y ∨ y < x := by
-  simpa[models_iff] using Theory.Mod.models M (@Theory.PAminus.ltTri oRing _)
+  simpa[models_iff] using Theory.Mod.models M Theory.PAminus.ltTri
 
 instance : AddCommMonoid M where
   add_assoc := Model.add_assoc