modal

Foundation/Modal/Boxdot/Basic.lean

@@ -37,27 +37,27 @@ theorem boxdotTranslated
     dsimp only [BoxdotTranslation];
     trivial;
 
-lemma boxdotTranslatedK4_of_S4 : 𝐒𝟒 ⊢! φ → 𝐊𝟒 ⊢! φᵇ := boxdotTranslated $ by
+lemma boxdotTranslatedK4_of_S4 : (Hilbert.S4 α) ⊢! φ → (Hilbert.K4 α) ⊢! φᵇ := boxdotTranslated $ by
   intro φ hp;
   simp at hp;
   rcases hp with (⟨_, _, rfl⟩ | ⟨_, rfl⟩ | ⟨_, rfl⟩);
   . dsimp [BoxdotTranslation]; exact boxdot_axiomK!;
   . dsimp [BoxdotTranslation]; exact boxdot_axiomT!;
   . dsimp [BoxdotTranslation]; exact boxdot_axiomFour!
 
-lemma iff_boxdotTranslation_S4 : 𝐒𝟒 ⊢! φ ⭤ φᵇ := by
+lemma iff_boxdotTranslation_S4 : (Hilbert.S4 α) ⊢! φ ⭤ φᵇ := by
   induction φ using Formula.rec' with
   | hbox φ ihp => exact iff_trans''! (box_iff! ihp) iff_box_boxdot!;
   | himp φ ψ ihp ihq => exact imp_replace_iff! ihp ihq;
   | _ => exact iff_id!;
 
-lemma S4_of_boxdotTranslatedK4 (h : 𝐊𝟒 ⊢! φᵇ) : 𝐒𝟒 ⊢! φ := by
-  exact (and₂'! iff_boxdotTranslation_S4) ⨀ (weakerThan_iff.mp $ K4_weakerThan_S4) h
+lemma S4_of_boxdotTranslatedK4 (h : (Hilbert.K4 α) ⊢! φᵇ) : (Hilbert.S4 α) ⊢! φ := by
+  exact (and₂'! iff_boxdotTranslation_S4) ⨀ (weakerThan_iff.mp $ Hilbert.K4_weakerThan_S4) h
 
-theorem iff_S4_boxdotTranslatedK4 : 𝐒𝟒 ⊢! φ ↔ 𝐊𝟒 ⊢! φᵇ := by
+theorem iff_S4_boxdotTranslatedK4 : (Hilbert.S4 α) ⊢! φ ↔ (Hilbert.K4 α) ⊢! φᵇ := by
   constructor;
   . apply boxdotTranslatedK4_of_S4;
   . apply S4_of_boxdotTranslatedK4;
-instance : BoxdotProperty (𝐒𝟒 : Hilbert α) 𝐊𝟒 := ⟨iff_S4_boxdotTranslatedK4⟩
+instance : BoxdotProperty (Hilbert.S4 α) (Hilbert.K4 α) := ⟨iff_S4_boxdotTranslatedK4⟩
 
 end LO.Modal

Foundation/Modal/Boxdot/GL_Grz.lean

@@ -105,13 +105,13 @@ variable {φ : Formula α}
 
 open Formula (BoxdotTranslation)
 open System in
-lemma boxdotTranslatedGL_of_Grz : 𝐆𝐫𝐳 ⊢! φ → 𝐆𝐋 ⊢! φᵇ := boxdotTranslated $ by
+lemma boxdotTranslatedGL_of_Grz : (Hilbert.Grz α) ⊢! φ → (Hilbert.GL α) ⊢! φᵇ := boxdotTranslated $ by
   intro φ hp;
   rcases hp with (⟨_, _, rfl⟩ | ⟨_, rfl⟩);
   . dsimp [BoxdotTranslation]; exact boxdot_axiomK!;
   . dsimp [BoxdotTranslation]; exact boxdot_Grz_of_L!
 
-lemma Grz_of_boxdotTranslatedGL [Inhabited α] : 𝐆𝐋 ⊢! φᵇ → 𝐆𝐫𝐳 ⊢! φ := by
+lemma Grz_of_boxdotTranslatedGL [Inhabited α] : (Hilbert.GL α) ⊢! φᵇ → (Hilbert.Grz α) ⊢! φ := by
   contrapose;
   intro h;
   apply (not_imp_not.mpr $ Kripke.GL_finite_sound.sound);
@@ -134,11 +134,11 @@ lemma Grz_of_boxdotTranslatedGL [Inhabited α] : 𝐆𝐋 ⊢! φᵇ → 𝐆
     use V, x;
     exact iff_reflexivize_irreflexivize FF_refl |>.not.mp h;
 
-theorem iff_Grz_boxdotTranslatedGL [Inhabited α] : 𝐆𝐫𝐳 ⊢! φ ↔ 𝐆𝐋 ⊢! φᵇ := by
+theorem iff_Grz_boxdotTranslatedGL [Inhabited α] : (Hilbert.Grz α) ⊢! φ ↔ (Hilbert.GL α) ⊢! φᵇ := by
   constructor;
   . apply boxdotTranslatedGL_of_Grz;
   . apply Grz_of_boxdotTranslatedGL;
 
-instance [Inhabited α] : BoxdotProperty (α := α) 𝐆𝐫𝐳 𝐆𝐋 := ⟨iff_Grz_boxdotTranslatedGL⟩
+instance [Inhabited α] : BoxdotProperty (Hilbert.Grz α) (Hilbert.GL α) := ⟨iff_Grz_boxdotTranslatedGL⟩
 
 end LO.Modal

Foundation/Modal/Geach.lean

@@ -50,8 +50,7 @@ lemma dense_def : Dense R ↔ (GeachConfluent ⟨0, 1, 2, 0⟩ R) := by
   . rintro h x y z rfl Rxz; exact h Rxz;
   . intro h x y Rxy; exact h rfl Rxy;
 
-@[simp]
-lemma satisfies_eq : GeachConfluent (α := α) t (· = ·) := by simp [GeachConfluent];
+@[simp] lemma satisfies_eq : GeachConfluent (α := α) t (· = ·) := by simp [GeachConfluent];
 
 end GeachConfluent
 
@@ -144,44 +143,43 @@ variable {Ax : Theory α}
 
 open System
 
-protected abbrev Geach (l : List GeachTaple) : Hilbert α := 𝜿(𝗚𝗲(l))
-notation "𝐆𝐞(" l ")" => Modal.Geach l
+protected abbrev Hilbert.Geach (α) (l : List GeachTaple) : Hilbert α := Hilbert.ExtK (𝗚𝗲(l))
 
 namespace Geach
 
 end Geach
 
 protected class Hilbert.IsGeach (L : Hilbert α) (ts : List GeachTaple) where
-  char : L = 𝐆𝐞(ts) := by aesop;
+  char : L = Hilbert.Geach _ ts := by aesop;
 
 attribute [simp] Hilbert.IsGeach.char
 
 namespace IsGeach
 
 lemma ax {Λ : Hilbert α} [geach : Λ.IsGeach ts] : Λ.axioms = (𝗞 ∪ 𝗚𝗲(ts)) := by
   have e := geach.char;
-  simp [Modal.Geach] at e;
+  simp [Hilbert.Geach] at e;
   simp_all;
 
-instance : 𝐊.IsGeach (α := α) [] where
+instance : (Hilbert.K α).IsGeach [] where
 
-instance : 𝐊𝐃.IsGeach (α := α) [⟨0, 0, 1, 1⟩] where
+instance : (Hilbert.KD α).IsGeach [⟨0, 0, 1, 1⟩] where
 
-instance : 𝐊𝐓.IsGeach (α := α) [⟨0, 0, 1, 0⟩] where
+instance : (Hilbert.KT α).IsGeach [⟨0, 0, 1, 0⟩] where
 
-instance : 𝐊𝐓𝐁.IsGeach (α := α) [⟨0, 0, 1, 0⟩, ⟨0, 1, 0, 1⟩] where
+instance : (Hilbert.KTB α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 1, 0, 1⟩] where
 
-instance : 𝐊𝟒.IsGeach (α := α) [⟨0, 2, 1, 0⟩] where
+instance : (Hilbert.K4 α).IsGeach [⟨0, 2, 1, 0⟩] where
 
-instance : 𝐒𝟒.IsGeach (α := α) [⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩] where
+instance : (Hilbert.S4 α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩] where
 
-instance : 𝐒𝟒.𝟐.IsGeach (α := α) [⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩, ⟨1, 1, 1, 1⟩] where
+instance : (Hilbert.S4Dot2 α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩, ⟨1, 1, 1, 1⟩] where
 
-instance : 𝐒𝟓.IsGeach (α := α) [⟨0, 0, 1, 0⟩, ⟨1, 1, 0, 1⟩] where
+instance : (Hilbert.S5 α).IsGeach [⟨0, 0, 1, 0⟩, ⟨1, 1, 0, 1⟩] where
 
-instance : 𝐊𝐓𝟒𝐁.IsGeach (α := α) [⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩, ⟨0, 1, 0, 1⟩] where
+instance : (Hilbert.KT4B α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩, ⟨0, 1, 0, 1⟩] where
 
-instance : 𝐓𝐫𝐢𝐯.IsGeach (α := α) [⟨0, 0, 1, 0⟩, ⟨0, 1, 0, 0⟩] where
+instance : (Hilbert.Triv α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 1, 0, 0⟩] where
 
 end IsGeach