remove LO.Semantics.Mod

Logic/FirstOrder/Arith/Basic.lean

@@ -159,13 +159,12 @@ lemma consequence_of (σ : Sentence L)
          [Zero M] [One M] [Add M] [Mul M] [LT M]
          [Structure L M]
          [Structure.ORing L M]
-         [Theory.Mod M T],
+         [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))
+  letI : 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))
 
 end Arith
 

Logic/FirstOrder/Arith/EA/Basic.lean

@@ -111,7 +111,7 @@ lemma modelsSuccInd_exp (p : Semiformula ℒₒᵣ(exp) ℕ 1) : ℕ ⊧ₘ (∀
 
 lemma modelsTheoryElementaryArithmetic : ℕ ⊧ₘ* 𝐄𝐀 := by
   simp [Theory.elementaryArithmetic, Theory.indScheme]
-  exact ⟨⟨by intro σ hσ; simpa [models_iff] using modelsTheoryPeanoMinus hσ, modelsTheoryExponential⟩,
+  exact ⟨⟨by intro σ hσ; simpa [models_iff] using models_peanoMinus hσ, modelsTheoryExponential⟩,
     by rintro σ p _ rfl; exact modelsSuccInd_exp p⟩
 
 end Standard

Logic/FirstOrder/Arith/Model.lean

@@ -133,19 +133,17 @@ variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [s : Structure L M]
   · simp [Theory.lMap]
     intro H p hp; exact eval_lMap_oringEmb.mpr (H hp)
 
-lemma mod_lMap_oringEmb (T : Theory ℒₒᵣ) :
-    (T.lMap oringEmb : Theory L).Mod M ↔ T.Mod M := by simp [Theory.Mod.iff]
+instance [M ⊧ₘ* 𝐈open] : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ Semiformula.Open)
 
-instance [(𝐈open).Mod M] : 𝐏𝐀⁻.Mod M := Theory.Mod.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ Semiformula.Open)
+instance [M ⊧ₘ* 𝐈open] : M ⊧ₘ* Theory.indScheme ℒₒᵣ Semiformula.Open :=
+  ModelsTheory.of_add_right M 𝐏𝐀⁻ (Theory.indScheme _ Semiformula.Open)
 
-instance [(𝐈open).Mod M] : (Theory.indScheme (L := ℒₒᵣ) Semiformula.Open).Mod M := Theory.Mod.of_add_right M 𝐏𝐀⁻ (Theory.indScheme _ Semiformula.Open)
+def mod_peanoMinus_of_mod_indH [M ⊧ₘ* 𝐈𝐍𝐃 Γ n] : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ (Arith.Hierarchy Γ n))
 
-def mod_peanoMinus_of_mod_indH [(𝐈𝐍𝐃 Γ ν).Mod M] : 𝐏𝐀⁻.Mod M := Theory.Mod.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ (Arith.Hierarchy Γ ν))
+def mod_indScheme_of_mod_indH [M ⊧ₘ* 𝐈𝐍𝐃 Γ n] : M ⊧ₘ* Theory.indScheme ℒₒᵣ (Arith.Hierarchy Γ n) :=
+  ModelsTheory.of_add_right M 𝐏𝐀⁻ (Theory.indScheme _ (Arith.Hierarchy Γ n))
 
-def mod_indScheme_of_mod_indH [(𝐈𝐍𝐃 Γ ν).Mod M] : (Theory.indScheme (L := ℒₒᵣ) (Arith.Hierarchy Γ ν)).Mod M :=
-  Theory.Mod.of_add_right M 𝐏𝐀⁻ (Theory.indScheme _ (Arith.Hierarchy Γ ν))
-
-instance [𝐏𝐀.Mod M] : 𝐏𝐀⁻.Mod M := Theory.Mod.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ Set.univ)
+instance [M ⊧ₘ* 𝐏𝐀] : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ Set.univ)
 
 end
 
@@ -155,7 +153,7 @@ namespace Standard
 
 variable {μ : Type v} (e : Fin n → ℕ) (ε : μ → ℕ)
 
-lemma modelsTheoryPeanoMinus : ℕ ⊧ₘ* 𝐏𝐀⁻ := by
+instance models_peanoMinus : ℕ ⊧ₘ* 𝐏𝐀⁻ := ⟨by
   intro σ h
   rcases h <;> simp [models_def, ←le_iff_eq_or_lt]
   case addAssoc => intro l m n; exact add_assoc l m n
@@ -167,22 +165,22 @@ lemma modelsTheoryPeanoMinus : ℕ ⊧ₘ* 𝐏𝐀⁻ := by
   case mulLtMul => rintro l m n h hl; exact (mul_lt_mul_right hl).mpr h
   case distr => intro l m n; exact Nat.mul_add l m n
   case ltTrans => intro l m n; exact Nat.lt_trans
-  case ltTri => intro n m; exact Nat.lt_trichotomy n m
+  case ltTri => intro n m; exact Nat.lt_trichotomy n m⟩
 
-lemma modelsSuccInd (p : Semiformula ℒₒᵣ ℕ 1) : ℕ ⊧ₘ (∀ᶠ* succInd p) := by
+lemma models_succInd (p : Semiformula ℒₒᵣ ℕ 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 modelsPeano : ℕ ⊧ₘ* 𝐏𝐀 := by
-  simp [Theory.peano, Theory.indScheme, modelsTheoryPeanoMinus]; rintro _ p _ rfl; simp [modelsSuccInd]
+instance models_peano : ℕ ⊧ₘ* 𝐏𝐀 := by
+  simp [Theory.peano, Theory.indScheme, models_peanoMinus]; rintro _ p _ rfl; simp [models_succInd]
 
 end Standard
 
 theorem peano_consistent : System.Consistent 𝐏𝐀 :=
-  Sound.consistent_of_model Standard.modelsPeano
+  Sound.consistent_of_model Standard.models_peano
 
 section
 
@@ -207,7 +205,7 @@ variable (T : Theory ℒₒᵣ) [𝐄𝐪 ≾ T]
 lemma oRing_consequence_of (σ : Sentence ℒₒᵣ)
   (H : ∀ (M : Type)
          [Zero M] [One M] [Add M] [Mul M] [LT M]
-         [Theory.Mod M T],
+         [M ⊧ₘ* T],
          M ⊧ₘ σ) :
     T ⊨ σ := consequence_of T σ fun M _ _ _ _ _ s _ _ ↦ by
   rcases standardModel_unique M s

Logic/FirstOrder/Arith/Nonstandard.lean

@@ -60,9 +60,9 @@ local notation "⋆" => star
 
 lemma models_union_trueArithWithStarUnbounded : ℕ⋆ ⊧ₘ* ⋃ c, trueArithWithStarUnbounded c := ModelOfSatEq.models _
 
-lemma trueArith : ℕ⋆ ⊧ₘ* 𝐓𝐀 := by
+instance trueArith : ℕ⋆ ⊧ₘ* 𝐓𝐀 := ⟨by
   have : ℕ⋆ ⊧ₘ* Semiformula.lMap (Language.Hom.add₁ _ _) '' 𝐓𝐀 :=
-    Semantics.realizeTheory_of_subset models_union_trueArithWithStarUnbounded
+    Semantics.RealizeTheory.of_subset models_union_trueArithWithStarUnbounded
       (Set.subset_iUnion_of_subset 0 $ Set.subset_union_of_subset_left (Set.subset_union_right _ _ ) _)
   intro σ hσ
   let s : Structure ℒₒᵣ ℕ⋆ := (ModelOfSatEq.struc satisfiable_union_trueArithWithStarUnbounded).lMap
@@ -77,19 +77,17 @@ lemma trueArith : ℕ⋆ ⊧ₘ* 𝐓𝐀 := by
         ←Semiformula.eval_lMap, Matrix.fun_eq_vec₂]⟩
     haveI : Structure.LT ℒₒᵣ ℕ⋆ := ⟨fun _ _ => iff_of_eq rfl⟩
     exact standardModel_unique _ _
-  have : s.toStruc ⊧ σ := Semiformula.models_lMap.mp (this (Set.mem_image_of_mem _ hσ))
-  exact e ▸ this
+  have : s.toStruc ⊧ σ := Semiformula.models_lMap.mp (this.realize (Set.mem_image_of_mem _ hσ))
+  exact e ▸ this⟩
 
-instance : Theory.Mod ℕ⋆ 𝐓𝐀 := ⟨trueArith⟩
-
-instance : Theory.Mod ℕ⋆ 𝐏𝐀⁻ :=
-  Theory.Mod.of_ss (T₁ := 𝐓𝐀) _ (Structure.subset_of_models.mpr $ Arith.Standard.modelsTheoryPeanoMinus)
+instance : ℕ⋆ ⊧ₘ* 𝐏𝐀⁻ :=
+  ModelsTheory.of_ss (U := 𝐓𝐀) inferInstance (Structure.subset_of_models.mpr $ Arith.Standard.models_peanoMinus)
 
 lemma star_unbounded (n : ℕ) : n < ⋆ := by
   have : ℕ⋆ ⊧ₘ (“!!(Semiterm.Operator.numeral ℒₒᵣ⋆ n) < ⋆” : Sentence ℒₒᵣ⋆) :=
-    models_union_trueArithWithStarUnbounded
+    models_union_trueArithWithStarUnbounded.realize
       (Set.mem_iUnion_of_mem (n + 1) (Set.mem_union_right _ $ Set.mem_range_self $ Fin.last n))
-  simpa [models_iff] using this
+  simpa [models_iff, Model.numeral_eq_natCast] using this
 
 end Nonstandard
 

Logic/FirstOrder/Arith/PeanoMinus.lean

@@ -11,7 +11,7 @@ namespace Arith
 
 noncomputable section
 
-variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [𝐏𝐀⁻.Mod M]
+variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻]
 
 open Language
 
@@ -22,55 +22,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.peanoMinus.addZero
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.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.peanoMinus.addAssoc
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.addAssoc
 
 protected lemma add_comm : ∀ x y : M, x + y = y + x := by
-  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.addComm
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.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.peanoMinus.addEqOfLt
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.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.peanoMinus.zeroLe
+  simpa[models_iff, Structure.le_iff_of_eq_of_lt] using ModelsTheory.models M Theory.peanoMinus.zeroLe
 
 lemma zero_lt_one : (0 : M) < 1 := by
-  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.zeroLtOne
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.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.peanoMinus.oneLeOfZeroLt
+  simpa[models_iff, Structure.le_iff_of_eq_of_lt] using ModelsTheory.models M Theory.peanoMinus.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.peanoMinus.addLtAdd
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.addLtAdd
 
 protected lemma mul_zero : ∀ x : M, x * 0 = 0 := by
-  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.mulZero
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.mulZero
 
 protected lemma mul_one : ∀ x : M, x * 1 = x := by
-  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.mulOne
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.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.peanoMinus.mulAssoc
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.mulAssoc
 
 protected lemma mul_comm : ∀ x y : M, x * y = y * x := by
-  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.mulComm
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.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.peanoMinus.mulLtMul
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.mulLtMul
 
 lemma distr : ∀ x y z : M, x * (y + z) = x * y + x * z := by
-  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.distr
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.distr
 
 lemma lt_irrefl : ∀ x : M, ¬x < x := by
-  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.ltIrrefl
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.ltIrrefl
 
 lemma lt_trans : ∀ x y z : M, x < y → y < z → x < z := by
-  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.ltTrans
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.ltTrans
 
 lemma lt_tri : ∀ x y : M, x < y ∨ x = y ∨ y < x := by
-  simpa[models_iff] using Theory.Mod.models M Theory.peanoMinus.ltTri
+  simpa[models_iff] using ModelsTheory.models M Theory.peanoMinus.ltTri
 
 instance : AddCommMonoid M where
   add_assoc := Model.add_assoc
@@ -140,7 +140,7 @@ instance : CanonicallyOrderedAddCommMonoid M where
     · simpa[eq_comm] using add_eq_of_lt x y h
   le_self_add := by intro x y; simp
 
-@[simp] lemma numeral_eq_natCast : (n : ℕ) → (ORingSymbol.numeral n : M) = n
+lemma numeral_eq_natCast : (n : ℕ) → (ORingSymbol.numeral n : M) = n
   | 0     => rfl
   | 1     => by simp
   | n + 2 => by simp[ORingSymbol.numeral, numeral_eq_natCast (n + 1), add_assoc, one_add_one_eq_two]
@@ -214,7 +214,7 @@ variable {T : Theory ℒₒᵣ} [𝐄𝐪 ≾ T] [𝐏𝐀⁻ ≾ T]
 theorem sigma_one_completeness {σ : Sentence ℒₒᵣ} (hσ : Hierarchy Σ 1 σ) :
     ℕ ⊧ₘ σ → T ⊢ σ := fun H =>
   Complete.complete (oRing_consequence_of _ _ (fun M _ _ _ _ _ _ => by
-    haveI : 𝐏𝐀⁻.Mod M := Theory.Mod.of_subtheory (T₁ := T) M (Semantics.ofSystemSubtheory _ _)
+    haveI : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_subtheory (T₁ := T) inferInstance (Semantics.ofSystemSubtheory _ _)
     simpa [Matrix.empty_eq] using Model.pval_of_pval_nat_of_sigma_one (M := M) hσ H))
 
 end

Logic/FirstOrder/Arith/Representation.lean

@@ -36,7 +36,7 @@ def code (c : Code k) : Semisentence ℒₒᵣ (k + 1) := (Rew.bind ![] (#0 :> (
 
 section model
 
-variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [𝐏𝐀⁻.Mod M]
+variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻]
 
 lemma codeAux_uniq {k} {c : Code k} {v : Fin k → M} {z z' : M} :
     Semiformula.Val! M (z :> v) (codeAux c) → Semiformula.Val! M (z' :> v) (codeAux c) → z = z' := by
@@ -88,9 +88,11 @@ lemma codeAux_sigma_one {k} (c : Nat.ArithPart₁.Code k) : Hierarchy Σ 1 (code
 lemma code_sigma_one {k} (c : Nat.ArithPart₁.Code k) : Hierarchy Σ 1 (code c) :=
   Hierarchy.rew _ (codeAux_sigma_one c)
 
+@[simp] lemma natCast_nat (n : ℕ) : Nat.cast n = n := by rfl
+
 lemma models_codeAux {c : Code k} {f : Vector ℕ k →. ℕ} (hc : c.eval f) (y : ℕ) (v : Fin k → ℕ) :
     Semiformula.Val! ℕ (y :> v) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y := by
-  induction hc generalizing y <;> simp[code, codeAux, models_iff]
+  induction hc generalizing y <;> simp [code, codeAux, models_iff]
   case zero =>
     have : (0 : Part ℕ) = Part.some 0 := rfl
     simp[this, eq_comm]
@@ -172,12 +174,12 @@ lemma provable_computable_code_uniq {k} {f : Vector ℕ k → ℕ}
     T ⊢! ∀' ((Rew.substs $ #0 :> (⸢v ·⸣)).hom (code $ codeOfPartrec f)
       ⟷ “#0 = !!(⸢f (Vector.ofFn v)⸣)”) :=
   Complete.consequence_iff_provable.mp (oRing_consequence_of _ _ (fun M _ _ _ _ _ _ => by
-    haveI : 𝐏𝐀⁻.Mod M :=
-      Theory.Mod.of_subtheory (T₁ := T) M (Semantics.ofSystemSubtheory _ _)
+    haveI : M ⊧ₘ* 𝐏𝐀⁻ :=
+      ModelsTheory.of_subtheory (T₁ := T) inferInstance (Semantics.ofSystemSubtheory _ _)
     have Hfv : Semiformula.PVal! M (f (Vector.ofFn v) :> (v ·)) (code (codeOfPartrec f)) := by
-      simpa[models_iff, Semiformula.eval_substs, Matrix.comp_vecCons'] using
+      simpa [Model.numeral_eq_natCast, models_iff, Semiformula.eval_substs, Matrix.comp_vecCons'] using
         consequence_iff'.mp (Sound.sound! (provable_iff_computable T hf v)) M
-    simp[models_iff, Semiformula.eval_substs, Matrix.comp_vecCons']
+    simp [Model.numeral_eq_natCast, models_iff, Semiformula.eval_substs, Matrix.comp_vecCons']
     intro x; constructor
     · intro H; exact code_uniq H Hfv
     · rintro rfl; simpa))
@@ -240,7 +242,7 @@ noncomputable def pred (p : α → Prop) : Semisentence ℒₒᵣ 1 :=
 
 theorem pred_representation {p : α → Prop} (hp : RePred p) {x} :
     T ⊢! (pred p)/[⸢x⸣] ↔ p x := by
-  simpa[pred, ←Rew.hom_comp_app, Rew.substs_comp_substs] using
+  simpa [pred, ←Rew.hom_comp_app, Rew.substs_comp_substs] using
     representation hp (T := T) (x := x) (y := ())
 
 end representation