rebase fix

Logic/Modal/Normal/Deduction.lean

@@ -42,9 +42,8 @@ notation:45 Γ " ⊢ᴹ[" Λ "]! " p => Deducible Λ Γ p
 abbrev Undeducible := ¬(Γ ⊢ᴹ[Λ]! p)
 notation:45 Γ " ⊬ᴹ[" Λ "]! " p => Undeducible Λ Γ p
 
-abbrev Theory.Consistent := Hilbert.Consistent (@Deduction α Λ) Γ
-
-abbrev Theory.Inconsistent := Hilbert.Inconsistent (@Deduction α Λ) Γ
+abbrev Theory.Consistent := Deduction.Consistent (@Deduction α Λ) Γ
+abbrev Theory.Inconsistent := Deduction.Inconsistent (@Deduction α Λ) Γ
 
 namespace Deduction
 

Logic/Modal/Normal/Semantics.lean

@@ -157,18 +157,6 @@ notation w "⊮ᴹ[" M "] " Γ => Theory.Unsatisfies M w Γ
 
 variable [DecidableEq β]
 
-variable [DecidableEq β]
-
-lemma Theory.satisfies_conj {Δ : Context β} {Γ : Theory β} (hs : ↑Δ ⊆ Γ) {M : Model α β} {w : α} : (w ⊩ᴹ[M] Γ) → (w ⊩ᴹ[M] Δ.conj) := by
-  intro hΓ;
-  induction Δ using Finset.induction_on with
-  | empty => simp [Finset.conj];
-  | @insert p Δ _ ih =>
-    -- have := Finset.toList_insert h;
-    -- simp [Finset.conj] at this;
-    suffices w ⊩ᴹ[M] (Δ.conj ⋏ p) by simpa [←Context.insert_conj] using this;
-    simp_all [Finset.coe_insert, Set.insert_subset_iff];
-
 @[simp]
 def Theory.Models (M : Model α β) (Γ : Theory β) := ∀ p ∈ Γ, ⊧ᴹ[M] p
 notation "⊧ᴹ[" M "] " Γ => Theory.Models M Γ