add(Modal): GL + □^[n]⊥ provable equivalent to GL (#513)

Author: SnO2WMaN

Foundation/Modal/Logic/GLPlusBoxBot/Basic.lean

@@ -1,7 +1,7 @@
 import Foundation.Modal.Logic.Extension
 import Foundation.Modal.Maximal.Unprovability
 import Mathlib.Data.ENat.Basic
-
+import Foundation.Modal.Kripke.Logic.GL.Completeness
 
 namespace LO.Modal.Axioms
 
@@ -15,6 +15,9 @@ protected abbrev BoxBot (n : ℕ∞) : F :=
 @[simp]
 lemma BoxBot.eq_omega : (Axioms.BoxBot ⊤ : F) = ⊤ := rfl
 
+@[simp]
+lemma BoxBot.subst {s : Substitution α} : (Axioms.BoxBot n)⟦s⟧ = (Axioms.BoxBot n) := by cases n <;> simp;
+
 end LO.Modal.Axioms
 
 
@@ -34,23 +37,28 @@ instance : Modal.GL ⪯ Modal.GLPlusBoxBot n := by
   dsimp [Modal.GLPlusBoxBot];
   infer_instance;
 
-lemma Logic.GLPlusBoxBot.boxbot : (Modal.Axioms.BoxBot n) ∈ Modal.GLPlusBoxBot n := by
-  apply Logic.sumQuasiNormal.mem₂;
+@[simp]
+lemma Logic.GLPlusBoxBot.boxbot : Modal.GLPlusBoxBot n ⊢! (Modal.Axioms.BoxBot n) := by
+  apply Logic.sumQuasiNormal.mem₂!;
   tauto;
 
-@[simp]
-lemma GLPlusBoxBot.eq_omega : (Modal.GLPlusBoxBot ⊤ : Logic ℕ) = Modal.GL := by
-  ext φ;
-  suffices Modal.GLPlusBoxBot ⊤ ⊢! φ ↔ Modal.GL ⊢! φ by simpa;
+lemma iff_provable_GLBB_provable_GL {n : ℕ∞} {φ} : Modal.GLPlusBoxBot n ⊢! φ ↔ Modal.GL ⊢! (Modal.Axioms.BoxBot n) ➝ φ := by
   constructor;
   . intro h;
     induction h using sumQuasiNormal.rec! with
-    | mem₁ h => assumption;
+    | mem₁ h => cl_prover [h]
     | mem₂ h => simp_all;
-    | mdp ihφψ ihφ => exact ihφψ ⨀ ihφ;
-    | subst => apply Logic.subst!; assumption;
+    | mdp ihφψ ihφ => cl_prover [ihφψ, ihφ];
+    | subst ihφ => simpa using Logic.subst! _ ihφ;
   . intro h;
-    apply sumQuasiNormal.mem₁!;
-    assumption;
+    replace h : Modal.GLPlusBoxBot n ⊢! (Modal.Axioms.BoxBot n) ➝ φ := sumQuasiNormal.mem₁! h;
+    exact h ⨀ Logic.GLPlusBoxBot.boxbot;
+
+@[simp]
+lemma eq_GLBB_omega_GL : (Modal.GLPlusBoxBot ⊤ : Logic ℕ) = Modal.GL := by
+  ext φ;
+  suffices Modal.GLPlusBoxBot ⊤ ⊢! φ ↔ Modal.GL ⊢! φ by simpa;
+  apply Iff.trans iff_provable_GLBB_provable_GL;
+  constructor <;> . intro h; cl_prover [h];
 
 end LO.Modal