Add Trivial Modal Logics, Empty and Univ (#205)

* Add trivial modal logics

* refactor

* refct

Foundation.lean

@@ -100,3 +100,4 @@ import Foundation.Modal.Boxdot.GL_Grz
 import Foundation.Modal.Logic.WellKnown
 import Foundation.Modal.Logic.Extension
 import Foundation.Modal.Logic.Sublogic
+import Foundation.Modal.Logic.Trivials

Foundation/Modal/Logic/Basic.lean

@@ -19,16 +19,21 @@ protected class Unnecessitation (L : Logic) where
 protected class ModalDisjunctive (L : Logic) where
   modal_disjunctive_closed {φ ψ} : □φ ⋎ □ψ ∈ L → φ ∈ L ∨ ψ ∈ L
 
-class QuasiNormal (L : Logic) where
+protected class QuasiNormal (L : Logic) where
   subset_K : Logic.K ⊆ L
   mdp_closed {φ ψ} : φ ➝ ψ ∈ L → φ ∈ L → ψ ∈ L
   subst_closed {φ} : φ ∈ L → ∀ s, φ⟦s⟧ ∈ L
 
-class Normal (L : Logic) extends L.QuasiNormal where
+protected class Normal (L : Logic) extends L.QuasiNormal where
   nec_closed {φ} : φ ∈ L → □φ ∈ L
 
-end Logic
+class Sublogic (L₁ L₂ : Logic) where
+  subset : L₁ ⊆ L₂
+
+class ProperSublogic (L₁ L₂ : Logic) : Prop where
+  ssubset : L₁ ⊂ L₂
 
+end Logic
 
 namespace Hilbert
 
@@ -59,10 +64,9 @@ instance [Entailment.Unnecessitation H] : H.logic.Unnecessitation := ⟨fun {_}
 
 instance [Entailment.ModalDisjunctive H] : H.logic.ModalDisjunctive := ⟨fun {_ _} h => modal_disjunctive h⟩
 
-end Hilbert
-
 instance : (Logic.K).Normal := Hilbert.normal
 
+end Hilbert
 
 
 section

Foundation/Modal/Logic/Sublogic.lean

@@ -7,12 +7,6 @@ open Formula
 open Entailment
 open Kripke
 
-class Sublogic (L₁ L₂ : Logic) where
-  subset : L₁ ⊆ L₂
-
-class ProperSublogic (L₁ L₂ : Logic) where
-  ssubset : L₁ ⊂ L₂
-
 theorem KTB_ssubset_S5 : Logic.KTB ⊂ Logic.S5 := by
   constructor;
   . rw [KTB.eq_ReflexiveSymmetricKripkeFrameClass_Logic, S5.eq_ReflexiveEuclideanKripkeFrameClass_Logic];
@@ -775,4 +769,5 @@ theorem K_ssubset_KH : Logic.K ⊂ Logic.KH := by
       constructor <;> tauto;
 instance : ProperSublogic Logic.K Logic.KH := ⟨K_ssubset_KH⟩
 
+
 end LO.Modal.Logic

Foundation/Modal/Logic/Trivials.lean

@@ -0,0 +1,34 @@
+import Foundation.Modal.Logic.WellKnown
+import Batteries.Tactic.Instances
+
+namespace LO.Modal.Logic
+
+protected abbrev Empty : Logic := ∅
+
+protected abbrev Univ : Logic := Set.univ
+
+instance : ProperSublogic Logic.Empty Logic.K := ⟨by
+  constructor;
+  . simp;
+  . suffices ∃ φ, Hilbert.K ⊢! φ by tauto_set;
+    use ⊤;
+    simp;
+⟩
+
+instance : ProperSublogic Logic.Triv Logic.Univ := ⟨by
+  constructor;
+  . simp;
+  . suffices ∃ φ, ¬Hilbert.Triv ⊢! φ by tauto_set;
+    use ⊥;
+    exact Hilbert.Triv.Kripke.consistent.not_bot;
+⟩
+
+instance : ProperSublogic Logic.Ver Logic.Univ := ⟨by
+  constructor;
+  . simp;
+  . suffices ∃ φ, ¬Hilbert.Ver ⊢! φ by tauto_set;
+    use ⊥;
+    exact Hilbert.Ver.Kripke.consistent.not_bot;
+⟩
+
+end LO.Modal.Logic