Refactor System WeakerThan (#198)

* WeakerThan

* `System` ↦ `Entailment`

* remove

Foundation.lean

@@ -4,7 +4,7 @@ import Foundation.Vorspiel.Order
 
 import Foundation.Logic.LogicSymbol
 import Foundation.Logic.Semantics
-import Foundation.Logic.System
+import Foundation.Logic.Entailment
 
 -- AutoProver
 

Foundation/FirstOrder/Arith/Basic.lean

@@ -191,14 +191,14 @@ section
 
 variable {L : Language} [Structure L ℕ] (T : Theory L) (F : Set (Sentence L))
 
-lemma consistent_of_sound [SoundOn T F] (hF : ⊥ ∈ F) : System.Consistent T :=
-  System.consistent_iff_unprovable_bot.mpr fun b ↦ by simpa [Models₀] using SoundOn.sound (F := F) hF b
+lemma consistent_of_sound [SoundOn T F] (hF : ⊥ ∈ F) : Entailment.Consistent T :=
+  Entailment.consistent_iff_unprovable_bot.mpr fun b ↦ by simpa [Models₀] using SoundOn.sound (F := F) hF b
 
 end
 
 section
 
-variable {L : Language.{u}} [L.ORing] (T : Theory L) [𝐄𝐐 ≼ T]
+variable {L : Language.{u}} [L.ORing] (T : Theory L) [𝐄𝐐 ⪯ T]
 
 lemma consequence_of (φ : SyntacticFormula L)
   (H : ∀ (M : Type (max u w))
@@ -246,13 +246,14 @@ notation "𝐄𝐐'" => EQ'
 
 variable (T : Theory L)
 
-noncomputable instance EQ'.subTheoryOfEQ : (𝐄𝐐' : Theory L) ≼ 𝐄𝐐 := System.Subtheory.ofAxm! <| by
+noncomputable instance EQ'.subTheoryOfEQ : (𝐄𝐐' : Theory L) ⪯ 𝐄𝐐 := Entailment.WeakerThan.ofAxm! <| by
   rintro φ h
   rcases (show 𝐄𝐐' φ from h)
   case refl =>
-    apply System.by_axm _ (by simpa using eqAxiom.refl)
+    apply Entailment.by_axm _ (by simpa using eqAxiom.refl)
   case replace φ =>
-    apply complete <| EQ.provOf.{0, 0} _ ?_
+    apply complete ?_
+    apply EQ.provOf.{_, 0} _ ?_
     intro M _ s _ _
     simp [models_iff, Semiformula.eval_substs]
 

Foundation/FirstOrder/Arith/CobhamR0.lean

@@ -96,18 +96,18 @@ namespace FirstOrder.Arith
 
 open LO.Arith
 
-variable {T : Theory ℒₒᵣ} [𝐑₀ ≼ T]
+variable {T : Theory ℒₒᵣ} [𝐑₀ ⪯ T]
 
 theorem sigma_one_completeness {σ : Sentence ℒₒᵣ} (hσ : Hierarchy 𝚺 1 σ) :
     ℕ ⊧ₘ₀ σ → T ⊢! ↑σ := fun H =>
-  haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐑₀) inferInstance inferInstance
+  haveI : 𝐄𝐐 ⪯ T := Entailment.WeakerThan.trans (𝓣 := 𝐑₀) inferInstance inferInstance
   complete <| oRing_consequence_of.{0} _ _ <| fun M _ _ => by
-    haveI : M ⊧ₘ* 𝐑₀ := ModelsTheory.of_provably_subtheory M 𝐑₀ T inferInstance (by assumption)
+    haveI : M ⊧ₘ* 𝐑₀ := ModelsTheory.of_provably_subtheory M 𝐑₀ T inferInstance
     exact LO.Arith.sigma_one_completeness hσ H
 
 theorem sigma_one_completeness_iff [ss : Sigma1Sound T] {σ : Sentence ℒₒᵣ} (hσ : Hierarchy 𝚺 1 σ) :
     ℕ ⊧ₘ₀ σ ↔ T ⊢! ↑σ :=
-  haveI : 𝐑₀ ≼ T := System.Subtheory.comp (𝓣 := T) inferInstance inferInstance
+  haveI : 𝐑₀ ⪯ T := Entailment.WeakerThan.trans (𝓣 := T) inferInstance inferInstance
   ⟨fun h ↦ sigma_one_completeness (T := T) hσ h, fun h ↦ ss.sound (by simp [hσ]) h⟩
 
 end FirstOrder.Arith

Foundation/FirstOrder/Arith/Hierarchy.lean

@@ -359,7 +359,7 @@ variable {L : Language} [L.LT] [Structure L ℕ]
 abbrev Sigma1Sound (T : Theory L) := SoundOn T (Hierarchy 𝚺 1)
 
 lemma consistent_of_sigma1Sound (T : Theory L) [Sigma1Sound T] :
-    System.Consistent T := consistent_of_sound T (Hierarchy 𝚺 1) (by simp [Set.mem_def])
+    Entailment.Consistent T := consistent_of_sound T (Hierarchy 𝚺 1) (by simp [Set.mem_def])
 
 end
 

Foundation/FirstOrder/Arith/Model.lean

@@ -217,7 +217,7 @@ notation "𝐓𝐀" => Theory.TrueArith
 instance Standard.models_trueArith : ℕ ⊧ₘ* 𝐓𝐀 :=
   modelsTheory_iff.mpr fun {φ} ↦ by simp
 
-variable (T : Theory ℒₒᵣ) [𝐄𝐐 ≼ T]
+variable (T : Theory ℒₒᵣ) [𝐄𝐐 ⪯ T]
 
 lemma oRing_consequence_of (φ : SyntacticFormula ℒₒᵣ) (H : ∀ (M : Type*) [ORingStruc M] [M ⊧ₘ* T], M ⊧ₘ φ) :
     T ⊨ φ := consequence_of T φ fun M _ s _ _ ↦ by
@@ -230,10 +230,10 @@ namespace Theory
 
 open Arith
 
-instance CobhamR0.consistent : System.Consistent 𝐑₀ :=
+instance CobhamR0.consistent : Entailment.Consistent 𝐑₀ :=
   Sound.consistent_of_satisfiable ⟨_, Standard.models_CobhamR0⟩
 
-instance Peano.consistent : System.Consistent 𝐏𝐀 :=
+instance Peano.consistent : Entailment.Consistent 𝐏𝐀 :=
   Sound.consistent_of_satisfiable ⟨_, Standard.models_peano⟩
 
 end Theory

Foundation/FirstOrder/Arith/Nonstandard.lean

@@ -41,8 +41,8 @@ lemma satisfiable_union_trueArithWithStarUnbounded :
   (Compact.compact_cumulative trueArithWithStarUnbounded.cumulative).mpr
     satisfiable_trueArithWithStarUnbounded
 
-instance trueArithWithStarUnbounded.eqTheory : 𝐄𝐐 ≼ (⋃ c, trueArithWithStarUnbounded c) :=
-  System.Subtheory.ofSubset <|
+instance trueArithWithStarUnbounded.eqTheory : 𝐄𝐐 ⪯ (⋃ c, trueArithWithStarUnbounded c) :=
+  Entailment.WeakerThan.ofSubset <|
     Set.subset_iUnion_of_subset 0 (Set.subset_union_of_subset_left (by simp) _)
 
 abbrev Nonstandard : Type := ModelOfSatEq satisfiable_union_trueArithWithStarUnbounded

Foundation/FirstOrder/Arith/PeanoMinus.lean

@@ -173,13 +173,13 @@ namespace FirstOrder.Arith
 
 open LO.Arith
 
-variable {T : Theory ℒₒᵣ} [𝐏𝐀⁻ ≼ T]
+variable {T : Theory ℒₒᵣ} [𝐏𝐀⁻ ⪯ T]
 
-instance CobhamR0.subTheoryPAMinus : 𝐑₀ ≼ 𝐏𝐀⁻ := System.Subtheory.ofAxm! <| by
+instance CobhamR0.subTheoryPAMinus : 𝐑₀ ⪯ 𝐏𝐀⁻ := Entailment.WeakerThan.ofAxm! <| by
   intro φ h
   rcases h
   case equal h =>
-    exact System.by_axm _ (Theory.PAMinus.equal _ h)
+    exact Entailment.by_axm _ (Theory.PAMinus.equal _ h)
   case Ω₁ n m =>
     apply complete <| oRing_consequence_of.{0} _ _ <| fun M _ _ => by simp [models_iff, numeral_eq_natCast]
   case Ω₂ n m =>

Foundation/FirstOrder/Arith/Representation.lean

@@ -380,7 +380,7 @@ lemma codeOfRePred_spec {p : ℕ → Prop} (hp : RePred p) {x : ℕ} :
   simp [Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.constant_eq_singleton]
   apply (codeOfPartrec'_spec (Nat.Partrec'.of_part this) (v := ![x]) (y := 0)).trans (by simp [f])
 
-variable {T : Theory ℒₒᵣ} [𝐑₀ ≼ T] [Sigma1Sound T]
+variable {T : Theory ℒₒᵣ} [𝐑₀ ⪯ T] [Sigma1Sound T]
 
 lemma re_complete {p : ℕ → Prop} (hp : RePred p) {x : ℕ} :
     p x ↔ T ⊢! ↑((codeOfRePred p)/[‘↑x’] : Sentence ℒₒᵣ) := Iff.trans

Foundation/FirstOrder/Arith/Theory.lean

@@ -88,15 +88,15 @@ lemma coe_indH_subset_indH : (indScheme ℒₒᵣ (Arith.Hierarchy Γ ν) : Theo
   exact ⟨Semiformula.lMap (Language.oringEmb : ℒₒᵣ →ᵥ L) φ, Hierarchy.oringEmb Hp,
     by simp [succInd, Semiformula.lMap_substs]⟩
 
-instance PAMinus.subtheoryOfIndH : 𝐏𝐀⁻ ≼ 𝐈𝐍𝐃Γ n := System.Subtheory.ofSubset (by simp [indH, Theory.add_def])
+instance PAMinus.subtheoryOfIndH : 𝐏𝐀⁻ ⪯ 𝐈𝐍𝐃Γ n := Entailment.WeakerThan.ofSubset (by simp [indH, Theory.add_def])
 
-instance EQ.subtheoryOfCobhamR0 : 𝐄𝐐 ≼ 𝐑₀ := System.Subtheory.ofSubset <| fun φ hp ↦ CobhamR0.equal φ hp
+instance EQ.subtheoryOfCobhamR0 : 𝐄𝐐 ⪯ 𝐑₀ := Entailment.WeakerThan.ofSubset <| fun φ hp ↦ CobhamR0.equal φ hp
 
-instance EQ.subtheoryOfPAMinus : 𝐄𝐐 ≼ 𝐏𝐀⁻ := System.Subtheory.ofSubset <| fun φ hp ↦ PAMinus.equal φ hp
+instance EQ.subtheoryOfPAMinus : 𝐄𝐐 ⪯ 𝐏𝐀⁻ := Entailment.WeakerThan.ofSubset <| fun φ hp ↦ PAMinus.equal φ hp
 
-instance EQ.subtheoryOfIndH : 𝐄𝐐 ≼ 𝐈𝐍𝐃Γ n := System.Subtheory.comp PAMinus.subtheoryOfIndH EQ.subtheoryOfPAMinus
+instance EQ.subtheoryOfIndH : 𝐄𝐐 ⪯ 𝐈𝐍𝐃Γ n := Entailment.WeakerThan.trans (inferInstanceAs (𝐄𝐐 ⪯ 𝐏𝐀⁻)) inferInstance
 
-instance EQ.subtheoryOfIOpen : 𝐄𝐐 ≼ 𝐈open := System.Subtheory.comp inferInstance EQ.subtheoryOfPAMinus
+instance EQ.subtheoryOfIOpen : 𝐄𝐐 ⪯ 𝐈open := Entailment.WeakerThan.trans (inferInstanceAs (𝐄𝐐 ⪯ 𝐏𝐀⁻)) inferInstance
 
 end Theory
 

Foundation/FirstOrder/Basic/Calculus.lean

@@ -313,18 +313,18 @@ private def deductionAux {Γ : Sequent L} : T ⟹ Γ → T \ {φ} ⟹ ∼(∀∀
 
 def deduction (d : insert φ T ⟹ Γ) : T ⟹ ∼(∀∀φ) :: Γ := Tait.ofAxiomSubset (by intro x; simp; tauto) (deductionAux d (φ := φ))
 
-def provable_iff_inconsistent : T ⊢! φ ↔ System.Inconsistent (insert (∼∀∀φ) T) := by
+def provable_iff_inconsistent : T ⊢! φ ↔ Entailment.Inconsistent (insert (∼∀∀φ) T) := by
   constructor
   · rintro b
-    exact System.inconsistent_of_provable_of_unprovable
-      (System.wk! (by simp) (toClose! b)) (System.by_axm _ (by simp))
+    exact Entailment.inconsistent_of_provable_of_unprovable
+      (Entailment.wk! (by simp) (toClose! b)) (Entailment.by_axm _ (by simp))
   · intro h
     rcases Tait.inconsistent_iff_provable.mp h with ⟨d⟩
     have : T ⊢ ∀∀φ :=  Derivation.cast (deduction d) (by rw [close_eq_self_of (∼∀∀φ) (by simp)]; simp)
     exact ⟨invClose this⟩
 
-def unprovable_iff_consistent : T ⊬ φ ↔ System.Consistent (insert (∼∀∀φ) T) := by
-  simp [←System.not_inconsistent_iff_consistent, ←provable_iff_inconsistent]
+def unprovable_iff_consistent : T ⊬ φ ↔ Entailment.Consistent (insert (∼∀∀φ) T) := by
+  simp [←Entailment.not_inconsistent_iff_consistent, ←provable_iff_inconsistent]
 
 section Hom
 
@@ -363,8 +363,8 @@ def lMap (Φ : L₁ →ᵥ L₂) {Δ} : T₁ ⟹ Δ → T₁.lMap Φ ⟹ Δ.map
     Derivation.cast this (by simp[Finset.image_union])
   | root h               => root (Set.mem_image_of_mem _ h)
 
-lemma inconsistent_lMap (Φ : L₁ →ᵥ L₂) : System.Inconsistent T₁ → System.Inconsistent (T₁.lMap Φ) := by
-  simp only [System.inconsistent_iff_provable_bot]; intro ⟨b⟩; exact ⟨by simpa using lMap Φ b⟩
+lemma inconsistent_lMap (Φ : L₁ →ᵥ L₂) : Entailment.Inconsistent T₁ → Entailment.Inconsistent (T₁.lMap Φ) := by
+  simp only [Entailment.inconsistent_iff_provable_bot]; intro ⟨b⟩; exact ⟨by simpa using lMap Φ b⟩
 
 end Hom
 
@@ -422,9 +422,9 @@ end Derivation
 
 namespace Theory
 
-instance {T U : Theory L} : T ≼ T + U := System.Axiomatized.subtheoryOfSubset (by simp [add_def])
+instance {T U : Theory L} : T ⪯ T + U := Entailment.Axiomatized.weakerThanOfSubset (by simp [add_def])
 
-instance {T U : Theory L} : U ≼ T + U := System.Axiomatized.subtheoryOfSubset (by simp [add_def])
+instance {T U : Theory L} : U ⪯ T + U := Entailment.Axiomatized.weakerThanOfSubset (by simp [add_def])
 
 end Theory
 
@@ -440,7 +440,7 @@ variable {L}
 
 alias Theory.alt := Theory.Alt.mk
 
-instance : System (Sentence L) (Theory.Alt L) := ⟨fun T σ ↦ T.thy ⊢ ↑σ⟩
+instance : Entailment (Sentence L) (Theory.Alt L) := ⟨fun T σ ↦ T.thy ⊢ ↑σ⟩
 
 @[simp] lemma Theory.alt_thy (T : Theory L) : T.alt.thy = T := rfl
 
@@ -454,7 +454,7 @@ abbrev Unprovable₀ (T : Theory L) (σ : Sentence L) : Prop := T.alt ⊬ σ
 
 infix:45 " ⊬. " => Unprovable₀
 
-instance (T : Theory.Alt L) : System.Classical T := System.Classical.ofEquiv T.thy T (Rewriting.app Rew.emb) (fun _ ↦ .refl _)
+instance (T : Theory.Alt L) : Entailment.Classical T := Entailment.Classical.ofEquiv T.thy T (Rewriting.app Rew.emb) (fun _ ↦ .refl _)
 
 variable {T : Theory L} {σ : Sentence L}
 

Foundation/FirstOrder/Basic/Eq.lean

@@ -187,7 +187,7 @@ end Eq
 
 end Structure
 
-lemma consequence_iff_eq {T : Theory L} [𝐄𝐐 ≼ T] {φ : SyntacticFormula L} :
+lemma consequence_iff_eq {T : Theory L} [𝐄𝐐 ⪯ T] {φ : SyntacticFormula L} :
     T ⊨[Struc.{v, u} L] φ ↔ (∀ (M : Type v) [Nonempty M] [Structure L M] [Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ φ) := by
   simp [consequence_iff]; constructor
   · intro h M x s _ hM; exact h M x hM
@@ -197,11 +197,11 @@ lemma consequence_iff_eq {T : Theory L} [𝐄𝐐 ≼ T] {φ : SyntacticFormula
     have e : Structure.Eq.QuotEq L M ≡ₑ[L] M := Structure.Eq.QuotEq.elementaryEquiv L M
     exact e.models.mp $ h (Structure.Eq.QuotEq L M) ⟦x⟧ (e.modelsTheory.mpr hM)
 
-lemma consequence_iff_eq' {T : Theory L} [𝐄𝐐 ≼ T] {φ : SyntacticFormula L} :
+lemma consequence_iff_eq' {T : Theory L} [𝐄𝐐 ⪯ T] {φ : SyntacticFormula L} :
     T ⊨[Struc.{v, u} L] φ ↔ (∀ (M : Type v) [Nonempty M] [Structure L M] [Structure.Eq L M] [M ⊧ₘ* T], M ⊧ₘ φ) := by
   rw [consequence_iff_eq]
 
-lemma satisfiable_iff_eq {T : Theory L} [𝐄𝐐 ≼ T] :
+lemma satisfiable_iff_eq {T : Theory L} [𝐄𝐐 ⪯ T] :
     Semantics.Satisfiable (Struc.{v, u} L) T ↔ (∃ (M : Type v) (_ : Nonempty M) (_ : Structure L M) (_ : Structure.Eq L M), M ⊧ₘ* T) := by
   simp [satisfiable_iff]; constructor
   · intro ⟨M, x, s, hM⟩;
@@ -211,15 +211,15 @@ lemma satisfiable_iff_eq {T : Theory L} [𝐄𝐐 ≼ T] :
     exact ⟨Structure.Eq.QuotEq L M, ⟦x⟧, inferInstance, inferInstance, e.modelsTheory.mpr hM⟩
   · intro ⟨M, i, s, _, hM⟩; exact ⟨M, i, s, hM⟩
 
-instance {T : Theory L} [𝐄𝐐 ≼ T] (sat : Semantics.Satisfiable (Struc.{v, u} L) T) :
+instance {T : Theory L} [𝐄𝐐 ⪯ T] (sat : Semantics.Satisfiable (Struc.{v, u} L) T) :
     ModelOfSat sat ⊧ₘ* (𝐄𝐐 : Theory L) := models_of_subtheory (ModelOfSat.models sat)
 
-def ModelOfSatEq {T : Theory L} [𝐄𝐐 ≼ T] (sat : Semantics.Satisfiable (Struc.{v, u} L) T) : Type _ :=
+def ModelOfSatEq {T : Theory L} [𝐄𝐐 ⪯ T] (sat : Semantics.Satisfiable (Struc.{v, u} L) T) : Type _ :=
   Structure.Eq.QuotEq L (ModelOfSat sat)
 
 namespace ModelOfSatEq
 
-variable {T : Theory L} [𝐄𝐐 ≼ T] (sat : Semantics.Satisfiable (Struc.{v, u} L) T)
+variable {T : Theory L} [𝐄𝐐 ⪯ T] (sat : Semantics.Satisfiable (Struc.{v, u} L) T)
 
 noncomputable instance : Nonempty (ModelOfSatEq sat) := Structure.Eq.QuotEq.inhabited
 

Foundation/FirstOrder/Basic/Soundness.lean

@@ -65,8 +65,9 @@ variable {φ : SyntacticFormula L}
 
 theorem sound : T ⊢ φ → T ⊨[Struc.{v, u} L] φ := fun b s hT f ↦ by
   haveI : s.Dom ⊧ₘ* T := hT
-  rcases Derivation.sound s.Dom f b with ⟨φ, hp, h⟩
-  simp at hp; rcases hp with rfl
+  rcases Derivation.sound s.Dom f b with ⟨ψ, hp, h⟩
+  have : ψ = φ := by simpa using hp
+  rcases this
   exact h
 
 theorem sound! : T ⊢! φ → T ⊨[Struc.{v, u} L] φ := fun ⟨b⟩ ↦ sound b
@@ -77,12 +78,12 @@ theorem sound₀! : T ⊢! φ → T ⊨ φ := sound!
 
 instance (T : Theory L) : Sound T (Semantics.models (Struc.{v, u} L) T) := ⟨sound!⟩
 
-lemma models_of_subtheory {T U : Theory L} [U ≼ T] {M : Type*} [Structure L M] [Nonempty M] (hM : M ⊧ₘ* T) : M ⊧ₘ* U :=
+lemma models_of_subtheory {T U : Theory L} [U ⪯ T] {M : Type*} [Structure L M] [Nonempty M] (hM : M ⊧ₘ* T) : M ⊧ₘ* U :=
   ⟨ fun {φ} hp ↦ by
-    have : T ⊢ φ := System.Subtheory.prf (System.byAxm hp)
-    exact sound this hM ⟩
+    have : T ⊢! φ := (inferInstanceAs (U ⪯ T)).pbl (Entailment.by_axm _ hp)
+    exact sound! this hM ⟩
 
-lemma consistent_of_satidfiable (h : Semantics.Satisfiable (Struc.{v, u} L) T) : System.Consistent T :=
+lemma consistent_of_satidfiable (h : Semantics.Satisfiable (Struc.{v, u} L) T) : Entailment.Consistent T :=
   Sound.consistent_of_satisfiable h
 
 end sound

Foundation/FirstOrder/Basic/Syntax/Rew.lean

@@ -2,7 +2,7 @@ import Foundation.Logic.Predicate.Rew
 import Foundation.FirstOrder.Basic.Syntax.Formula
 
 /-!
-# Rewriting System
+# Rewriting Entailment
 
 term/formula morphisms such as Rewritings, substitutions, and embeddings are handled by the structure `LO.FirstOrder.Rew`.
 - `LO.FirstOrder.Rew.rewrite f` is a Rewriting of the free variables occurring in the term by `f : ξ₁ → Semiterm L ξ₂ n`.

Foundation/FirstOrder/Completeness/Coding.lean

@@ -7,7 +7,7 @@ namespace FirstOrder
 open Semiformula
 variable {L : Language.{u}}
 
-namespace System
+namespace Entailment
 
 inductive Code (L : Language.{u})
   | axL : {k : ℕ} → (r : L.Rel k) → (v : Fin k → SyntacticTerm L) → Code L
@@ -54,7 +54,7 @@ instance [∀ k, DecidableEq (L.Func k)] [∀ k, DecidableEq (L.Rel k)] [∀ k,
   haveI : Encodable Empty := IsEmpty.toEncodable
   Encodable.ofEquiv _ (Code.equiv L)
 
-end System
+end Entailment
 
 end FirstOrder
 

Foundation/FirstOrder/Completeness/Completeness.lean

@@ -53,27 +53,27 @@ theorem complete {φ : SyntacticFormula L} :
       rw[←image_u']
       simpa using (satisfiable_lMap L.ofSubLanguage (fun k ↦ Subtype.val_injective) (fun _ ↦ Subtype.val_injective) h)
     contradiction
-  have : System.Inconsistent (u' : Theory (languageFinset u)) := Complete.inconsistent_of_unsatisfiable this
-  have : System.Inconsistent (u : Theory L) := by rw[←image_u']; simpa using Derivation.inconsistent_lMap L.ofSubLanguage this
-  have : System.Inconsistent (insert (∼∀∀φ) T) := this.of_supset ssu
+  have : Entailment.Inconsistent (u' : Theory (languageFinset u)) := Complete.inconsistent_of_unsatisfiable this
+  have : Entailment.Inconsistent (u : Theory L) := by rw[←image_u']; simpa using Derivation.inconsistent_lMap L.ofSubLanguage this
+  have : Entailment.Inconsistent (insert (∼∀∀φ) T) := this.of_supset ssu
   exact Derivation.provable_iff_inconsistent.mpr this
 
 theorem complete_iff : T ⊨ φ ↔ T ⊢! φ :=
   ⟨fun h ↦ complete h, sound!⟩
 
 instance (T : Theory L) : Complete T (Semantics.models (SmallStruc L) T) := ⟨complete⟩
 
-lemma satisfiable_of_consistent' (h : System.Consistent T) : Semantics.Satisfiable (SmallStruc L) T :=
+lemma satisfiable_of_consistent' (h : Entailment.Consistent T) : Semantics.Satisfiable (SmallStruc L) T :=
   Complete.satisfiable_of_consistent h
 
-lemma satisfiable_of_consistent (h : System.Consistent T) : Semantics.Satisfiable (Struc.{max u w} L) T := by
+lemma satisfiable_of_consistent (h : Entailment.Consistent T) : Semantics.Satisfiable (Struc.{max u w} L) T := by
   let ⟨M, _, _, h⟩ := satisfiable_iff.mp (satisfiable_of_consistent' h)
   exact satisfiable_iff.mpr ⟨ULift.{w} M, inferInstance, inferInstance, ((uLift_elementaryEquiv L M).modelsTheory).mpr h⟩
 
-lemma satisfiable_iff_consistent' : Semantics.Satisfiable (Struc.{max u w} L) T ↔ System.Consistent T :=
+lemma satisfiable_iff_consistent' : Semantics.Satisfiable (Struc.{max u w} L) T ↔ Entailment.Consistent T :=
   ⟨consistent_of_satidfiable, satisfiable_of_consistent.{u, w}⟩
 
-lemma satisfiable_iff_consistent : Satisfiable T ↔ System.Consistent T := satisfiable_iff_consistent'.{u, u}
+lemma satisfiable_iff_consistent : Satisfiable T ↔ Entailment.Consistent T := satisfiable_iff_consistent'.{u, u}
 
 lemma satidfiable_iff_satisfiable : Semantics.Satisfiable (Struc.{max u w} L) T ↔ Satisfiable T := by
   simp [satisfiable_iff_consistent'.{u, w}, satisfiable_iff_consistent]

Foundation/FirstOrder/Completeness/Corollaries.lean

@@ -6,12 +6,12 @@ namespace ModelsTheory
 
 variable {L : Language.{u}} (M : Type w) [Nonempty M] [Structure L M] (T U V : Theory L)
 
-lemma of_provably_subtheory (_ : T ≼ U) (h : M ⊧ₘ* U) : M ⊧ₘ* T := ⟨by
+lemma of_provably_subtheory [T ⪯ U] (h : M ⊧ₘ* U) : M ⊧ₘ* T := ⟨by
   intro φ hp
-  have : U ⊢ φ := System.Subtheory.prf (System.byAxm hp)
-  exact consequence_iff'.{u, w}.mp (sound! ⟨this⟩) M⟩
+  have : U ⊢! φ := (inferInstanceAs (T ⪯ U)).pbl (Entailment.by_axm _ hp)
+  exact consequence_iff'.{u, w}.mp (sound! this) M⟩
 
-lemma of_provably_subtheory' [T ≼ U] [M ⊧ₘ* U] : M ⊧ₘ* T := of_provably_subtheory M T U inferInstance inferInstance
+lemma of_provably_subtheory' [T ⪯ U] [M ⊧ₘ* U] : M ⊧ₘ* T := of_provably_subtheory M T U inferInstance
 
 lemma of_add_left [M ⊧ₘ* T + U] : M ⊧ₘ* T := of_ss inferInstance (show T ⊆ T + U from by simp [Theory.add_def])
 
@@ -23,7 +23,7 @@ lemma of_add_left_right [M ⊧ₘ* T + U + V] : M ⊧ₘ* U := @of_add_right _ M
 
 end ModelsTheory
 
-variable {L : Language.{u}} [L.Eq] {T : Theory L} [𝐄𝐐 ≼ T]
+variable {L : Language.{u}} [L.Eq] {T : Theory L} [𝐄𝐐 ⪯ T]
 
 lemma EQ.provOf (φ : SyntacticFormula L)
   (H : ∀ (M : Type (max u w))

Foundation/FirstOrder/Completeness/SearchTree.lean

@@ -7,7 +7,7 @@ namespace FirstOrder
 
 namespace Completeness
 
-open Semiformula Encodable System
+open Semiformula Encodable Entailment
 variable {L : Language.{u}}
 variable {T : Theory L} {Γ : Sequent L}
 

Foundation/FirstOrder/Hauptsatz.lean

@@ -356,7 +356,7 @@ end Forces
 
 noncomputable
 def main [L.DecidableEq] {Γ : Sequent L} : ⊢ᵀ Γ → {d : ⊢ᵀ Γ // Derivation.IsCutFree d} := fun d ↦
-  let d : 𝐌𝐢𝐧¹ ⊢ ⋀(∼Γ)ᴺ ➝ ⊥ := System.FiniteContext.toDef (Derivation.goedelGentzen d)
+  let d : 𝐌𝐢𝐧¹ ⊢ ⋀(∼Γ)ᴺ ➝ ⊥ := Entailment.FiniteContext.toDef (Derivation.goedelGentzen d)
   let ff : ∼Γ ⊩ ⋀(∼Γ)ᴺ ➝ ⊥ := Forces.ofMinimalProof d (∼Γ)
   let fc : ∼Γ ⊩ ⋀(∼Γ)ᴺ := Forces.conj' fun φ hφ ↦
     (Forces.refl φ).monotone (StrongerThan.ofSubset <| List.cons_subset.mpr ⟨hφ, by simp⟩)