refactor(FirstOrder): WeakerThan

FormalizedFormalLogic · Feb 14, 2025 · 2b158b5 · 2b158b5
1 parent a668f38
commit 2b158b5
Show file tree

Hide file tree

Showing 4 changed files with 41 additions and 25 deletions.
diff --git a/Foundation/FirstOrder/Arith/Basic.lean b/Foundation/FirstOrder/Arith/Basic.lean
@@ -198,9 +198,9 @@ end
 
 section
 
-variable {L : Language.{u}} [L.ORing] (T : Theory L) [𝐄𝐐 ⪯ T]
+variable {L : Language.{u}} [L.ORing] (T : Theory L)
 
-lemma consequence_of (φ : SyntacticFormula L)
+lemma consequence_of [𝐄𝐐 ⪯ T] (φ : SyntacticFormula L)
   (H : ∀ (M : Type (max u w))
          [ORingStruc M]
          [Structure L M]

diff --git a/Foundation/FirstOrder/Arith/Model.lean b/Foundation/FirstOrder/Arith/Model.lean
@@ -227,13 +227,18 @@ instance (T : Theory ℒₒᵣ) [ℕ ⊧ₘ* T] : T ⪯ 𝐓𝐀 := ⟨by
   have : ℕ ⊧ₘ φ := consequence_iff'.mp (sound₀! h) ℕ
   exact trueArith_provable_iff.mpr this⟩
 
-variable (T : Theory ℒₒᵣ) [𝐄𝐐 ⪯ T]
-
-lemma oRing_consequence_of (φ : SyntacticFormula ℒₒᵣ) (H : ∀ (M : Type*) [ORingStruc M] [M ⊧ₘ* T], M ⊧ₘ φ) :
+lemma oRing_consequence_of (T : Theory ℒₒᵣ) [𝐄𝐐 ⪯ T] (φ : SyntacticFormula ℒₒᵣ) (H : ∀ (M : Type*) [ORingStruc M] [M ⊧ₘ* T], M ⊧ₘ φ) :
     T ⊨ φ := consequence_of T φ fun M _ s _ _ ↦ by
   rcases standardModel_unique M s
   exact H M
 
+lemma oRing_weakerThan_of (T S : Theory ℒₒᵣ) [𝐄𝐐 ⪯ S]
+    (H : ∀ (M : Type*)
+           [ORingStruc M]
+           [M ⊧ₘ* S],
+           M ⊧ₘ* T) : T ⪯ S :=
+  Entailment.weakerThan_iff.mpr fun h ↦ complete <| oRing_consequence_of _ _ fun M _ _ ↦ sound! h (H M)
+
 end Arith
 
 namespace Theory

diff --git a/Foundation/FirstOrder/Arith/PeanoMinus.lean b/Foundation/FirstOrder/Arith/PeanoMinus.lean
@@ -167,32 +167,34 @@ lemma eq_nat_of_lt_nat : ∀ {n : ℕ} {x : M}, x < n → ∃ m : ℕ, x = m
     · exact ⟨n, rfl⟩
     · exact eq_nat_of_lt_nat hx
 
-end Arith
-
-namespace FirstOrder.Arith
-
-open LO.Arith
-
-variable {T : Theory ℒₒᵣ} [𝐏𝐀⁻ ⪯ T]
-
-instance CobhamR0.subTheoryPeanoMinus : 𝐑₀ ⪯ 𝐏𝐀⁻ := Entailment.WeakerThan.ofAxm! <| by
+instance qq : M ⊧ₘ* 𝐑₀ := modelsTheory_iff.mpr <| by
   intro φ h
   rcases h
   case equal h =>
-    exact Entailment.by_axm _ (Theory.PeanoMinus.equal _ h)
+    have : M ⊧ₘ* (𝐄𝐐 : Theory ℒₒᵣ) := inferInstance
+    exact modelsTheory_iff.mp this h
   case Ω₁ n m =>
-    apply complete <| oRing_consequence_of.{0} _ _ <| fun M _ _ => by simp [models_iff, numeral_eq_natCast]
+    simp [models_iff, numeral_eq_natCast]
   case Ω₂ n m =>
-    apply complete <| oRing_consequence_of.{0} _ _ <| fun M _ _ => by simp [models_iff, numeral_eq_natCast]
+    simp [models_iff, numeral_eq_natCast]
   case Ω₃ n m h =>
-    apply complete <| oRing_consequence_of.{0} _ _ <| fun M _ _ => by simp [models_iff, numeral_eq_natCast, h]
+    simp [models_iff, numeral_eq_natCast, h]
   case Ω₄ n =>
-    apply complete <| oRing_consequence_of.{0} _ _ <| fun M _ _ => by
       simp [models_iff, numeral_eq_natCast]; intro x
       constructor
       · intro hx; rcases eq_nat_of_lt_nat hx with ⟨x, rfl⟩; exact ⟨x, by simpa using hx, by simp⟩
       · rintro ⟨i, hi, rfl⟩; simp [hi]
 
+end Arith
+
+namespace FirstOrder.Arith
+
+open LO.Arith
+
+variable {T : Theory ℒₒᵣ} [𝐏𝐀⁻ ⪯ T]
+
+instance : 𝐑₀ ⪯ 𝐏𝐀⁻ := oRing_weakerThan_of.{0} _ _ fun _ _ _ ↦ inferInstance
+
 instance : 𝐑₀ ⪱ 𝐏𝐀⁻ :=
   Entailment.StrictlyWeakerThan.of_unprovable_provable
     R₀_unprovable_add_zero

diff --git a/Foundation/Logic/Entailment.lean b/Foundation/Logic/Entailment.lean
@@ -538,27 +538,36 @@ end
 
 section
 
-variable {𝓢 : S} {T : Set F} [Complete 𝓢 (Semantics.models M T)]
+variable {𝓢 : S} {s : Set F} [Complete 𝓢 (Semantics.models M s)]
 
-lemma provable_of_consequence {f : F} : T ⊨[M] f → 𝓢 ⊢! f := complete
+lemma provable_of_consequence {f : F} : s ⊨[M] f → 𝓢 ⊢! f := complete
 
-lemma provable_iff_consequence [Sound 𝓢 (Semantics.models M T)] {f : F} : T ⊨[M] f ↔ 𝓢 ⊢! f := ⟨complete, Sound.sound⟩
+lemma provable_iff_consequence [Sound 𝓢 (Semantics.models M s)] {f : F} : s ⊨[M] f ↔ 𝓢 ⊢! f := ⟨complete, Sound.sound⟩
+
+
+section
 
 variable [LogicalConnective F] [∀ 𝓜 : M, Semantics.Meaningful 𝓜]
 
 lemma satisfiable_of_consistent :
-    Entailment.Consistent 𝓢 → Semantics.Satisfiable M T :=
+    Entailment.Consistent 𝓢 → Semantics.Satisfiable M s :=
   fun H ↦ Semantics.meaningful_iff_satisfiableSet.mpr (meaningful_of_consistent H)
 
 lemma inconsistent_of_unsatisfiable :
-    ¬Semantics.Satisfiable M T → Entailment.Inconsistent 𝓢 := by
+    ¬Semantics.Satisfiable M s → Entailment.Inconsistent 𝓢 := by
   contrapose; simpa [←Entailment.not_consistent_iff_inconsistent] using satisfiable_of_consistent
 
-lemma consistent_iff_satisfiable [Sound 𝓢 (Semantics.models M T)] : Entailment.Consistent 𝓢 ↔ Semantics.Satisfiable M T :=
+lemma consistent_iff_satisfiable [Sound 𝓢 (Semantics.models M s)] : Entailment.Consistent 𝓢 ↔ Semantics.Satisfiable M s :=
   ⟨satisfiable_of_consistent, Sound.consistent_of_satisfiable⟩
 
 end
 
+lemma weakerthan_of_models {𝓣 : S} {t : Set F} [Sound 𝓣 (Semantics.models M t)]
+    (H : ∀ 𝓜 : M, 𝓜 ⊧* s → 𝓜 ⊧* t) : 𝓣 ⪯ 𝓢 :=
+  Entailment.weakerThan_iff.mpr <| fun h ↦ provable_of_consequence <| fun 𝓜 h𝓜 ↦ Sound.consequence_of_provable (M := M) (T := t) h (H 𝓜 h𝓜)
+
+end
+
 end Complete
 
 end