From 4049921c179ecec13b7b6c01f06010b363057d62 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 8 Nov 2024 02:24:19 +0900 Subject: [PATCH] modal --- Foundation/Modal/Boxdot/Basic.lean | 12 +- Foundation/Modal/Boxdot/GL_Grz.lean | 8 +- Foundation/Modal/Geach.lean | 30 +- Foundation/Modal/Hilbert.lean | 277 ++++++++---------- Foundation/Modal/Kripke/Completeness.lean | 4 +- Foundation/Modal/Kripke/Dot3.lean | 8 +- Foundation/Modal/Kripke/Filteration.lean | 16 +- Foundation/Modal/Kripke/GL/Completeness.lean | 36 +-- Foundation/Modal/Kripke/GL/Definability.lean | 6 +- Foundation/Modal/Kripke/GL/MDP.lean | 14 +- Foundation/Modal/Kripke/GL/Tree.lean | 16 +- Foundation/Modal/Kripke/Geach.lean | 72 ++--- Foundation/Modal/Kripke/Grz/Completeness.lean | 58 ++-- Foundation/Modal/Kripke/Grz/Definability.lean | 6 +- Foundation/Modal/Kripke/S5.lean | 2 +- Foundation/Modal/Kripke/Semantics.lean | 52 ++-- Foundation/Modal/Kripke/Ver.lean | 12 +- Foundation/Modal/Maximal.lean | 41 +-- Foundation/Modal/ModalCompanion/Basic.lean | 2 +- Foundation/Modal/ModalCompanion/GMT.lean | 6 +- Foundation/Modal/PLoN/Completeness.lean | 2 +- Foundation/Modal/PLoN/Semantics.lean | 2 +- Foundation/Modal/PLoN/Soundness.lean | 4 +- 23 files changed, 321 insertions(+), 365 deletions(-) diff --git a/Foundation/Modal/Boxdot/Basic.lean b/Foundation/Modal/Boxdot/Basic.lean index 2fa4921d..9f591467 100644 --- a/Foundation/Modal/Boxdot/Basic.lean +++ b/Foundation/Modal/Boxdot/Basic.lean @@ -37,7 +37,7 @@ 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⟩); @@ -45,19 +45,19 @@ lemma boxdotTranslatedK4_of_S4 : 𝐒𝟒 ⊢! φ → 𝐊𝟒 ⊢! φᵇ := box . 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 diff --git a/Foundation/Modal/Boxdot/GL_Grz.lean b/Foundation/Modal/Boxdot/GL_Grz.lean index d87d4d6d..9cad0390 100644 --- a/Foundation/Modal/Boxdot/GL_Grz.lean +++ b/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 diff --git a/Foundation/Modal/Geach.lean b/Foundation/Modal/Geach.lean index 1e0defa6..c2f3d81a 100644 --- a/Foundation/Modal/Geach.lean +++ b/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,15 +143,14 @@ 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 @@ -160,28 +158,28 @@ 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 diff --git a/Foundation/Modal/Hilbert.lean b/Foundation/Modal/Hilbert.lean index 8ceba203..dc82a9af 100644 --- a/Foundation/Modal/Hilbert.lean +++ b/Foundation/Modal/Hilbert.lean @@ -173,174 +173,160 @@ macro_rules | `(tactic| trivial) => `(tactic | apply dne!) end Deduction -abbrev Hilbert.theorems (Λ : Hilbert α) := System.theory Λ +namespace Hilbert + +abbrev theorems (Λ : Hilbert α) := System.theory Λ + +section K + +variable (α) protected abbrev K : Hilbert α := ⟨𝗞, ⟮Nec⟯⟩ -notation "𝐊" => Modal.K -instance : 𝐊.IsNormal (α := α) where +instance : (Hilbert.K α).IsNormal where -abbrev ExtK (Ax : Theory α) : Hilbert α := ⟨𝗞 ∪ Ax, ⟮Nec⟯⟩ -prefix:max "𝜿" => ExtK -instance : (𝜿Ax).IsNormal (α := α) where +end K -lemma K_is_extK_of_empty : (𝐊 : Hilbert α) = 𝜿∅ := by aesop; -lemma K_is_extK_of_AxiomK : (𝐊 : Hilbert α) = 𝜿𝗞 := by aesop; +section K_extension -namespace Normal +protected abbrev ExtK (Ax : Theory α) : Hilbert α := ⟨𝗞 ∪ Ax, ⟮Nec⟯⟩ +instance : (Hilbert.ExtK Ax).IsNormal where -open System +namespace ExtK -variable {Ax : Theory α} +lemma K_is_extK_of_empty : (Hilbert.K α) = (Hilbert.ExtK ∅) := by aesop; -lemma def_ax : (𝜿Ax).axioms = (𝗞 ∪ Ax) := by simp; +lemma K_is_extK_of_AxiomK : (Hilbert.K α) = (Hilbert.ExtK 𝗞) := by aesop; -lemma maxm! (h : φ ∈ Ax) : 𝜿Ax ⊢! φ := ⟨Deduction.maxm (by simp [def_ax]; right; assumption)⟩ +lemma def_ax : (Hilbert.ExtK Ax).axioms = (𝗞 ∪ Ax) := rfl -end Normal +lemma maxm! (h : φ ∈ Ax) : (Hilbert.ExtK Ax) ⊢! φ := ⟨Deduction.maxm (by simp [Hilbert.ExtK]; tauto)⟩ +end ExtK + +end K_extension --- tools of Modal Companion -section -abbrev ExtS4 (Ax : Theory α) : Hilbert α := 𝜿(𝗧 ∪ 𝟰 ∪ Ax) -prefix:max "𝝈" => ExtS4 -instance : System.S4 (𝝈Ax) where +section S4_extension + +protected abbrev ExtS4 (Ax : Theory α) : Hilbert α := Hilbert.ExtK (𝗧 ∪ 𝟰 ∪ Ax) +instance : System.S4 (Hilbert.ExtS4 Ax) where T _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) Four _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -@[simp] lemma ExtS4.def_ax : (𝝈Ax).axioms = (𝗞 ∪ 𝗧 ∪ 𝟰 ∪ Ax) := by aesop; +@[simp] lemma ExtS4.def_ax : (Hilbert.ExtS4 Ax).axioms = (𝗞 ∪ 𝗧 ∪ 𝟰 ∪ Ax) := by aesop; -end +end S4_extension -protected abbrev KT : Hilbert α := 𝜿(𝗧) -notation "𝐊𝐓" => Modal.KT -instance : System.KT (𝐊𝐓 : Hilbert α) where +section systems + +variable (α) + +protected abbrev KT : Hilbert α := Hilbert.ExtK $ 𝗧 +instance : System.KT (Hilbert.KT α) where T _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -protected abbrev KB : Hilbert α := 𝜿(𝗕) -notation "𝐊𝐁" => Modal.KB -instance : System.KB (𝐊𝐁 : Hilbert α) where +protected abbrev KB : Hilbert α := Hilbert.ExtK $ 𝗕 +instance : System.KB (Hilbert.KB α) where B _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -protected abbrev KD : Hilbert α := 𝜿(𝗗) -notation "𝐊𝐃" => Modal.KD -instance : System.KD (𝐊𝐃 : Hilbert α) where +protected abbrev KD : Hilbert α := Hilbert.ExtK $ 𝗗 +instance : System.KD (Hilbert.KD α) where D _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -protected abbrev KP : Hilbert α := 𝜿(𝗣) -notation "𝐊𝐏" => Modal.KP -instance : System.KP (𝐊𝐏 : Hilbert α) where +protected abbrev KP : Hilbert α := Hilbert.ExtK $ 𝗣 +instance : System.KP (Hilbert.KP α) where P := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -protected abbrev KTB : Hilbert α := 𝜿(𝗧 ∪ 𝗕) -notation "𝐊𝐓𝐁" => Modal.KTB +protected abbrev KTB : Hilbert α := Hilbert.ExtK $ 𝗧 ∪ 𝗕 -protected abbrev K4 : Hilbert α := 𝜿(𝟰) -notation "𝐊𝟒" => Modal.K4 -instance : System.K4 (𝐊𝟒 : Hilbert α) where +protected abbrev K4 : Hilbert α := Hilbert.ExtK $ 𝟰 +instance : System.K4 (Hilbert.K4 α) where Four _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -protected abbrev K5 : Hilbert α := 𝜿(𝟱) -notation "𝐊𝟓" => Modal.K5 -instance : System.K5 (𝐊𝟓 : Hilbert α) where +protected abbrev K5 : Hilbert α := Hilbert.ExtK $ 𝟱 +instance : System.K5 (Hilbert.K5 α) where Five _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -protected abbrev S4 : Hilbert α := 𝝈(∅) -notation "𝐒𝟒" => Modal.S4 -instance : System.S4 (𝐒𝟒 : Hilbert α) where +protected abbrev S4 : Hilbert α := Hilbert.ExtS4 $ ∅ +instance : System.S4 (Hilbert.S4 α) where T _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) Four _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -protected abbrev S4Dot2 : Hilbert α := 𝝈(.𝟮) -notation "𝐒𝟒.𝟐" => Modal.S4Dot2 +protected abbrev S4Dot2 : Hilbert α := Hilbert.ExtS4 $ .𝟮 -protected abbrev S4Dot3 : Hilbert α := 𝝈(.𝟯) -notation "𝐒𝟒.𝟑" => Modal.S4Dot3 +protected abbrev S4Dot3 : Hilbert α := Hilbert.ExtS4 $ .𝟯 -protected abbrev S4Grz : Hilbert α := 𝝈(𝗚𝗿𝘇) -- S4 + 𝗚𝗿𝘇 -notation "𝐒𝟒𝐆𝐫𝐳" => Modal.S4Grz +protected abbrev S4Grz : Hilbert α := Hilbert.ExtS4 $ 𝗚𝗿𝘇 -protected abbrev KT4B : Hilbert α := 𝝈(𝗕) -notation "𝐊𝐓𝟒𝐁" => Modal.KT4B +protected abbrev KT4B : Hilbert α := Hilbert.ExtS4 $ 𝗕 -protected abbrev S5 : Hilbert α := 𝜿(𝗧 ∪ 𝟱) -notation "𝐒𝟓" => Modal.S5 -instance : System.S5 (𝐒𝟓 : Hilbert α) where +protected abbrev S5 : Hilbert α := Hilbert.ExtK $ 𝗧 ∪ 𝟱 +instance : System.S5 (Hilbert.S5 α) where T _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) Five _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -protected abbrev S5Grz : Hilbert α := 𝜿(𝗧 ∪ 𝟱 ∪ 𝗚𝗿𝘇) -- 𝐒𝟓 + 𝗚𝗿𝘇 -notation "𝐒𝟓𝐆𝐫𝐳" => Modal.S5Grz -instance : System.S5Grz (𝐒𝟓𝐆𝐫𝐳 : Hilbert α) where +protected abbrev S5Grz : Hilbert α := Hilbert.ExtK $ 𝗧 ∪ 𝟱 ∪ 𝗚𝗿𝘇 +instance : System.S5Grz (Hilbert.S5Grz α) where T _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) Five _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) Grz _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -protected abbrev Triv : Hilbert α := 𝜿(𝗧 ∪ 𝗧𝗰) -notation "𝐓𝐫𝐢𝐯" => Modal.Triv -instance : System.Triv (𝐓𝐫𝐢𝐯 : Hilbert α) where +protected abbrev Triv : Hilbert α := Hilbert.ExtK $ 𝗧 ∪ 𝗧𝗰 +instance : System.Triv (Hilbert.Triv α) where T _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) Tc _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -protected abbrev Ver : Hilbert α := 𝜿(𝗩𝗲𝗿) -notation "𝐕𝐞𝐫" => Modal.Ver -instance : System.Ver (𝐕𝐞𝐫 : Hilbert α) where +protected abbrev Ver : Hilbert α := Hilbert.ExtK $ 𝗩𝗲𝗿 +instance : System.Ver (Hilbert.Ver α) where Ver _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -protected abbrev GL : Hilbert α := 𝜿(𝗟) -notation "𝐆𝐋" => Modal.GL -instance : System.GL (𝐆𝐋 : Hilbert α) where +protected abbrev GL : Hilbert α := Hilbert.ExtK $ 𝗟 +instance : System.GL (Hilbert.GL α) where L _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -protected abbrev Grz : Hilbert α := 𝜿(𝗚𝗿𝘇) -notation "𝐆𝐫𝐳" => Modal.Grz -instance : System.Grz (𝐆𝐫𝐳 : Hilbert α) where +protected abbrev Grz : Hilbert α := Hilbert.ExtK $ 𝗚𝗿𝘇 +instance : System.Grz (Hilbert.Grz α) where Grz _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) -protected abbrev K4H : Hilbert α := 𝜿(𝟰 ∪ 𝗛) -notation "𝐊𝟒𝐇" => Modal.K4H -instance : System.K4H (𝐊𝟒𝐇 : Hilbert α) where +protected abbrev K4H : Hilbert α := Hilbert.ExtK $ 𝟰 ∪ 𝗛 +instance : System.K4H (Hilbert.K4H α) where Four _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) H _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) --- Non-normal modal logic - protected abbrev K4Loeb : Hilbert α := ⟨𝗞 ∪ 𝟰, ⟮Nec⟯ ∪ ⟮Loeb⟯⟩ -notation "𝐊𝟒(𝐋)" => Modal.K4Loeb -instance : 𝐊𝟒(𝐋).HasAxiomK (α := α) where -instance : 𝐊𝟒(𝐋).HasNecessitation (α := α) where -instance : 𝐊𝟒(𝐋).HasLoebRule (α := α) where -instance : System.K4Loeb (𝐊𝟒(𝐋) : Hilbert α) where +instance : (Hilbert.K4Loeb α).HasAxiomK where +instance : (Hilbert.K4Loeb α).HasNecessitation where +instance : (Hilbert.K4Loeb α).HasLoebRule where +instance : System.K4Loeb (Hilbert.K4Loeb α) where Four _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) protected abbrev K4Henkin : Hilbert α := ⟨𝗞 ∪ 𝟰, ⟮Nec⟯ ∪ ⟮Henkin⟯⟩ -notation "𝐊𝟒(𝐇)" => Modal.K4Henkin -instance : 𝐊𝟒(𝐇).HasAxiomK (α := α) where -instance : 𝐊𝟒(𝐇).HasNecessitation (α := α) where -instance : 𝐊𝟒(𝐇).HasHenkinRule (α := α) where -instance : System.K4Henkin (𝐊𝟒(𝐇) : Hilbert α) where +instance : (Hilbert.K4Henkin α).HasAxiomK where +instance : (Hilbert.K4Henkin α).HasNecessitation where +instance : (Hilbert.K4Henkin α).HasHenkinRule where +instance : System.K4Henkin (Hilbert.K4Henkin α) where Four _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) /-- Solovey's Provability Logic of True Arithmetic. Remark necessitation is *not* permitted. -/ -protected abbrev GLS : Hilbert α := ⟨𝐆𝐋.theorems ∪ 𝗧, ∅⟩ -notation "𝐆𝐋𝐒" => Modal.GLS -instance : System.HasAxiomK (𝐆𝐋𝐒 : Hilbert α) where +protected abbrev GLS : Hilbert α := ⟨(Hilbert.GL α).theorems ∪ 𝗧, ∅⟩ +instance : System.HasAxiomK (Hilbert.GLS α) where K _ _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) $ by simp [Hilbert.theorems, System.theory, System.axiomK!]; -instance : System.HasAxiomL (𝐆𝐋𝐒 : Hilbert α) where +instance : System.HasAxiomL (Hilbert.GLS α) where L _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) $ by simp [Hilbert.theorems, System.theory, System.axiomK!]; -instance : System.HasAxiomT (𝐆𝐋𝐒 : Hilbert α) where +instance : System.HasAxiomT (Hilbert.GLS α) where T _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp) /-- Logic of Pure Necessitation -/ protected abbrev N : Hilbert α := ⟨∅, ⟮Nec⟯⟩ -notation "𝐍" => Modal.N -instance : 𝐍.HasNecOnly (α := α) where +instance : (Hilbert.N α).HasNecOnly where + +end systems section @@ -366,71 +352,50 @@ lemma normal_weakerThan_of_subset {Λ₁ Λ₂ : Hilbert α} [Λ₁.IsNormal] [ intro φ hp; exact ⟨Deduction.maxm $ hSubset hp⟩; -lemma K_weakerThan_KD : (𝐊 : Hilbert α) ≤ₛ 𝐊𝐃 := normal_weakerThan_of_subset $ by aesop; -lemma K_weakerThan_KB : (𝐊 : Hilbert α) ≤ₛ 𝐊𝐁 := normal_weakerThan_of_subset $ by aesop; +lemma K_weakerThan_KD : (Hilbert.K α) ≤ₛ (Hilbert.KD α) := normal_weakerThan_of_subset $ by aesop; -lemma K_weakerThan_KT : (𝐊 : Hilbert α) ≤ₛ 𝐊𝐓 := normal_weakerThan_of_subset $ by aesop; +lemma K_weakerThan_KB : (Hilbert.K α) ≤ₛ (Hilbert.KB α) := normal_weakerThan_of_subset $ by aesop; -lemma K_weakerThan_K4 : (𝐊 : Hilbert α) ≤ₛ 𝐊𝟒 := normal_weakerThan_of_subset $ by aesop; +lemma K_weakerThan_KT : (Hilbert.K α) ≤ₛ (Hilbert.KT α) := normal_weakerThan_of_subset $ by aesop; -lemma K_weakerThan_K5 : (𝐊 : Hilbert α) ≤ₛ 𝐊𝟓 := normal_weakerThan_of_subset $ by aesop; +lemma K_weakerThan_K4 : (Hilbert.K α) ≤ₛ (Hilbert.K4 α) := normal_weakerThan_of_subset $ by aesop; -lemma KT_weakerThan_S4 : (𝐊𝐓 : Hilbert α) ≤ₛ 𝐒𝟒 := normal_weakerThan_of_subset $ by intro; aesop; +lemma K_weakerThan_K5 : (Hilbert.K α) ≤ₛ (Hilbert.K5 α) := normal_weakerThan_of_subset $ by aesop; -lemma K4_weakerThan_S4 : (𝐊𝟒 : Hilbert α) ≤ₛ 𝐒𝟒 := normal_weakerThan_of_subset $ by intro; aesop; +lemma KT_weakerThan_S4 : (Hilbert.KT α) ≤ₛ (Hilbert.S4 α) := normal_weakerThan_of_subset $ by intro; aesop; -lemma S4_weakerThan_S4Dot2 : (𝐒𝟒 : Hilbert α) ≤ₛ 𝐒𝟒.𝟐 := normal_weakerThan_of_subset $ by intro; aesop; +lemma K4_weakerThan_S4 : (Hilbert.K4 α) ≤ₛ (Hilbert.S4 α) := normal_weakerThan_of_subset $ by intro; aesop; -lemma S4_weakerThan_S4Dot3 : (𝐒𝟒 : Hilbert α) ≤ₛ 𝐒𝟒.𝟑 := normal_weakerThan_of_subset $ by intro; aesop; +lemma S4_weakerThan_S4Dot2 : (Hilbert.S4 α) ≤ₛ (Hilbert.S4Dot2 α) := normal_weakerThan_of_subset $ by intro; aesop; -lemma S4_weakerThan_S4Grz : (𝐒𝟒 : Hilbert α) ≤ₛ 𝐒𝟒𝐆𝐫𝐳 := normal_weakerThan_of_subset $ by intro; aesop; +lemma S4_weakerThan_S4Dot3 : (Hilbert.S4 α) ≤ₛ (Hilbert.S4Dot3 α) := normal_weakerThan_of_subset $ by intro; aesop; -lemma K_weakerThan_GL : (𝐊 : Hilbert α) ≤ₛ 𝐆𝐋 := normal_weakerThan_of_subset $ by intro; aesop; +lemma S4_weakerThan_S4Grz : (Hilbert.S4 α) ≤ₛ (Hilbert.S4Grz α) := normal_weakerThan_of_subset $ by intro; aesop; -lemma K4_weakerThan_Triv : (𝐊𝟒 : Hilbert α) ≤ₛ 𝐓𝐫𝐢𝐯 := by - apply normal_weakerThan_of_maxm; - intro φ hp; - rcases hp with (hK | hFour) - . obtain ⟨_, _, rfl⟩ := hK; exact axiomK!; - . obtain ⟨_, _, rfl⟩ := hFour; exact axiomFour!; +lemma K_weakerThan_GL : (Hilbert.K α) ≤ₛ (Hilbert.GL α) := normal_weakerThan_of_subset $ by intro; aesop; -lemma K4_weakerThan_GL : (𝐊𝟒 : Hilbert α) ≤ₛ 𝐆𝐋 := by - apply normal_weakerThan_of_maxm; - intro φ hp; - rcases hp with (hK | hFour) - . obtain ⟨_, _, rfl⟩ := hK; exact axiomK!; - . obtain ⟨_, _, rfl⟩ := hFour; exact axiomFour!; +lemma K4_weakerThan_Triv : (Hilbert.K4 α) ≤ₛ (Hilbert.Triv α) := normal_weakerThan_of_maxm $ by + rintro φ (⟨_, _, rfl⟩ | ⟨_, _, rfl⟩) <;> simp; -lemma KT_weakerThan_Grz : (𝐊𝐓 : Hilbert α) ≤ₛ 𝐆𝐫𝐳 := by - apply normal_weakerThan_of_maxm; - intro φ hp; - rcases hp with (hK | hGrz) - . obtain ⟨_, _, rfl⟩ := hK; exact axiomK!; - . obtain ⟨_, _, rfl⟩ := hGrz; exact axiomT!; +lemma K4_weakerThan_GL : (Hilbert.K4 α) ≤ₛ (Hilbert.GL α) := normal_weakerThan_of_maxm $ by + rintro _ (⟨_, _, rfl⟩ | ⟨_, _, rfl⟩) <;> simp; -lemma K4_weakerThan_Grz : (𝐊𝟒 : Hilbert α) ≤ₛ 𝐆𝐫𝐳 := by - apply normal_weakerThan_of_maxm; - intro φ hp; - rcases hp with (hK | hGrz) - . obtain ⟨_, _, rfl⟩ := hK; exact axiomK!; - . obtain ⟨_, _, rfl⟩ := hGrz; exact axiomFour!; +lemma KT_weakerThan_Grz : (Hilbert.KT α) ≤ₛ (Hilbert.Grz α) := normal_weakerThan_of_maxm $ by + rintro _ (⟨_, _, rfl⟩ | ⟨_, _, rfl⟩) <;> simp; +lemma K4_weakerThan_Grz : (Hilbert.K4 α) ≤ₛ (Hilbert.Grz α) := normal_weakerThan_of_maxm $ by + rintro _ (⟨_, _, rfl⟩ | ⟨_, _, rfl⟩) <;> simp; -lemma KD_weakerThan_KP : (𝐊𝐃 : Hilbert α) ≤ₛ 𝐊𝐏 := normal_weakerThan_of_maxm $ by - rintro φ (⟨φ, ψ, rfl⟩ | ⟨φ, rfl⟩); - . exact axiomK!; - . exact axiomD!; +lemma KD_weakerThan_KP : (Hilbert.KD α) ≤ₛ (Hilbert.KP α) := normal_weakerThan_of_maxm $ by + rintro _ (⟨_, _, rfl⟩ | ⟨_, rfl⟩) <;> simp; -lemma KP_weakerThan_KD : (𝐊𝐏 : Hilbert α) ≤ₛ 𝐊𝐃 := normal_weakerThan_of_maxm $ by - rintro φ (⟨φ, ψ, rfl⟩ | ⟨_, rfl⟩); - . exact axiomK!; - . exact axiomP!; +lemma KP_weakerThan_KD : (Hilbert.KP α) ≤ₛ (Hilbert.KD α) := normal_weakerThan_of_maxm $ by + rintro _ (⟨_, _, rfl⟩ | ⟨_, rfl⟩) <;> simp; -lemma KD_equiv_KP : (𝐊𝐃 : Hilbert α) =ₛ 𝐊𝐏 := Equiv.antisymm_iff.mpr ⟨KD_weakerThan_KP, KP_weakerThan_KD⟩ +lemma KD_equiv_KP : (Hilbert.KD α) =ₛ (Hilbert.KP α) := Equiv.antisymm_iff.mpr ⟨KD_weakerThan_KP, KP_weakerThan_KD⟩ - -lemma GL_weakerThan_K4Loeb : (𝐆𝐋 : Hilbert α) ≤ₛ 𝐊𝟒(𝐋) := by +lemma GL_weakerThan_K4Loeb : (Hilbert.GL α) ≤ₛ (Hilbert.K4Loeb α) := by apply System.weakerThan_iff.mpr; intro φ h; induction h using Deduction.inducition_with_necOnly! with @@ -442,7 +407,7 @@ lemma GL_weakerThan_K4Loeb : (𝐆𝐋 : Hilbert α) ≤ₛ 𝐊𝟒(𝐋) := by | hNec ihp => exact nec! ihp; | _ => trivial; -lemma K4Loeb_weakerThan_K4Henkin : (𝐊𝟒(𝐋) : Hilbert α) ≤ₛ 𝐊𝟒(𝐇) := by +lemma K4Loeb_weakerThan_K4Henkin : (Hilbert.K4Loeb α) ≤ₛ (Hilbert.K4Henkin α) := by apply System.weakerThan_iff.mpr; intro φ h; induction h using Deduction.inducition! with @@ -457,7 +422,7 @@ lemma K4Loeb_weakerThan_K4Henkin : (𝐊𝟒(𝐋) : Hilbert α) ≤ₛ 𝐊𝟒 . obtain ⟨φ, rfl⟩ := hLoeb; exact loeb! $ ihp $ by simp_all only [List.mem_singleton, forall_eq]; | _ => trivial; -lemma K4Henkin_weakerThan_K4H : (𝐊𝟒(𝐇) : Hilbert α) ≤ₛ 𝐊𝟒𝐇 := by +lemma K4Henkin_weakerThan_K4H : (Hilbert.K4Henkin α) ≤ₛ (Hilbert.K4H α) := by apply System.weakerThan_iff.mpr; intro φ h; induction h using Deduction.inducition! with @@ -472,7 +437,7 @@ lemma K4Henkin_weakerThan_K4H : (𝐊𝟒(𝐇) : Hilbert α) ≤ₛ 𝐊𝟒 . obtain ⟨φ, rfl⟩ := hHenkin; exact henkin! $ ihp $ by simp_all only [List.mem_singleton, forall_eq]; | _ => trivial; -lemma K4Henkin_weakerThan_GL : (𝐊𝟒𝐇 : Hilbert α) ≤ₛ 𝐆𝐋 := by +lemma K4Henkin_weakerThan_GL : (Hilbert.K4H α) ≤ₛ (Hilbert.GL α) := by apply normal_weakerThan_of_maxm; intro φ hp; rcases hp with hK | hFour | hH @@ -480,38 +445,30 @@ lemma K4Henkin_weakerThan_GL : (𝐊𝟒𝐇 : Hilbert α) ≤ₛ 𝐆𝐋 := by . obtain ⟨_, _, rfl⟩ := hFour; exact axiomFour!; . obtain ⟨_, _, rfl⟩ := hH; exact axiomH!; -lemma GL_equiv_K4Loeb : (𝐆𝐋 : Hilbert α) =ₛ 𝐊𝟒(𝐋) := by +lemma GL_equiv_K4Loeb : (Hilbert.GL α) =ₛ (Hilbert.K4Loeb α) := by apply Equiv.antisymm_iff.mpr; constructor; . exact GL_weakerThan_K4Loeb; . exact WeakerThan.trans (K4Loeb_weakerThan_K4Henkin) $ WeakerThan.trans K4Henkin_weakerThan_K4H K4Henkin_weakerThan_GL -set_option linter.unusedSectionVars false in -- TODO: remove -lemma GL_weakerThan_GLS : (𝐆𝐋 : Hilbert α) ≤ₛ 𝐆𝐋𝐒 := by +omit [DecidableEq α] in +lemma GL_weakerThan_GLS : (Hilbert.GL α) ≤ₛ (Hilbert.GLS α) := by apply System.weakerThan_iff.mpr; intro φ h; exact Deduction.maxm! (by left; simpa); -lemma S5Grz_weakerThan_Triv : (𝐒𝟓𝐆𝐫𝐳 : Hilbert α) ≤ₛ 𝐓𝐫𝐢𝐯 := by - apply normal_weakerThan_of_maxm; - intro φ hp; - rcases hp with ⟨_, _, rfl⟩ | (⟨_, rfl⟩ | ⟨_, rfl⟩) | ⟨_, rfl⟩ - . exact axiomK!; - . exact axiomT!; - . exact axiomFive!; - . exact axiomGrz!; +lemma S5Grz_weakerThan_Triv : (Hilbert.S5Grz α) ≤ₛ (Hilbert.Triv α) := normal_weakerThan_of_maxm $ by + rintro φ (⟨_, _, rfl⟩ | (⟨_, rfl⟩ | ⟨_, rfl⟩) | ⟨_, rfl⟩) <;> simp; -lemma Triv_weakerThan_S5Grz : (𝐓𝐫𝐢𝐯 : Hilbert α) ≤ₛ 𝐒𝟓𝐆𝐫𝐳 := by - apply normal_weakerThan_of_maxm; - intro φ hp; - rcases hp with ⟨_, _, rfl⟩ | ⟨_, rfl⟩ | ⟨_, rfl⟩ - . exact axiomK!; - . exact axiomT!; - . exact axiomTc!; +lemma Triv_weakerThan_S5Grz : (Hilbert.Triv α) ≤ₛ (Hilbert.S5Grz α) := normal_weakerThan_of_maxm $ by + rintro φ (⟨_, _, rfl⟩ | ⟨_, rfl⟩ | ⟨_, rfl⟩) <;> simp; -lemma S5Grz_equiv_Triv : (𝐒𝟓𝐆𝐫𝐳 : Hilbert α) =ₛ 𝐓𝐫𝐢𝐯 +lemma S5Grz_equiv_Triv : (Hilbert.S5Grz α) =ₛ (Hilbert.Triv α) := Equiv.antisymm_iff.mpr ⟨S5Grz_weakerThan_Triv, Triv_weakerThan_S5Grz⟩ end + +end Hilbert + end LO.Modal diff --git a/Foundation/Modal/Kripke/Completeness.lean b/Foundation/Modal/Kripke/Completeness.lean index e527452a..cff7001d 100644 --- a/Foundation/Modal/Kripke/Completeness.lean +++ b/Foundation/Modal/Kripke/Completeness.lean @@ -192,9 +192,9 @@ lemma complete_of_mem_canonicalFrame [Nonempty (MCT Λ)] {𝔽 : FrameClass} (hF instance instComplete_of_mem_canonicalFrame [Nonempty (MCT Λ)] (𝔽 : FrameClass) (hFC : CanonicalFrame Λ ∈ 𝔽) : Complete (Λ) (𝔽#α) := ⟨complete_of_mem_canonicalFrame hFC⟩ -instance K_complete : Complete 𝐊 (AllFrameClass.{u}#α) := by +instance K_complete : Complete (Hilbert.K α) (AllFrameClass.{u}#α) := by convert instComplete_of_mem_canonicalFrame (α := α) AllFrameClass trivial; - rw [K_is_extK_of_empty]; + rw [Hilbert.ExtK.K_is_extK_of_empty]; . tauto; . infer_instance; diff --git a/Foundation/Modal/Kripke/Dot3.lean b/Foundation/Modal/Kripke/Dot3.lean index 2738fc85..2b10e581 100644 --- a/Foundation/Modal/Kripke/Dot3.lean +++ b/Foundation/Modal/Kripke/Dot3.lean @@ -73,14 +73,14 @@ instance axiomS4Dot3_defines [Atleast 2 α] [Inhabited α] [DecidableEq α] : simp [Reflexive, Transitive, Connected]; refine ⟨⟨?_, ?_⟩, ?_⟩ <;> tauto; -instance S4Dot3_defines [Inhabited α] [DecidableEq α] [Atleast 2 α] : 𝔽((𝐒𝟒.𝟑 : Hilbert α)).DefinedBy ReflexiveTransitiveConnectedFrameClass := inferInstance +instance S4Dot3_defines [Inhabited α] [DecidableEq α] [Atleast 2 α] : 𝔽((Hilbert.S4Dot3 α)).DefinedBy ReflexiveTransitiveConnectedFrameClass := inferInstance -instance [Inhabited α] [DecidableEq α] [Atleast 2 α] : System.Consistent (𝐒𝟒.𝟑 : Hilbert α) := inferInstance +instance [Inhabited α] [DecidableEq α] [Atleast 2 α] : System.Consistent (Hilbert.S4Dot3 α) := inferInstance open MaximalConsistentTheory in lemma connected_CanonicalFrame [Inhabited α] [DecidableEq α] [Atleast 2 α] - {Ax : Theory α} (hAx : .𝟯 ⊆ Ax) [System.Consistent (𝜿Ax)] : Connected (CanonicalFrame 𝜿Ax) := by + {Ax : Theory α} (hAx : .𝟯 ⊆ Ax) [System.Consistent (Hilbert.ExtK Ax)] : Connected (CanonicalFrame (Hilbert.ExtK Ax)) := by dsimp only [Connected]; intro X Y Z ⟨hXY, hXZ⟩; by_contra hC; push_neg at hC; @@ -108,7 +108,7 @@ lemma connected_CanonicalFrame instance [Inhabited α] [DecidableEq α] [Atleast 2 α] - : Complete (𝐒𝟒.𝟑 : Hilbert α) (ReflexiveTransitiveConnectedFrameClass.{u}#α) := instComplete_of_mem_canonicalFrame ReflexiveTransitiveConnectedFrameClass $ by + : Complete (Hilbert.S4Dot3 α) (ReflexiveTransitiveConnectedFrameClass.{u}#α) := instComplete_of_mem_canonicalFrame ReflexiveTransitiveConnectedFrameClass $ by refine ⟨?reflexive, ?transitive, ?connective⟩; . simp [GeachConfluent.reflexive_def]; apply geachConfluent_CanonicalFrame; diff --git a/Foundation/Modal/Kripke/Filteration.lean b/Foundation/Modal/Kripke/Filteration.lean index 14cf2f29..e703a75a 100644 --- a/Foundation/Modal/Kripke/Filteration.lean +++ b/Foundation/Modal/Kripke/Filteration.lean @@ -180,7 +180,7 @@ theorem filteration {x : M.World} {φ : Formula α} (hs : φ ∈ T := by trivial end -instance K_finite_complete [DecidableEq α] : Complete 𝐊 (AllFrameClass.{u}ꟳ#α) := ⟨by +instance K_finite_complete [DecidableEq α] : Complete (Hilbert.K α) (AllFrameClass.{u}ꟳ#α) := ⟨by intro φ hp; apply K_complete.complete; intro F _ V x; @@ -195,10 +195,10 @@ instance K_finite_complete [DecidableEq α] : Complete 𝐊 (AllFrameClass.{u} ) FM.Valuation ⟩ -instance [DecidableEq α] : FiniteFrameProperty (α := α) 𝐊 AllFrameClass where +instance [DecidableEq α] : FiniteFrameProperty (Hilbert.K α) AllFrameClass where -instance KTB_finite_complete [DecidableEq α] [Inhabited α] : Complete 𝐊𝐓𝐁 (ReflexiveSymmetricFrameClass.{u}ꟳ#α) := ⟨by +instance KTB_finite_complete [DecidableEq α] [Inhabited α] : Complete (Hilbert.KTB α) (ReflexiveSymmetricFrameClass.{u}ꟳ#α) := ⟨by intro φ hp; apply KTB_complete.complete; intro F ⟨F_refl, F_symm⟩ V x; @@ -219,7 +219,7 @@ instance KTB_finite_complete [DecidableEq α] [Inhabited α] : Complete 𝐊𝐓 ) FM.Valuation ⟩ -instance [DecidableEq α] [Inhabited α] : FiniteFrameProperty (α := α) 𝐊𝐓𝐁 ReflexiveSymmetricFrameClass where +instance [DecidableEq α] [Inhabited α] : FiniteFrameProperty (Hilbert.KTB α) ReflexiveSymmetricFrameClass where section @@ -272,7 +272,7 @@ end FinestFilterationTransitiveClosureModel end open FinestFilterationTransitiveClosureModel in -instance S4_finite_complete [Inhabited α] [DecidableEq α] : Complete 𝐒𝟒 (PreorderFrameClass.{u}ꟳ#α) := ⟨by +instance S4_finite_complete [Inhabited α] [DecidableEq α] : Complete (Hilbert.S4 α) (PreorderFrameClass.{u}ꟳ#α) := ⟨by intro φ hp; apply S4_complete.complete; intro F ⟨F_refl, F_trans⟩ V x; @@ -291,11 +291,11 @@ instance S4_finite_complete [Inhabited α] [DecidableEq α] : Complete 𝐒𝟒 exact F_trans; ⟩ -instance [Inhabited α] [DecidableEq α] : FiniteFrameProperty (α := α) 𝐒𝟒 PreorderFrameClass where +instance [Inhabited α] [DecidableEq α] : FiniteFrameProperty (Hilbert.S4 α) PreorderFrameClass where open FinestFilterationTransitiveClosureModel in -instance KT4B_finite_complete [Inhabited α] [DecidableEq α] : Complete 𝐊𝐓𝟒𝐁 (EquivalenceFrameClass.{u}ꟳ#α) := ⟨by +instance KT4B_finite_complete [Inhabited α] [DecidableEq α] : Complete (Hilbert.KT4B α) (EquivalenceFrameClass.{u}ꟳ#α) := ⟨by intro φ hp; apply KT4B_complete.complete; intro F ⟨F_refl, F_trans, F_symm⟩ V x; @@ -315,7 +315,7 @@ instance KT4B_finite_complete [Inhabited α] [DecidableEq α] : Complete 𝐊 exact F_trans; ⟩ -instance [Inhabited α] [DecidableEq α] : FiniteFrameProperty (α := α) 𝐊𝐓𝟒𝐁 EquivalenceFrameClass where +instance [Inhabited α] [DecidableEq α] : FiniteFrameProperty (Hilbert.KT4B α) EquivalenceFrameClass where -- MEMO: `𝐒𝟓 =ₛ 𝐊𝐓𝟒𝐁`だから決定可能性という面では`𝐒𝟓`も決定可能． end Kripke diff --git a/Foundation/Modal/Kripke/GL/Completeness.lean b/Foundation/Modal/Kripke/GL/Completeness.lean index 81a39500..e1dcb417 100644 --- a/Foundation/Modal/Kripke/GL/Completeness.lean +++ b/Foundation/Modal/Kripke/GL/Completeness.lean @@ -13,7 +13,7 @@ namespace Kripke open Formula abbrev GLCompleteFrame (φ : Formula α) : Kripke.FiniteFrame where - World := CCF 𝐆𝐋 φ.subformulae + World := CCF (Hilbert.GL α) φ.subformulae Rel X Y := (∀ ψ ∈ □''⁻¹φ.subformulae, □ψ ∈ X.formulae → (ψ ∈ Y.formulae ∧ □ψ ∈ Y.formulae)) ∧ (∃ χ ∈ □''⁻¹φ.subformulae, □χ ∉ X.formulae ∧ □χ ∈ Y.formulae) @@ -45,7 +45,7 @@ open ComplementaryClosedConsistentFormulae omit [Inhabited α] in private lemma GL_truthlemma.lemma1 - {X : CCF 𝐆𝐋 φ.subformulae} (hq : □ψ ∈ φ.subformulae) + {X : CCF (Hilbert.GL α) φ.subformulae} (hq : □ψ ∈ φ.subformulae) : ((X.formulae.prebox ∪ X.formulae.prebox.box) ∪ {□ψ, -ψ}) ⊆ φ.subformulae⁻ := by simp only [Formulae.complementary]; intro χ hr; @@ -68,8 +68,8 @@ private lemma GL_truthlemma.lemma1 omit [Inhabited α] in private lemma GL_truthlemma.lemma2 - {X : CCF 𝐆𝐋 φ.subformulae} (hq₁ : □ψ ∈ φ.subformulae) (hq₂ : □ψ ∉ X.formulae) - : Formulae.Consistent 𝐆𝐋 ((X.formulae.prebox ∪ X.formulae.prebox.box) ∪ {□ψ, -ψ}) := by + {X : CCF (Hilbert.GL α) φ.subformulae} (hq₁ : □ψ ∈ φ.subformulae) (hq₂ : □ψ ∉ X.formulae) + : Formulae.Consistent (Hilbert.GL α) ((X.formulae.prebox ∪ X.formulae.prebox.box) ∪ {□ψ, -ψ}) := by apply Formulae.intro_union_consistent; rintro Γ₁ Γ₂ ⟨hΓ₁, hΓ₂⟩; @@ -78,29 +78,29 @@ private lemma GL_truthlemma.lemma2 simpa using hΓ₂ χ hr; by_contra hC; - have : Γ₁ ⊢[𝐆𝐋]! ⋀Γ₂ ➝ ⊥ := provable_iff.mpr $ and_imply_iff_imply_imply'!.mp hC; - have : Γ₁ ⊢[𝐆𝐋]! (□ψ ⋏ -ψ) ➝ ⊥ := imp_trans''! (by - suffices Γ₁ ⊢[𝐆𝐋]! ⋀[□ψ, -ψ] ➝ ⋀Γ₂ by + have : Γ₁ ⊢[_]! ⋀Γ₂ ➝ ⊥ := provable_iff.mpr $ and_imply_iff_imply_imply'!.mp hC; + have : Γ₁ ⊢[_]! (□ψ ⋏ -ψ) ➝ ⊥ := imp_trans''! (by + suffices Γ₁ ⊢[(Hilbert.GL α)]! ⋀[□ψ, -ψ] ➝ ⋀Γ₂ by simpa only [ne_eq, List.cons_ne_self, not_false_eq_true, List.conj₂_cons_nonempty, List.conj₂_singleton]; apply conjconj_subset!; simpa using hΓ₂; ) this; - have : Γ₁ ⊢[𝐆𝐋]! □ψ ➝ -ψ ➝ ⊥ := and_imply_iff_imply_imply'!.mp this; - have : Γ₁ ⊢[𝐆𝐋]! □ψ ➝ ψ := by + have : Γ₁ ⊢[_]! □ψ ➝ -ψ ➝ ⊥ := and_imply_iff_imply_imply'!.mp this; + have : Γ₁ ⊢[(Hilbert.GL α)]! □ψ ➝ ψ := by rcases Formula.complement.or (φ := ψ) with (hp | ⟨ψ, rfl⟩); . rw [hp] at this; exact imp_trans''! this dne!; . simpa only [complement] using this; - have : (□'Γ₁) ⊢[𝐆𝐋]! □(□ψ ➝ ψ) := contextual_nec! this; - have : (□'Γ₁) ⊢[𝐆𝐋]! □ψ := axiomL! ⨀ this; - have : 𝐆𝐋 ⊢! ⋀□'Γ₁ ➝ □ψ := provable_iff.mp this; - have : 𝐆𝐋 ⊢! ⋀□'(X.formulae.prebox ∪ X.formulae.prebox.box |>.toList) ➝ □ψ := imp_trans''! (conjconj_subset! (by + have : (□'Γ₁) ⊢[_]! □(□ψ ➝ ψ) := contextual_nec! this; + have : (□'Γ₁) ⊢[_]! □ψ := axiomL! ⨀ this; + have : _ ⊢! ⋀□'Γ₁ ➝ □ψ := provable_iff.mp this; + have : _ ⊢! ⋀□'(X.formulae.prebox ∪ X.formulae.prebox.box |>.toList) ➝ □ψ := imp_trans''! (conjconj_subset! (by simp; intro χ hr; have := hΓ₁ _ hr; simp at this; tauto; )) this; - have : 𝐆𝐋 ⊢! ⋀□'(X.formulae.prebox.toList) ➝ □ψ := imp_trans''! (conjconj_provable! (by + have : _ ⊢! ⋀□'(X.formulae.prebox.toList) ➝ □ψ := imp_trans''! (conjconj_provable! (by intro ψ hq; simp at hq; obtain ⟨χ, hr, rfl⟩ := hq; @@ -111,7 +111,7 @@ private lemma GL_truthlemma.lemma2 apply FiniteContext.by_axm!; simpa; )) this; - have : X.formulae *⊢[𝐆𝐋]! □ψ := by + have : X.formulae *⊢[(Hilbert.GL α)]! □ψ := by apply Context.provable_iff.mpr; use □'X.formulae.prebox.toList; constructor; @@ -169,7 +169,7 @@ lemma GL_truthlemma {X : (GLCompleteModel φ)} (q_sub : ψ ∈ φ.subformulae) : refine RXY.1 ψ ?_ h |>.1; assumption; -private lemma GL_completeAux : TransitiveIrreflexiveFrameClass.{u}ꟳ#α ⊧ φ → 𝐆𝐋 ⊢! φ := by +private lemma GL_completeAux : TransitiveIrreflexiveFrameClass.{u}ꟳ#α ⊧ φ → (Hilbert.GL α) ⊢! φ := by contrapose; intro h; apply exists_finite_frame.mpr; @@ -190,9 +190,9 @@ private lemma GL_completeAux : TransitiveIrreflexiveFrameClass.{u}ꟳ#α ⊧ φ apply hX₁; tauto; -instance GL_complete : Complete (𝐆𝐋 : Hilbert α) TransitiveIrreflexiveFrameClass.{u}ꟳ#α := ⟨GL_completeAux⟩ +instance GL_complete : Complete (Hilbert.GL α) TransitiveIrreflexiveFrameClass.{u}ꟳ#α := ⟨GL_completeAux⟩ -instance : FiniteFrameProperty (α := α) 𝐆𝐋 TransitiveIrreflexiveFrameClass where +instance : FiniteFrameProperty (Hilbert.GL α) TransitiveIrreflexiveFrameClass where end Kripke diff --git a/Foundation/Modal/Kripke/GL/Definability.lean b/Foundation/Modal/Kripke/GL/Definability.lean index fcd26313..f856c7a6 100644 --- a/Foundation/Modal/Kripke/GL/Definability.lean +++ b/Foundation/Modal/Kripke/GL/Definability.lean @@ -88,8 +88,8 @@ instance axiomL_definability : 𝔽((𝗟 : Theory α)).DefinedBy (TransitiveCon simp [Transitive, ConverseWellFounded]; apply WellFounded.trivial_wellfounded; -instance : Sound (𝐆𝐋 : Hilbert α) (TransitiveConverseWellFoundedFrameClass#α) := inferInstance -instance : System.Consistent (𝐆𝐋 : Hilbert α) := inferInstance +instance : Sound (Hilbert.GL α) (TransitiveConverseWellFoundedFrameClass#α) := inferInstance +instance : System.Consistent (Hilbert.GL α) := inferInstance instance axiomL_finite_definability : 𝔽ꟳ((𝗟 : Theory α)).DefinedBy (TransitiveIrreflexiveFrameClassꟳ) where define := by @@ -111,7 +111,7 @@ instance axiomL_finite_definability : 𝔽ꟳ((𝗟 : Theory α)).DefinedBy (Tra use ⟨PUnit, λ _ _ => False⟩; refine ⟨?_, ?_⟩ <;> tauto; -instance GL_finite_sound : Sound 𝐆𝐋 (TransitiveIrreflexiveFrameClassꟳ#α) := inferInstance +instance GL_finite_sound : Sound (Hilbert.GL α) (TransitiveIrreflexiveFrameClassꟳ#α) := inferInstance end Kripke diff --git a/Foundation/Modal/Kripke/GL/MDP.lean b/Foundation/Modal/Kripke/GL/MDP.lean index 4e1d46e5..a0f49685 100644 --- a/Foundation/Modal/Kripke/GL/MDP.lean +++ b/Foundation/Modal/Kripke/GL/MDP.lean @@ -119,16 +119,16 @@ end Kripke variable {X : Theory α} {φ₁ φ₂ : Formula α} -lemma GL_MDP_Aux [Inhabited α] (h : (□''X) *⊢[𝐆𝐋]! □φ₁ ⋎ □φ₂) : (□''X) *⊢[𝐆𝐋]! □φ₁ ∨ (□''X) *⊢[𝐆𝐋]! □φ₂ := by +lemma GL_MDP_Aux [Inhabited α] (h : (□''X) *⊢[(Hilbert.GL α)]! □φ₁ ⋎ □φ₂) : (□''X) *⊢[(Hilbert.GL α)]! □φ₁ ∨ (□''X) *⊢[(Hilbert.GL α)]! □φ₂ := by obtain ⟨Δ, sΓ, hΓ⟩ := Context.provable_iff_boxed.mp h; - have : 𝐆𝐋 ⊢! ⋀□'Δ ➝ (□φ₁ ⋎ □φ₂) := FiniteContext.provable_iff.mp hΓ; - have : 𝐆𝐋 ⊢! □⋀Δ ➝ (□φ₁ ⋎ □φ₂) := imp_trans''! (by simp) this; + have : (Hilbert.GL α) ⊢! ⋀□'Δ ➝ (□φ₁ ⋎ □φ₂) := FiniteContext.provable_iff.mp hΓ; + have : (Hilbert.GL α) ⊢! □⋀Δ ➝ (□φ₁ ⋎ □φ₂) := imp_trans''! (by simp) this; generalize e : ⋀Δ = c at this; - have : (𝐆𝐋 ⊢! ⊡c ➝ φ₁) ⋎ (𝐆𝐋 ⊢! ⊡c ➝ φ₂) := by + have : ((Hilbert.GL α) ⊢! ⊡c ➝ φ₁) ⋎ ((Hilbert.GL α) ⊢! ⊡c ➝ φ₂) := by by_contra hC; - have ⟨h₁, h₂⟩ : (𝐆𝐋 ⊬ ⊡c ➝ φ₁) ∧ (𝐆𝐋 ⊬ ⊡c ➝ φ₂) := not_or.mp hC; + have ⟨h₁, h₂⟩ : ((Hilbert.GL α) ⊬ ⊡c ➝ φ₁) ∧ ((Hilbert.GL α) ⊬ ⊡c ➝ φ₂) := not_or.mp hC; obtain ⟨M₁, hM₁⟩ := iff_unprovable_GL_exists_unsatisfies_at_root_on_FiniteTransitiveTree.mp h₁; obtain ⟨M₂, hM₂⟩ := iff_unprovable_GL_exists_unsatisfies_at_root_on_FiniteTransitiveTree.mp h₂; @@ -175,7 +175,7 @@ lemma GL_MDP_Aux [Inhabited α] (h : (□''X) *⊢[𝐆𝐋]! □φ₁ ⋎ □φ tauto; }; -theorem GL_MDP [Inhabited α] (h : 𝐆𝐋 ⊢! □φ₁ ⋎ □φ₂) : 𝐆𝐋 ⊢! φ₁ ∨ 𝐆𝐋 ⊢! φ₂ := by +theorem GL_MDP [Inhabited α] (h : (Hilbert.GL α) ⊢! □φ₁ ⋎ □φ₂) : (Hilbert.GL α) ⊢! φ₁ ∨ (Hilbert.GL α) ⊢! φ₂ := by have := GL_MDP_Aux (X := ∅) (φ₁ := φ₁) (φ₂ := φ₂) $ Context.of! h; simp at this; rcases this with (h | h) <;> { @@ -183,6 +183,6 @@ theorem GL_MDP [Inhabited α] (h : 𝐆𝐋 ⊢! □φ₁ ⋎ □φ₂) : 𝐆 tauto; } -instance [Inhabited α] : System.ModalDisjunctive (𝐆𝐋 : Hilbert α) := ⟨GL_MDP⟩ +instance [Inhabited α] : System.ModalDisjunctive (Hilbert.GL α) := ⟨GL_MDP⟩ end LO.Modal diff --git a/Foundation/Modal/Kripke/GL/Tree.lean b/Foundation/Modal/Kripke/GL/Tree.lean index 42164bfb..cef4bb41 100644 --- a/Foundation/Modal/Kripke/GL/Tree.lean +++ b/Foundation/Modal/Kripke/GL/Tree.lean @@ -48,7 +48,7 @@ lemma valid_on_TransitiveIrreflexiveFrameClass_of_satisfies_at_root_on_FiniteTra exact H ⟨(F.FiniteTransitiveTreeUnravelling F_trans F_irrefl r), (M.FiniteTransitiveTreeUnravelling r).Valuation⟩; variable [Inhabited α] [DecidableEq α] -theorem iff_provable_GL_satisfies_at_root_on_FiniteTransitiveTree : 𝐆𝐋 ⊢! φ ↔ (∀ M : FiniteTransitiveTreeModel.{u, u} α, M.root ⊧ φ) := by +theorem iff_provable_GL_satisfies_at_root_on_FiniteTransitiveTree : (Hilbert.GL α) ⊢! φ ↔ (∀ M : FiniteTransitiveTreeModel.{u, u} α, M.root ⊧ φ) := by constructor; . intro h M; have : TransitiveIrreflexiveFrameClassꟳ#α ⊧ φ := GL_finite_sound.sound h; @@ -59,7 +59,7 @@ theorem iff_provable_GL_satisfies_at_root_on_FiniteTransitiveTree : 𝐆𝐋 ⊢ intro F hF V; apply valid_on_TransitiveIrreflexiveFrameClass_of_satisfies_at_root_on_FiniteTransitiveTree h hF; -lemma iff_unprovable_GL_exists_unsatisfies_at_root_on_FiniteTransitiveTree : 𝐆𝐋 ⊬ φ ↔ ∃ M : FiniteTransitiveTreeModel.{u, u} α, ¬M.root ⊧ φ := by +lemma iff_unprovable_GL_exists_unsatisfies_at_root_on_FiniteTransitiveTree : (Hilbert.GL α) ⊬ φ ↔ ∃ M : FiniteTransitiveTreeModel.{u, u} α, ¬M.root ⊧ φ := by constructor; . contrapose; simp; apply iff_provable_GL_satisfies_at_root_on_FiniteTransitiveTree.mpr; . contrapose; simp; apply iff_provable_GL_satisfies_at_root_on_FiniteTransitiveTree.mp; @@ -67,8 +67,6 @@ lemma iff_unprovable_GL_exists_unsatisfies_at_root_on_FiniteTransitiveTree : end -#check Finite - def FiniteTransitiveTree.SimpleExtension (F : FiniteTransitiveTree) : Kripke.FiniteTransitiveTree where World := (Fin 1) ⊕ F.World Rel x y := @@ -171,7 +169,7 @@ variable {φ ψ : Formula α} - `System.imply_boxdot_axiomT_of_imply_boxdot_boxdot` - `System.imply_box_box_of_imply_boxdot_axiomT` -/ -lemma GL_imply_boxdot_plain_of_imply_box_box : 𝐆𝐋 ⊢! □φ ➝ □ψ → 𝐆𝐋 ⊢! ⊡φ ➝ ψ := by +lemma GL_imply_boxdot_plain_of_imply_box_box : (Hilbert.GL α) ⊢! □φ ➝ □ψ → (Hilbert.GL α) ⊢! ⊡φ ➝ ψ := by contrapose; intro h; have := iff_unprovable_GL_exists_unsatisfies_at_root_on_FiniteTransitiveTree.mp h; @@ -199,13 +197,13 @@ lemma GL_imply_boxdot_plain_of_imply_box_box : 𝐆𝐋 ⊢! □φ ➝ □ψ → use M↧; exact _root_.not_imp.mpr ⟨hbp, hbq⟩; -theorem GL_unnecessitation! : 𝐆𝐋 ⊢! □φ → 𝐆𝐋 ⊢! φ := by +theorem GL_unnecessitation! : (Hilbert.GL α) ⊢! □φ → (Hilbert.GL α) ⊢! φ := by intro h; - have : 𝐆𝐋 ⊢! □⊤ ➝ □φ := imply₁'! (ψ := □⊤) h; - have : 𝐆𝐋 ⊢! ⊡⊤ ➝ φ := GL_imply_boxdot_plain_of_imply_box_box this; + have : (Hilbert.GL α) ⊢! □⊤ ➝ □φ := imply₁'! (ψ := □⊤) h; + have : (Hilbert.GL α) ⊢! ⊡⊤ ➝ φ := GL_imply_boxdot_plain_of_imply_box_box this; exact this ⨀ boxdotverum!; -noncomputable instance : System.Unnecessitation (𝐆𝐋 : Hilbert α) where +noncomputable instance : System.Unnecessitation (Hilbert.GL α) where unnec := λ h => GL_unnecessitation! ⟨h⟩ |>.some end Unnecessitation diff --git a/Foundation/Modal/Kripke/Geach.lean b/Foundation/Modal/Kripke/Geach.lean index 409f5d2c..6219a111 100644 --- a/Foundation/Modal/Kripke/Geach.lean +++ b/Foundation/Modal/Kripke/Geach.lean @@ -211,11 +211,11 @@ instance axiomMultiGeach_definability : 𝔽((𝗚𝗲(ts) : Theory α)).Defined define := axiomMultiGeach_defines; nonempty := MultiGeachConfluentFrameClass.nonempty -instance Geach_definability : 𝔽((𝐆𝐞(ts) : Hilbert α)).DefinedBy (MultiGeachConfluentFrameClass ts) := inferInstance +instance Geach_definability : 𝔽(Hilbert.Geach α ts).DefinedBy (MultiGeachConfluentFrameClass ts) := inferInstance -instance sound_Geach : Sound 𝐆𝐞(ts) ((MultiGeachConfluentFrameClass ts)#α) := inferInstance +instance sound_Geach : Sound (Hilbert.Geach α ts) ((MultiGeachConfluentFrameClass ts)#α) := inferInstance -instance : System.Consistent (𝐆𝐞(ts) : Hilbert α) := inferInstance +instance : System.Consistent (Hilbert.Geach α ts) := inferInstance instance instGeachLogicSound @@ -224,21 +224,21 @@ instance instGeachLogicSound . exact logic_geach.char; . exact class_geach.equality; -instance KD_sound : Sound 𝐊𝐃 (SerialFrameClass#α) := inferInstance +instance KD_sound : Sound (Hilbert.KD α) (SerialFrameClass#α) := inferInstance -instance KT_sound : Sound 𝐊𝐓 (ReflexiveFrameClass#α) := inferInstance +instance KT_sound : Sound (Hilbert.KT α) (ReflexiveFrameClass#α) := inferInstance -instance KTB_sound : Sound 𝐊𝐓𝐁 (ReflexiveSymmetricFrameClass#α) := inferInstance +instance KTB_sound : Sound (Hilbert.KTB α) (ReflexiveSymmetricFrameClass#α) := inferInstance -instance K4_sound : Sound 𝐊𝟒 (TransitiveFrameClass#α) := inferInstance +instance K4_sound : Sound (Hilbert.K4 α) (TransitiveFrameClass#α) := inferInstance -instance S4_sound : Sound 𝐒𝟒 (PreorderFrameClass#α) := inferInstance +instance S4_sound : Sound (Hilbert.S4 α) (PreorderFrameClass#α) := inferInstance -@[deprecated] lemma S4_sound_aux : 𝐒𝟒 ⊢! φ → (PreorderFrameClass#α) ⊧ φ := S4_sound.sound +@[deprecated] lemma S4_sound_aux : (Hilbert.S4 α) ⊢! φ → (PreorderFrameClass#α) ⊧ φ := S4_sound.sound -instance S5_sound : Sound 𝐒𝟓 (ReflexiveEuclideanFrameClass#α) := inferInstance +instance S5_sound : Sound (Hilbert.S5 α) (ReflexiveEuclideanFrameClass#α) := inferInstance -instance KT4B_sound : Sound 𝐊𝐓𝟒𝐁 (EquivalenceFrameClass#α) := inferInstance +instance KT4B_sound : Sound (Hilbert.KT4B α) (EquivalenceFrameClass#α) := inferInstance end @@ -246,12 +246,12 @@ end open System open Theory MaximalConsistentTheory CanonicalFrame -variable {Ax : Theory α} [System.Consistent (𝜿Ax)] [DecidableEq α] +variable {Ax : Theory α} [System.Consistent (Hilbert.ExtK Ax)] [DecidableEq α] -lemma geachConfluent_CanonicalFrame (h : 𝗴𝗲(t) ⊆ Ax) : GeachConfluent t (CanonicalFrame 𝜿Ax).Rel := by +lemma geachConfluent_CanonicalFrame (h : 𝗴𝗲(t) ⊆ Ax) : GeachConfluent t (CanonicalFrame (Hilbert.ExtK Ax)).Rel := by rintro Ω₁ Ω₂ Ω₃ h; have ⟨r₁₂, r₁₃⟩ := h; clear h; - have ⟨Ω, hΩ⟩ := lindenbaum (Λ := 𝜿Ax) (T := □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory) $ by + have ⟨Ω, hΩ⟩ := lindenbaum (Λ := (Hilbert.ExtK Ax)) (T := □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory) $ by apply intro_union_consistent; rintro Γ Δ ⟨hΓ, hΔ⟩ hC; @@ -262,17 +262,17 @@ lemma geachConfluent_CanonicalFrame (h : 𝗴𝗲(t) ⊆ Ax) : GeachConfluent t have : □^[t.n]⋀Δ ∈ Ω₃.theory := iff_mem_multibox_conj.mpr hΔ; have : □^[t.j](◇^[t.n]⋀Γ) ∈ Ω₁.theory := iff_mem_imp.mp - (membership_iff.mpr $ Context.of! $ Normal.maxm! (by aesop)) + (membership_iff.mpr $ Context.of! $ Hilbert.ExtK.maxm! (by aesop)) (multirel_def_multidia.mp r₁₂ hΓconj) have : ◇^[t.n]⋀Γ ∈ Ω₃.theory := multirel_def_multibox.mp r₁₃ this; - have : 𝜿Ax ⊢! □^[t.n]⋀Δ ⋏ ◇^[t.n]⋀Γ ➝ ⊥ := by { + have : (Hilbert.ExtK Ax) ⊢! □^[t.n]⋀Δ ⋏ ◇^[t.n]⋀Γ ➝ ⊥ := by { apply and_imply_iff_imply_imply'!.mpr; exact imp_trans''! - (show 𝜿Ax ⊢! □^[t.n]⋀Δ ➝ □^[t.n](∼⋀Γ) by exact imply_multibox_distribute'! $ contra₁'! $ imp_trans''! (and_imply_iff_imply_imply'!.mp hC) (and₂'! neg_equiv!)) - (show 𝜿Ax ⊢! □^[t.n](∼⋀Γ) ➝ (◇^[t.n]⋀Γ) ➝ ⊥ by exact imp_trans''! (contra₁'! $ and₁'! $ multidia_duality!) (and₁'! neg_equiv!)); + (show _ ⊢! □^[t.n]⋀Δ ➝ □^[t.n](∼⋀Γ) by exact imply_multibox_distribute'! $ contra₁'! $ imp_trans''! (and_imply_iff_imply_imply'!.mp hC) (and₂'! neg_equiv!)) + (show _ ⊢! □^[t.n](∼⋀Γ) ➝ (◇^[t.n]⋀Γ) ➝ ⊥ by exact imp_trans''! (contra₁'! $ and₁'! $ multidia_duality!) (and₁'! neg_equiv!)); } - have : 𝜿Ax ⊬ □^[t.n]⋀Δ ⋏ ◇^[t.n]⋀Γ ➝ ⊥ := by simpa using (def_consistent.mp Ω₃.consistent) (Γ := [□^[t.n]⋀Δ, ◇^[t.n]⋀Γ]) (by simp_all) + have : (Hilbert.ExtK Ax) ⊬ □^[t.n]⋀Δ ⋏ ◇^[t.n]⋀Γ ➝ ⊥ := by simpa using (def_consistent.mp Ω₃.consistent) (Γ := [□^[t.n]⋀Δ, ◇^[t.n]⋀Γ]) (by simp_all) contradiction; @@ -281,7 +281,7 @@ lemma geachConfluent_CanonicalFrame (h : 𝗴𝗲(t) ⊆ Ax) : GeachConfluent t . apply multirel_def_multibox.mpr; apply hΩ.1; . apply multirel_def_multibox.mpr; apply hΩ.2; -lemma multiGeachConfluent_CanonicalFrame (h : 𝗚𝗲(ts) ⊆ Ax) : MultiGeachConfluent ts (CanonicalFrame 𝜿Ax).Rel := by +lemma multiGeachConfluent_CanonicalFrame (h : 𝗚𝗲(ts) ⊆ Ax) : MultiGeachConfluent ts (CanonicalFrame (Hilbert.ExtK Ax)).Rel := by induction ts using List.induction_with_singleton with | hnil => simp [MultiGeachConfluent]; | hsingle t => @@ -296,7 +296,7 @@ lemma multiGeachConfluent_CanonicalFrame (h : 𝗚𝗲(ts) ⊆ Ax) : MultiGeachC variable [Inhabited α] -instance instMultiGeachComplete : Complete 𝜿(𝗚𝗲(ts)) ((MultiGeachConfluentFrameClass.{u} ts)#α) := +instance instMultiGeachComplete : Complete (Hilbert.ExtK (𝗚𝗲(ts))) ((MultiGeachConfluentFrameClass.{u} ts)#α) := instComplete_of_mem_canonicalFrame (MultiGeachConfluentFrameClass ts) $ by apply multiGeachConfluent_CanonicalFrame; tauto; @@ -307,22 +307,22 @@ instance {Λ : Hilbert α} {𝔽 : FrameClass.{u}} [logic_geach : Λ.IsGeach ts] . exact class_geach.equality; -instance KT_complete : Complete 𝐊𝐓 ReflexiveFrameClass.{u}#α := inferInstance +instance KT_complete : Complete (Hilbert.KT α) ReflexiveFrameClass.{u}#α := inferInstance -instance KTB_complete : Complete 𝐊𝐓𝐁 ReflexiveSymmetricFrameClass.{u}#α := inferInstance +instance KTB_complete : Complete (Hilbert.KTB α) ReflexiveSymmetricFrameClass.{u}#α := inferInstance -instance S4_complete : Complete 𝐒𝟒 PreorderFrameClass.{u}#α := inferInstance +instance S4_complete : Complete (Hilbert.S4 α) PreorderFrameClass.{u}#α := inferInstance -instance K4_complete : Complete 𝐊𝟒 TransitiveFrameClass.{u}#α := inferInstance +instance K4_complete : Complete (Hilbert.K4 α) TransitiveFrameClass.{u}#α := inferInstance -instance KT4B_complete : Complete 𝐊𝐓𝟒𝐁 EquivalenceFrameClass.{u}#α := inferInstance +instance KT4B_complete : Complete (Hilbert.KT4B α) EquivalenceFrameClass.{u}#α := inferInstance -instance S5_complete : Complete 𝐒𝟓 ReflexiveEuclideanFrameClass.{u}#α := inferInstance +instance S5_complete : Complete (Hilbert.S5 α) ReflexiveEuclideanFrameClass.{u}#α := inferInstance end Kripke -section +namespace Hilbert open System open LO.Kripke @@ -332,11 +332,11 @@ open Formula.Kripke variable [Inhabited α] [DecidableEq α] -lemma KD_weakerThan_KT : (𝐊𝐃 : Hilbert α) ≤ₛ 𝐊𝐓 := by +lemma KD_weakerThan_KT : (Hilbert.KD α) ≤ₛ (Hilbert.KT α) := by apply weakerThan_of_subset_FrameClass SerialFrameClass ReflexiveFrameClass; intro F hF; apply serial_of_refl hF; -theorem KD_strictlyWeakerThan_KT : (𝐊𝐃 : Hilbert α) <ₛ 𝐊𝐓 := by +theorem KD_strictlyWeakerThan_KT : (Hilbert.KD α) <ₛ (Hilbert.KT α) := by constructor; . apply KD_weakerThan_KT; . simp [weakerThan_iff]; @@ -352,9 +352,9 @@ theorem KD_strictlyWeakerThan_KT : (𝐊𝐃 : Hilbert α) <ₛ 𝐊𝐓 := by use (λ w _ => w = 1), 0; simp [Satisfies]; -theorem K_strictlyWeakerThan_KT : (𝐊 : Hilbert α) <ₛ 𝐊𝐓 := strictlyWeakerThan.trans K_strictlyWeakerThan_KD KD_strictlyWeakerThan_KT +theorem K_strictlyWeakerThan_KT : (Hilbert.K α) <ₛ (Hilbert.KT α) := strictlyWeakerThan.trans K_strictlyWeakerThan_KD KD_strictlyWeakerThan_KT -theorem K4_strictlyWeakerThan_S4 : (𝐊𝟒 : Hilbert α) <ₛ 𝐒𝟒 := by +theorem K4_strictlyWeakerThan_S4 : (Hilbert.K4 α) <ₛ (Hilbert.S4 α) := by constructor; . apply K4_weakerThan_S4; . simp [weakerThan_iff] @@ -370,12 +370,12 @@ theorem K4_strictlyWeakerThan_S4 : (𝐊𝟒 : Hilbert α) <ₛ 𝐒𝟒 := by use (λ w _ => w = 1), 0; simp [Satisfies]; -lemma S4_weakerThan_S5 : (𝐒𝟒 : Hilbert α) ≤ₛ 𝐒𝟓 := by +lemma S4_weakerThan_S5 : (Hilbert.S4 α) ≤ₛ (Hilbert.S5 α) := by apply weakerThan_of_subset_FrameClass PreorderFrameClass ReflexiveEuclideanFrameClass; rintro _ ⟨F_refl, F_eucl⟩; refine ⟨F_refl, trans_of_refl_eucl F_refl F_eucl⟩; -theorem S4_strictlyWeakerThan_S5 : (𝐒𝟒 : Hilbert α) <ₛ 𝐒𝟓 := by +theorem S4_strictlyWeakerThan_S5 : (Hilbert.S4 α) <ₛ (Hilbert.S5 α) := by constructor; . apply S4_weakerThan_S5; . simp [weakerThan_iff]; @@ -395,7 +395,7 @@ theorem S4_strictlyWeakerThan_S5 : (𝐒𝟒 : Hilbert α) <ₛ 𝐒𝟓 := by . omega; . use 1; omega; -theorem equiv_S5_KT4B : (𝐒𝟓 : Hilbert α) =ₛ 𝐊𝐓𝟒𝐁 := by +theorem equiv_S5_KT4B : (Hilbert.S5 α) =ₛ (Hilbert.KT4B α) := by apply equiv_of_eq_FrameClass ReflexiveEuclideanFrameClass EquivalenceFrameClass; apply Set.eq_of_subset_of_subset; . rintro F ⟨F_refl, F_eucl⟩; @@ -403,6 +403,6 @@ theorem equiv_S5_KT4B : (𝐒𝟓 : Hilbert α) =ₛ 𝐊𝐓𝟒𝐁 := by . rintro F ⟨F_refl, F_eucl, F_symm⟩; refine ⟨F_refl, eucl_of_symm_trans F_symm F_eucl⟩; -end +end Hilbert end LO.Modal diff --git a/Foundation/Modal/Kripke/Grz/Completeness.lean b/Foundation/Modal/Kripke/Grz/Completeness.lean index 0cd97b47..9b3912ec 100644 --- a/Foundation/Modal/Kripke/Grz/Completeness.lean +++ b/Foundation/Modal/Kripke/Grz/Completeness.lean @@ -47,7 +47,7 @@ namespace Kripke open Formula abbrev GrzCompleteFrame [Inhabited α] (φ : Formula α) : Kripke.FiniteFrame where - World := CCF 𝐆𝐫𝐳 (φ.subformulaeGrz) + World := CCF (Hilbert.Grz α) (φ.subformulaeGrz) Rel X Y := (∀ ψ ∈ □''⁻¹(φ.subformulaeGrz), □ψ ∈ X.formulae → □ψ ∈ Y.formulae) ∧ ((∀ ψ ∈ □''⁻¹(φ.subformulaeGrz), □ψ ∈ Y.formulae → □ψ ∈ X.formulae) → X = Y) @@ -90,7 +90,7 @@ open Formula.Kripke open ComplementaryClosedConsistentFormulae private lemma Grz_truthlemma.lemma1 - {X : CCF 𝐆𝐫𝐳 (φ.subformulaeGrz)} (hq : □ψ ∈ φ.subformulae) + {X : CCF (Hilbert.Grz α) (φ.subformulaeGrz)} (hq : □ψ ∈ φ.subformulae) : ((X.formulae.prebox.box) ∪ {□(ψ ➝ □ψ), -ψ}) ⊆ (φ.subformulaeGrz)⁻ := by simp only [Formulae.complementary]; intro χ hr; @@ -111,8 +111,8 @@ private lemma Grz_truthlemma.lemma1 . rfl; private lemma Grz_truthlemma.lemma2 - {X : CCF 𝐆𝐫𝐳 (φ.subformulaeGrz)} (hq₁ : □ψ ∈ φ.subformulae) (hq₂ : □ψ ∉ X.formulae) - : Formulae.Consistent 𝐆𝐫𝐳 ((X.formulae.prebox.box) ∪ {□(ψ ➝ □ψ), -ψ}) := by + {X : CCF (Hilbert.Grz α) (φ.subformulaeGrz)} (hq₁ : □ψ ∈ φ.subformulae) (hq₂ : □ψ ∉ X.formulae) + : Formulae.Consistent (Hilbert.Grz α) ((X.formulae.prebox.box) ∪ {□(ψ ➝ □ψ), -ψ}) := by apply Formulae.intro_union_consistent; rintro Γ₁ Γ₂ ⟨hΓ₁, hΓ₂⟩; replace hΓ₂ : ∀ χ ∈ Γ₂, χ = □(ψ ➝ □ψ) ∨ χ = -ψ := by @@ -120,34 +120,34 @@ private lemma Grz_truthlemma.lemma2 simpa using hΓ₂ χ hr; by_contra hC; - have : Γ₁ ⊢[𝐆𝐫𝐳]! ⋀Γ₂ ➝ ⊥ := provable_iff.mpr $ and_imply_iff_imply_imply'!.mp hC; - have : Γ₁ ⊢[𝐆𝐫𝐳]! (□(ψ ➝ □ψ) ⋏ -ψ) ➝ ⊥ := imp_trans''! (by - suffices Γ₁ ⊢[𝐆𝐫𝐳]! ⋀[□(ψ ➝ □ψ), -ψ] ➝ ⋀Γ₂ by + have : Γ₁ ⊢[(Hilbert.Grz α)]! ⋀Γ₂ ➝ ⊥ := provable_iff.mpr $ and_imply_iff_imply_imply'!.mp hC; + have : Γ₁ ⊢[(Hilbert.Grz α)]! (□(ψ ➝ □ψ) ⋏ -ψ) ➝ ⊥ := imp_trans''! (by + suffices Γ₁ ⊢[(Hilbert.Grz α)]! ⋀[□(ψ ➝ □ψ), -ψ] ➝ ⋀Γ₂ by simpa only [ne_eq, List.cons_ne_self, not_false_eq_true, List.conj₂_cons_nonempty, List.conj₂_singleton]; apply conjconj_subset!; simpa using hΓ₂; ) this; - have : Γ₁ ⊢[𝐆𝐫𝐳]! □(ψ ➝ □ψ) ➝ -ψ ➝ ⊥ := and_imply_iff_imply_imply'!.mp this; - have : Γ₁ ⊢[𝐆𝐫𝐳]! □(ψ ➝ □ψ) ➝ ψ := by + have : Γ₁ ⊢[(Hilbert.Grz α)]! □(ψ ➝ □ψ) ➝ -ψ ➝ ⊥ := and_imply_iff_imply_imply'!.mp this; + have : Γ₁ ⊢[(Hilbert.Grz α)]! □(ψ ➝ □ψ) ➝ ψ := by rcases Formula.complement.or (φ := ψ) with (hp | ⟨ψ, rfl⟩); . rw [hp] at this; exact imp_trans''! this dne!; . simpa only [complement] using this; - have : (□'Γ₁) ⊢[𝐆𝐫𝐳]! □(□(ψ ➝ □ψ) ➝ ψ) := contextual_nec! this; - have : (□'Γ₁) ⊢[𝐆𝐫𝐳]! ψ := axiomGrz! ⨀ this; - have : (□'□'Γ₁) ⊢[𝐆𝐫𝐳]! □ψ := contextual_nec! this; + have : (□'Γ₁) ⊢[(Hilbert.Grz α)]! □(□(ψ ➝ □ψ) ➝ ψ) := contextual_nec! this; + have : (□'Γ₁) ⊢[(Hilbert.Grz α)]! ψ := axiomGrz! ⨀ this; + have : (□'□'Γ₁) ⊢[(Hilbert.Grz α)]! □ψ := contextual_nec! this; -- TODO: `contextual_axiomFour` - have : 𝐆𝐫𝐳 ⊢! ⋀□'□'Γ₁ ➝ □ψ := provable_iff.mp this; - have : 𝐆𝐫𝐳 ⊢! □□⋀Γ₁ ➝ □ψ := imp_trans''! (imp_trans''! (distribute_multibox_conj! (n := 2)) $ conjconj_subset! (by simp)) this; - have : 𝐆𝐫𝐳 ⊢! □⋀Γ₁ ➝ □ψ := imp_trans''! axiomFour! this; - have : 𝐆𝐫𝐳 ⊢! ⋀□'Γ₁ ➝ □ψ := imp_trans''! collect_box_conj! this; - have : 𝐆𝐫𝐳 ⊢! ⋀□'(X.formulae.prebox.box |>.toList) ➝ □ψ := imp_trans''! (conjconj_subset! (by + have : (Hilbert.Grz α) ⊢! ⋀□'□'Γ₁ ➝ □ψ := provable_iff.mp this; + have : (Hilbert.Grz α) ⊢! □□⋀Γ₁ ➝ □ψ := imp_trans''! (imp_trans''! (distribute_multibox_conj! (n := 2)) $ conjconj_subset! (by simp)) this; + have : (Hilbert.Grz α) ⊢! □⋀Γ₁ ➝ □ψ := imp_trans''! axiomFour! this; + have : (Hilbert.Grz α) ⊢! ⋀□'Γ₁ ➝ □ψ := imp_trans''! collect_box_conj! this; + have : (Hilbert.Grz α) ⊢! ⋀□'(X.formulae.prebox.box |>.toList) ➝ □ψ := imp_trans''! (conjconj_subset! (by simp; intro χ hr; have := hΓ₁ _ hr; simp at this; tauto; )) this; - have : 𝐆𝐫𝐳 ⊢! ⋀□'(X.formulae.prebox.toList) ➝ □ψ := imp_trans''! (conjconj_provable! (by + have : (Hilbert.Grz α) ⊢! ⋀□'(X.formulae.prebox.toList) ➝ □ψ := imp_trans''! (conjconj_provable! (by intro ψ hq; simp at hq; obtain ⟨χ, hr, rfl⟩ := hq; @@ -155,7 +155,7 @@ private lemma Grz_truthlemma.lemma2 apply FiniteContext.by_axm!; simpa; )) this; - have : X.formulae *⊢[𝐆𝐫𝐳]! □ψ := by + have : X.formulae *⊢[(Hilbert.Grz α)]! □ψ := by apply Context.provable_iff.mpr; use □'X.formulae.prebox.toList; constructor; @@ -165,7 +165,7 @@ private lemma Grz_truthlemma.lemma2 contradiction; -- TODO: syntactical proof -private lemma Grz_truthlemma.lemma3 [Inhabited α] : 𝐊𝐓 ⊢! (φ ⋏ □(φ ➝ □φ)) ➝ □φ := by +private lemma Grz_truthlemma.lemma3 [Inhabited α] : (Hilbert.KT α) ⊢! (φ ⋏ □(φ ➝ □φ)) ➝ □φ := by by_contra hC; have := (not_imp_not.mpr $ KT_complete (α := α) |>.complete) hC; simp at this; @@ -233,10 +233,10 @@ lemma Grz_truthlemma [Inhabited α] {X : (GrzCompleteModel φ).World} (q_sub : . simp_all; . apply hY.2; simp; . by_contra hC; - have : ↑X.formulae *⊢[𝐆𝐫𝐳]! ψ := membership_iff (by simp; left; aesop) |>.mp w; - have : ↑X.formulae *⊢[𝐆𝐫𝐳]! □(ψ ➝ □ψ) := membership_iff (by simp; right; assumption) |>.mp hC; - have : ↑X.formulae *⊢[𝐆𝐫𝐳]! (ψ ⋏ □(ψ ➝ □ψ)) ➝ □ψ := Context.of! $ KT_weakerThan_Grz Grz_truthlemma.lemma3; - have : ↑X.formulae *⊢[𝐆𝐫𝐳]! □ψ := this ⨀ and₃'! (by assumption) (by assumption); + have : ↑X.formulae *⊢[(Hilbert.Grz α)]! ψ := membership_iff (by simp; left; aesop) |>.mp w; + have : ↑X.formulae *⊢[(Hilbert.Grz α)]! □(ψ ➝ □ψ) := membership_iff (by simp; right; assumption) |>.mp hC; + have : ↑X.formulae *⊢[(Hilbert.Grz α)]! (ψ ⋏ □(ψ ➝ □ψ)) ➝ □ψ := Context.of! $ Hilbert.KT_weakerThan_Grz Grz_truthlemma.lemma3; + have : ↑X.formulae *⊢[(Hilbert.Grz α)]! □ψ := this ⨀ and₃'! (by assumption) (by assumption); have : □ψ ∈ X.formulae := membership_iff (subformulaeGrz.mem_origin (by assumption)) |>.mpr this; contradiction; . apply ih (by aesop) |>.not.mpr; @@ -252,11 +252,11 @@ lemma Grz_truthlemma [Inhabited α] {X : (GrzCompleteModel φ).World} (q_sub : . exact ih (by aesop) |>.not.mpr w; . intro h Y RXY; apply ih (subformulae.mem_box q_sub) |>.mpr; - have : ↑Y.formulae *⊢[𝐆𝐫𝐳]! □ψ ➝ ψ := Context.of! $ axiomT!; - have : ↑Y.formulae *⊢[𝐆𝐫𝐳]! ψ := this ⨀ (membership_iff (by simp; left; trivial) |>.mp (RXY.1 ψ (by simp; tauto) h)); + have : ↑Y.formulae *⊢[(Hilbert.Grz α)]! □ψ ➝ ψ := Context.of! $ axiomT!; + have : ↑Y.formulae *⊢[(Hilbert.Grz α)]! ψ := this ⨀ (membership_iff (by simp; left; trivial) |>.mp (RXY.1 ψ (by simp; tauto) h)); exact membership_iff (by simp; left; exact subformulae.mem_box q_sub) |>.mpr this; -private lemma Grz_completeAux [Inhabited α] {φ : Formula α} : ReflexiveTransitiveAntisymmetricFrameClass.{u}ꟳ#α ⊧ φ → 𝐆𝐫𝐳 ⊢! φ := by +private lemma Grz_completeAux [Inhabited α] {φ : Formula α} : ReflexiveTransitiveAntisymmetricFrameClass.{u}ꟳ#α ⊧ φ → (Hilbert.Grz α) ⊢! φ := by contrapose; intro h; apply exists_finite_frame.mpr; @@ -275,9 +275,9 @@ private lemma Grz_completeAux [Inhabited α] {φ : Formula α} : ReflexiveTransi apply hX₁; tauto; -instance Grz_complete [Inhabited α] : Complete (𝐆𝐫𝐳 : Hilbert α) (ReflexiveTransitiveAntisymmetricFrameClass.{u}ꟳ#α) := ⟨Grz_completeAux⟩ +instance Grz_complete [Inhabited α] : Complete (Hilbert.Grz α) (ReflexiveTransitiveAntisymmetricFrameClass.{u}ꟳ#α) := ⟨Grz_completeAux⟩ -instance [Inhabited α] : FiniteFrameProperty (α := α) 𝐆𝐫𝐳 ReflexiveTransitiveAntisymmetricFrameClass where +instance [Inhabited α] : FiniteFrameProperty (Hilbert.Grz α) ReflexiveTransitiveAntisymmetricFrameClass where end Kripke diff --git a/Foundation/Modal/Kripke/Grz/Definability.lean b/Foundation/Modal/Kripke/Grz/Definability.lean index 471d1a44..73142853 100644 --- a/Foundation/Modal/Kripke/Grz/Definability.lean +++ b/Foundation/Modal/Kripke/Grz/Definability.lean @@ -178,8 +178,8 @@ instance axiomGrz_defineability : 𝔽((𝗚𝗿𝘇 : Theory α)).DefinedBy Ref simp [WeaklyConverseWellFounded, ConverseWellFounded, IrreflGen]; apply WellFounded.trivial_wellfounded; -instance : Sound (𝐆𝐫𝐳 : Hilbert α) (ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass#α) := inferInstance -instance : System.Consistent (𝐆𝐫𝐳 : Hilbert α) := inferInstance +instance : Sound (Hilbert.Grz α) (ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass#α) := inferInstance +instance : System.Consistent (Hilbert.Grz α) := inferInstance instance axiomGrz_finite_defines : 𝔽ꟳ((𝗚𝗿𝘇 : Theory α)).DefinedBy ReflexiveTransitiveAntisymmetricFrameClassꟳ where define := by @@ -199,7 +199,7 @@ instance axiomGrz_finite_defines : 𝔽ꟳ((𝗚𝗿𝘇 : Theory α)).DefinedBy use ⟨PUnit, λ _ _ => True⟩; refine ⟨?_, ?_, ?_⟩ <;> tauto; -instance : Sound (𝐆𝐫𝐳 : Hilbert α) (ReflexiveTransitiveAntisymmetricFrameClassꟳ#α) := inferInstance +instance : Sound (Hilbert.Grz α) (ReflexiveTransitiveAntisymmetricFrameClassꟳ#α) := inferInstance end Kripke diff --git a/Foundation/Modal/Kripke/S5.lean b/Foundation/Modal/Kripke/S5.lean index 74199153..8b277aa6 100644 --- a/Foundation/Modal/Kripke/S5.lean +++ b/Foundation/Modal/Kripke/S5.lean @@ -17,7 +17,7 @@ lemma iff_Universal_ReflexiveEuclidean_validOnFrameClass : UniversalFrameClass.{ . rintro h F F_univ; exact @h F (⟨refl_of_universal F_univ, eucl_of_universal F_univ⟩); -instance S5_complete_universal [Inhabited α] [DecidableEq α] : Complete 𝐒𝟓 (UniversalFrameClass.{u}#α) := ⟨by +instance S5_complete_universal [Inhabited α] [DecidableEq α] : Complete (Hilbert.S5 α) (UniversalFrameClass.{u}#α) := ⟨by intro φ hF; exact S5_complete.complete $ iff_Universal_ReflexiveEuclidean_validOnFrameClass.mp hF; ⟩ diff --git a/Foundation/Modal/Kripke/Semantics.lean b/Foundation/Modal/Kripke/Semantics.lean index 521c6556..a1886745 100644 --- a/Foundation/Modal/Kripke/Semantics.lean +++ b/Foundation/Modal/Kripke/Semantics.lean @@ -292,7 +292,7 @@ def characterizability_union_frameclass_of_theory {T₁ T₂ : Theory α} abbrev FrameClassOfHilbert (Λ : Hilbert α) : FrameClass.Dep α := 𝔽(Λ.theorems) notation "𝔽(" Λ ")" => FrameClassOfHilbert Λ -instance {Ax : Theory α} {𝔽 : FrameClass} [defi : 𝔽(Ax).DefinedBy 𝔽] : 𝔽(𝜿(Ax)).DefinedBy 𝔽 where +instance {Ax : Theory α} {𝔽 : FrameClass} [defi : 𝔽(Ax).DefinedBy 𝔽] : 𝔽(Hilbert.ExtK Ax).DefinedBy 𝔽 where define := by simp only [Hilbert.theorems, System.theory, Semantics.RealizeSet.setOf_iff, ValidOnFrame.models_iff, Set.mem_setOf_eq]; intro F; @@ -319,7 +319,7 @@ instance {Ax : Theory α} {𝔽 : FrameClass} [defi : 𝔽(Ax).DefinedBy 𝔽] : | exact Formula.Kripke.ValidOnFrame.elimContra; nonempty := defi.nonempty -instance {Ax : Theory α} {𝔽 : FrameClass} [char : 𝔽(Ax).Characteraizable 𝔽] : 𝔽(𝜿(Ax)).Characteraizable 𝔽 where +instance {Ax : Theory α} {𝔽 : FrameClass} [char : 𝔽(Ax).Characteraizable 𝔽] : 𝔽(Hilbert.ExtK Ax).Characteraizable 𝔽 where characterize := by simp only [Hilbert.theorems, System.theory, Semantics.RealizeSet.setOf_iff, ValidOnFrame.models_iff, Set.mem_setOf_eq]; intro F hF φ hp; @@ -343,7 +343,7 @@ instance {Ax : Theory α} {𝔽 : FrameClass} [char : 𝔽(Ax).Characteraizable abbrev FiniteFrameClassOfHilbert (Λ : Hilbert α) : FiniteFrameClass.Dep α := 𝔽(Λ)ꟳ notation "𝔽ꟳ(" Λ ")" => FiniteFrameClassOfHilbert Λ -instance {Ax : Set (Formula α)} {𝔽 : FiniteFrameClass} [defi : 𝔽ꟳ(Ax).DefinedBy 𝔽] : 𝔽ꟳ(𝜿(Ax)).DefinedBy 𝔽 where +instance {Ax : Set (Formula α)} {𝔽 : FiniteFrameClass} [defi : 𝔽ꟳ(Ax).DefinedBy 𝔽] : 𝔽ꟳ(Hilbert.ExtK Ax).DefinedBy 𝔽 where define := by simp only [Hilbert.theorems, System.theory, Semantics.RealizeSet.setOf_iff, ValidOnFrame.models_iff, Set.mem_setOf_eq]; intro F; @@ -370,7 +370,7 @@ instance {Ax : Set (Formula α)} {𝔽 : FiniteFrameClass} [defi : 𝔽ꟳ(Ax). | exact Formula.Kripke.ValidOnFrame.elimContra; nonempty := defi.nonempty -instance {Ax : Set (Formula α)} {𝔽 : FiniteFrameClass} [char : 𝔽ꟳ(Ax).Characteraizable 𝔽] : 𝔽ꟳ(𝜿(Ax)).Characteraizable 𝔽 where +instance {Ax : Set (Formula α)} {𝔽 : FiniteFrameClass} [char : 𝔽ꟳ(Ax).Characteraizable 𝔽] : 𝔽ꟳ(Hilbert.ExtK Ax).Characteraizable 𝔽 where characterize := by simp only [Hilbert.theorems, System.theory, Semantics.RealizeSet.setOf_iff, ValidOnFrame.models_iff, Set.mem_setOf_eq]; intro F hF φ hp; @@ -468,15 +468,15 @@ instance empty_axiom_definability : 𝔽((∅ : Theory α)).DefinedBy AllFrameCl define := by simp; nonempty := ⟨⟨PUnit, λ _ _ => True⟩, trivial⟩ -private instance K_definability' : 𝔽((𝜿(∅) : Hilbert α)).DefinedBy AllFrameClass := inferInstance +private instance K_definability' : 𝔽(((Hilbert.ExtK ∅) : Hilbert α)).DefinedBy AllFrameClass := inferInstance -instance K_definability : 𝔽((𝐊 : Hilbert α)).DefinedBy AllFrameClass := by +instance K_definability : 𝔽(Hilbert.K α).DefinedBy AllFrameClass := by convert K_definability'; - exact K_is_extK_of_empty; + exact Hilbert.ExtK.K_is_extK_of_empty; -instance K_sound : Sound 𝐊 (AllFrameClass#α) := inferInstance +instance K_sound : Sound (Hilbert.K α) (AllFrameClass#α) := inferInstance -instance K_consistent : System.Consistent (𝐊 : Hilbert α) := inferInstance +instance K_consistent : System.Consistent (Hilbert.K α) := inferInstance lemma restrict_finite : 𝔽#α ⊧ φ → 𝔽ꟳ#α ⊧ φ := by @@ -489,7 +489,7 @@ instance {Λ : Hilbert α} [sound : Sound Λ 𝔽#α] : Sound Λ 𝔽ꟳ#α := exact restrict_finite $ sound.sound h; ⟩ -instance : Sound 𝐊 (AllFrameClassꟳ#α) := inferInstance +instance : Sound (Hilbert.K α) (AllFrameClassꟳ#α) := inferInstance lemma exists_finite_frame : ¬𝔽ꟳ#α ⊧ φ ↔ ∃ F ∈ 𝔽ꟳ, ¬F#α ⊧ φ := by simp; @@ -500,14 +500,16 @@ class FiniteFrameProperty (Λ : Hilbert α) (𝔽 : FrameClass) where end Kripke + +namespace Hilbert + section open Formula (atom) open Formula.Kripke open Kripke (K_sound) - -theorem K_strictlyWeakerThan_KD [DecidableEq α] [Inhabited α] : (𝐊 : Hilbert α) <ₛ 𝐊𝐃 := by +theorem K_strictlyWeakerThan_KD [DecidableEq α] [Inhabited α] : (Hilbert.K α) <ₛ (Hilbert.KD α) := by constructor; . apply K_weakerThan_KD; . simp [weakerThan_iff]; @@ -519,7 +521,7 @@ theorem K_strictlyWeakerThan_KD [DecidableEq α] [Inhabited α] : (𝐊 : Hilber use ⟨Fin 1, λ _ _ => False⟩, (λ w _ => w = 0), 0; simp [Satisfies]; -theorem K_strictlyWeakerThan_KB [DecidableEq α] [Inhabited α] : (𝐊 : Hilbert α) <ₛ 𝐊𝐁 := by +theorem K_strictlyWeakerThan_KB [DecidableEq α] [Inhabited α] : (Hilbert.K α) <ₛ (Hilbert.KB α) := by constructor; . apply K_weakerThan_KB; . simp [weakerThan_iff]; @@ -532,7 +534,7 @@ theorem K_strictlyWeakerThan_KB [DecidableEq α] [Inhabited α] : (𝐊 : Hilber simp [Satisfies]; use 1; -theorem K_strictlyWeakerThan_K4 [DecidableEq α] [Inhabited α] : (𝐊 : Hilbert α) <ₛ 𝐊𝟒 := by +theorem K_strictlyWeakerThan_K4 [DecidableEq α] [Inhabited α] : (Hilbert.K α) <ₛ (Hilbert.K4 α) := by constructor; . apply K_weakerThan_K4; . simp [weakerThan_iff]; @@ -553,7 +555,7 @@ theorem K_strictlyWeakerThan_K4 [DecidableEq α] [Inhabited α] : (𝐊 : Hilber . aesop; . use 0; aesop; -theorem K_strictlyWeakerThan_K5 [DecidableEq α] [Inhabited α] : (𝐊 : Hilbert α) <ₛ 𝐊𝟓 := by +theorem K_strictlyWeakerThan_K5 [DecidableEq α] [Inhabited α] : (Hilbert.K α) <ₛ (Hilbert.K5 α) := by constructor; . apply K_weakerThan_K5; . simp [weakerThan_iff]; @@ -567,14 +569,17 @@ theorem K_strictlyWeakerThan_K5 [DecidableEq α] [Inhabited α] : (𝐊 : Hilber use 1; simp; +end + section variable {Ax₁ Ax₂ : Theory α} (𝔽₁ 𝔽₂ : FrameClass) lemma weakerThan_of_subset_FrameClass - [sound₁ : Sound 𝜿Ax₁ 𝔽₁#α] [complete₂ : Complete 𝜿Ax₂ 𝔽₂#α] - (h𝔽 : 𝔽₂ ⊆ 𝔽₁) : 𝜿Ax₁ ≤ₛ 𝜿Ax₂ := by + [sound₁ : Sound (Hilbert.ExtK Ax₁) 𝔽₁#α] [complete₂ : Complete (Hilbert.ExtK Ax₂) 𝔽₂#α] + (h𝔽 : 𝔽₂ ⊆ 𝔽₁) + : (Hilbert.ExtK Ax₁) ≤ₛ (Hilbert.ExtK Ax₂) := by apply System.weakerThan_iff.mpr; intro φ hp; apply complete₂.complete; @@ -582,9 +587,9 @@ lemma weakerThan_of_subset_FrameClass exact sound₁.sound hp $ h𝔽 hF; lemma equiv_of_eq_FrameClass - [sound₁ : Sound 𝜿Ax₁ 𝔽₁#α] [sound₂ : Sound 𝜿Ax₂ 𝔽₂#α] - [complete₁ : Complete 𝜿Ax₁ 𝔽₁#α] [complete₂ : Complete 𝜿Ax₂ 𝔽₂#α] - (h𝔽 : 𝔽₁ = 𝔽₂) : 𝜿Ax₁ =ₛ 𝜿Ax₂ := by + [sound₁ : Sound (Hilbert.ExtK Ax₁) 𝔽₁#α] [sound₂ : Sound (Hilbert.ExtK Ax₂) 𝔽₂#α] + [complete₁ : Complete (Hilbert.ExtK Ax₁) 𝔽₁#α] [complete₂ : Complete (Hilbert.ExtK Ax₂) 𝔽₂#α] + (h𝔽 : 𝔽₁ = 𝔽₂) : (Hilbert.ExtK Ax₁) =ₛ (Hilbert.ExtK Ax₂) := by apply System.Equiv.antisymm_iff.mpr; constructor; . apply weakerThan_of_subset_FrameClass 𝔽₁ 𝔽₂; subst_vars; rfl; @@ -592,9 +597,6 @@ lemma equiv_of_eq_FrameClass end +end Hilbert -end - -end Modal - -end LO +end LO.Modal diff --git a/Foundation/Modal/Kripke/Ver.lean b/Foundation/Modal/Kripke/Ver.lean index f9c6adf4..1c60dd94 100644 --- a/Foundation/Modal/Kripke/Ver.lean +++ b/Foundation/Modal/Kripke/Ver.lean @@ -30,20 +30,20 @@ instance axiomVer_definability : 𝔽((𝗩𝗲𝗿 : Theory α)).DefinedBy (Iso use ⟨PUnit, λ _ _ => False⟩ tauto; -instance Ver_definability : 𝔽((𝐕𝐞𝐫 : Hilbert α)).DefinedBy (IsolatedFrameClass) := inferInstance +instance Ver_definability : 𝔽(Hilbert.Ver α).DefinedBy (IsolatedFrameClass) := inferInstance -instance : Sound 𝐕𝐞𝐫 (IsolatedFrameClass#α) := inferInstance +instance : Sound (Hilbert.Ver α) (IsolatedFrameClass#α) := inferInstance -instance : System.Consistent (𝐕𝐞𝐫 : Hilbert α) := inferInstance +instance : System.Consistent (Hilbert.Ver α) := inferInstance variable [DecidableEq α] -lemma isolated_CanonicalFrame {Ax : Theory α} (h : 𝗩𝗲𝗿 ⊆ Ax) [System.Consistent 𝜿Ax] : Isolated (CanonicalFrame 𝜿Ax) := by +lemma isolated_CanonicalFrame {Ax : Theory α} (h : 𝗩𝗲𝗿 ⊆ Ax) [System.Consistent (Hilbert.ExtK Ax)] : Isolated (CanonicalFrame (Hilbert.ExtK Ax)) := by intro x y rxy; - have : (CanonicalModel 𝜿Ax) ⊧ □⊥ := iff_valid_on_canonicalModel_deducible.mpr $ Normal.maxm! (by aesop); + have : (CanonicalModel (Hilbert.ExtK Ax)) ⊧ □⊥ := iff_valid_on_canonicalModel_deducible.mpr $ (Hilbert.ExtK.maxm!) (by apply h; simp); exact this x _ rxy; -instance : Complete 𝐕𝐞𝐫 (IsolatedFrameClass.{u}#α) := instComplete_of_mem_canonicalFrame IsolatedFrameClass $ by +instance : Complete (Hilbert.Ver α) (IsolatedFrameClass.{u}#α) := instComplete_of_mem_canonicalFrame IsolatedFrameClass $ by apply isolated_CanonicalFrame; tauto; diff --git a/Foundation/Modal/Maximal.lean b/Foundation/Modal/Maximal.lean index 5ee5b6c9..8b60071e 100644 --- a/Foundation/Modal/Maximal.lean +++ b/Foundation/Modal/Maximal.lean @@ -2,9 +2,9 @@ import Foundation.Modal.Hilbert import Foundation.IntProp.Kripke.Semantics /-! - # Maximality of `𝐓𝐫𝐢𝐯` and `𝐕𝐞𝐫` + # Maximality of `Hilbert.Triv α` and `𝐕𝐞𝐫` - `𝐓𝐫𝐢𝐯` and `𝐕𝐞𝐫` are maximal in normal modal Foundation. + `Hilbert.Triv α` and `𝐕𝐞𝐫` are maximal in normal modal Foundation. -/ namespace LO.IntProp @@ -85,6 +85,7 @@ variable {φ : Formula α} open System open Formula +open Hilbert macro_rules | `(tactic| trivial) => `(tactic| first @@ -104,7 +105,7 @@ macro_rules | `(tactic| trivial) => `(tactic| | apply imp_id!; ) -lemma deducible_iff_trivTranslation : 𝐓𝐫𝐢𝐯 ⊢! φ ⭤ φᵀ := by +lemma deducible_iff_trivTranslation : (Hilbert.Triv α) ⊢! φ ⭤ φᵀ := by induction φ using Formula.rec' with | hbox φ ih => simp [TrivTranslation]; @@ -114,7 +115,7 @@ lemma deducible_iff_trivTranslation : 𝐓𝐫𝐢𝐯 ⊢! φ ⭤ φᵀ := by | himp _ _ ih₁ ih₂ => exact imp_replace_iff! ih₁ ih₂; | _ => apply iff_id! -lemma deducible_iff_verTranslation : 𝐕𝐞𝐫 ⊢! φ ⭤ φⱽ := by +lemma deducible_iff_verTranslation : (Hilbert.Ver α) ⊢! φ ⭤ φⱽ := by induction φ using Formula.rec' with | hbox => apply iff_intro!; @@ -136,7 +137,7 @@ lemma of_classical {mΛ : Modal.Hilbert α} {φ : IntProp.Formula α} : (𝐂 exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩); | _ => dsimp [IntProp.Formula.toModalFormula]; trivial; -lemma iff_Triv_classical : 𝐓𝐫𝐢𝐯 ⊢! φ ↔ 𝐂𝐥 ⊢! φᵀᴾ := by +lemma iff_Triv_classical : Hilbert.Triv α ⊢! φ ↔ 𝐂𝐥 ⊢! φᵀᴾ := by constructor; . intro h; induction h using Deduction.inducition_with_necOnly! with @@ -149,11 +150,11 @@ lemma iff_Triv_classical : 𝐓𝐫𝐢𝐯 ⊢! φ ↔ 𝐂𝐥 ⊢! φᵀᴾ : | hNec ih => dsimp [TrivTranslation]; trivial; | _ => dsimp [TrivTranslation]; trivial; . intro h; - have d₁ : 𝐓𝐫𝐢𝐯 ⊢! φᵀ ➝ φ := and₂'! deducible_iff_trivTranslation; - have d₂ : 𝐓𝐫𝐢𝐯 ⊢! φᵀ := by simpa only [TrivTranslation.back] using of_classical h; + have d₁ : Hilbert.Triv α ⊢! φᵀ ➝ φ := and₂'! deducible_iff_trivTranslation; + have d₂ : Hilbert.Triv α ⊢! φᵀ := by simpa only [TrivTranslation.back] using of_classical h; exact d₁ ⨀ d₂; -lemma iff_Ver_classical : 𝐕𝐞𝐫 ⊢! φ ↔ 𝐂𝐥 ⊢! φⱽᴾ := by +lemma iff_Ver_classical : (Hilbert.Ver α) ⊢! φ ↔ 𝐂𝐥 ⊢! φⱽᴾ := by constructor; . intro h; induction h using Deduction.inducition_with_necOnly! with @@ -166,17 +167,17 @@ lemma iff_Ver_classical : 𝐕𝐞𝐫 ⊢! φ ↔ 𝐂𝐥 ⊢! φⱽᴾ := by | hNec => dsimp [VerTranslation]; trivial; | _ => dsimp [VerTranslation]; trivial; . intro h; - have d₁ : 𝐕𝐞𝐫 ⊢! φⱽ ➝ φ := and₂'! deducible_iff_verTranslation; - have d₂ : 𝐕𝐞𝐫 ⊢! φⱽ := by simpa using of_classical h; + have d₁ : (Hilbert.Ver α) ⊢! φⱽ ➝ φ := and₂'! deducible_iff_verTranslation; + have d₂ : (Hilbert.Ver α) ⊢! φⱽ := by simpa using of_classical h; exact d₁ ⨀ d₂; -lemma trivTranslated_of_K4 : 𝐊𝟒 ⊢! φ → 𝐂𝐥 ⊢! φᵀᴾ := by +lemma trivTranslated_of_K4 : (Hilbert.K4 α) ⊢! φ → 𝐂𝐥 ⊢! φᵀᴾ := by intro h; apply iff_Triv_classical.mp; - exact System.weakerThan_iff.mp K4_weakerThan_Triv h; + exact System.weakerThan_iff.mp Hilbert.K4_weakerThan_Triv h; -lemma verTranslated_of_GL : 𝐆𝐋 ⊢! φ → 𝐂𝐥 ⊢! φⱽᴾ := by +lemma verTranslated_of_GL : (Hilbert.GL α) ⊢! φ → 𝐂𝐥 ⊢! φⱽᴾ := by intro h; induction h using Deduction.inducition_with_necOnly! with | hMaxm a => @@ -193,21 +194,21 @@ open IntProp.Kripke (unprovable_classical_of_exists_ClassicalValuation) variable [Inhabited α] -example : 𝐓𝐫𝐢𝐯 ⊬ Axioms.L (atom default : Formula α) := by +example : Hilbert.Triv α ⊬ Axioms.L (atom default : Formula α) := by apply iff_Triv_classical.not.mpr; apply unprovable_classical_of_exists_ClassicalValuation; simp [Axioms.L, TrivTranslation, toPropFormula, IntProp.Formula.Kripke.Satisfies]; use (λ _ => False); tauto; -lemma unprovable_AxiomL_K4 : 𝐊𝟒 ⊬ Axioms.L (atom default : Formula α) := by +lemma unprovable_AxiomL_K4 : Hilbert.K4 α ⊬ Axioms.L (atom default : Formula α) := by apply not_imp_not.mpr trivTranslated_of_K4; apply unprovable_classical_of_exists_ClassicalValuation; simp [Axioms.L, TrivTranslation, toPropFormula, IntProp.Formula.Kripke.Satisfies]; use (λ _ => False); tauto; -theorem K4_strictReducible_GL : (𝐊𝟒 : Hilbert α) <ₛ 𝐆𝐋 := by +theorem K4_strictReducible_GL : (Hilbert.K4 α) <ₛ (Hilbert.GL α) := by dsimp [StrictlyWeakerThan]; constructor; . apply K4_weakerThan_GL; @@ -217,7 +218,7 @@ theorem K4_strictReducible_GL : (𝐊𝟒 : Hilbert α) <ₛ 𝐆𝐋 := by . exact axiomL!; . exact unprovable_AxiomL_K4; -lemma unprovable_AxiomT_GL : 𝐆𝐋 ⊬ Axioms.T (atom default : Formula α) := by +lemma unprovable_AxiomT_GL : (Hilbert.GL α) ⊬ Axioms.T (atom default : Formula α) := by apply not_imp_not.mpr verTranslated_of_GL; apply unprovable_classical_of_exists_ClassicalValuation; simp [Axioms.T, VerTranslation, toPropFormula, IntProp.Formula.Kripke.Satisfies]; @@ -225,13 +226,13 @@ lemma unprovable_AxiomT_GL : 𝐆𝐋 ⊬ Axioms.T (atom default : Formula α) : tauto; -instance instGLConsistencyViaUnprovableAxiomT : System.Consistent (𝐆𝐋 : Hilbert α) := by +instance instGLConsistencyViaUnprovableAxiomT : System.Consistent (Hilbert.GL α) := by apply consistent_iff_exists_unprovable.mpr; existsi (Axioms.T (atom default)); apply unprovable_AxiomT_GL; -theorem not_S4_weakerThan_GL : ¬(𝐒𝟒 : Hilbert α) ≤ₛ 𝐆𝐋 := by +theorem not_S4_weakerThan_GL : ¬(Hilbert.S4 α) ≤ₛ (Hilbert.GL α) := by apply System.not_weakerThan_iff.mpr; existsi (Axioms.T (atom default)); constructor; @@ -239,7 +240,7 @@ theorem not_S4_weakerThan_GL : ¬(𝐒𝟒 : Hilbert α) ≤ₛ 𝐆𝐋 := by . exact unprovable_AxiomT_GL; -example : 𝐕𝐞𝐫 ⊬ (∼(□⊥) : Formula α) := by +example : (Hilbert.Ver α) ⊬ (∼(□⊥) : Formula α) := by apply iff_Ver_classical.not.mpr; apply unprovable_classical_of_exists_ClassicalValuation; dsimp [VerTranslation, toPropFormula, IntProp.Formula.Kripke.Satisfies]; diff --git a/Foundation/Modal/ModalCompanion/Basic.lean b/Foundation/Modal/ModalCompanion/Basic.lean index da6a929a..26003025 100644 --- a/Foundation/Modal/ModalCompanion/Basic.lean +++ b/Foundation/Modal/ModalCompanion/Basic.lean @@ -73,7 +73,7 @@ private lemma provable_efq_of_provable_S4.case_neg_equiv [System.K4 mΛ] : mΛ instance [System.S4 mΛ] : System.K4 mΛ where open provable_efq_of_provable_S4 in -lemma provable_efq_of_provable_S4 [DecidableEq α] (h : 𝐈𝐧𝐭 ⊢! φ) : 𝐒𝟒 ⊢! φᵍ := by +lemma provable_efq_of_provable_S4 [DecidableEq α] (h : 𝐈𝐧𝐭 ⊢! φ) : (Hilbert.S4 α) ⊢! φᵍ := by induction h.some with | eaxm ih => simp_all only [Set.mem_setOf_eq]; diff --git a/Foundation/Modal/ModalCompanion/GMT.lean b/Foundation/Modal/ModalCompanion/GMT.lean index bfebaa09..00a5f4b4 100644 --- a/Foundation/Modal/ModalCompanion/GMT.lean +++ b/Foundation/Modal/ModalCompanion/GMT.lean @@ -12,7 +12,7 @@ variable {α : Type u} [DecidableEq α] [Inhabited α] [Encodable α] variable {iΛ : IntProp.Hilbert α} {mΛ : Modal.Hilbert α} variable {φ ψ χ : IntProp.Formula α} -lemma provable_S4_of_provable_efq : (𝐒𝟒 ⊢! φᵍ) → (𝐈𝐧𝐭 ⊢! φ) := by +lemma provable_S4_of_provable_efq : ((Hilbert.S4 α) ⊢! φᵍ) → (𝐈𝐧𝐭 ⊢! φ) := by contrapose; intro h; @@ -49,7 +49,7 @@ lemma provable_S4_of_provable_efq : (𝐒𝟒 ⊢! φᵍ) → (𝐈𝐧𝐭 ⊢! use F; exact ⟨⟨F_refl, F_trans⟩, by use V, w⟩; -theorem provable_efq_iff_provable_S4 : 𝐈𝐧𝐭 ⊢! φ ↔ 𝐒𝟒 ⊢! φᵍ := ⟨provable_efq_of_provable_S4, provable_S4_of_provable_efq⟩ -instance : ModalCompanion (α := α) 𝐈𝐧𝐭 𝐒𝟒 := ⟨provable_efq_iff_provable_S4⟩ +theorem provable_efq_iff_provable_S4 : 𝐈𝐧𝐭 ⊢! φ ↔ (Hilbert.S4 α) ⊢! φᵍ := ⟨provable_efq_of_provable_S4, provable_S4_of_provable_efq⟩ +instance : ModalCompanion (α := α) 𝐈𝐧𝐭 (Hilbert.S4 α) := ⟨provable_efq_iff_provable_S4⟩ end LO.Modal diff --git a/Foundation/Modal/PLoN/Completeness.lean b/Foundation/Modal/PLoN/Completeness.lean index 70ea86a3..0fe28eee 100644 --- a/Foundation/Modal/PLoN/Completeness.lean +++ b/Foundation/Modal/PLoN/Completeness.lean @@ -69,7 +69,7 @@ lemma complete_of_mem_canonicalFrame {𝔽 : FrameClass α} (hFC : CanonicalFram lemma instComplete_of_mem_canonicalFrame {𝔽 : FrameClass α} (hFC : CanonicalFrame Λ ∈ 𝔽) : Complete Λ 𝔽 := ⟨complete_of_mem_canonicalFrame hFC⟩ -instance : Complete 𝐍 (AllFrameClass.{u, u} α) := instComplete_of_mem_canonicalFrame (by simp) +instance : Complete (Hilbert.N α) (AllFrameClass.{u, u} α) := instComplete_of_mem_canonicalFrame (by simp) end PLoN diff --git a/Foundation/Modal/PLoN/Semantics.lean b/Foundation/Modal/PLoN/Semantics.lean index cdd35c90..e6c30810 100644 --- a/Foundation/Modal/PLoN/Semantics.lean +++ b/Foundation/Modal/PLoN/Semantics.lean @@ -188,7 +188,7 @@ lemma AllFrameClass.nonempty : (AllFrameClass.{_, 0} α).Nonempty := by open Formula -lemma N_defines : 𝐍.DefinesPLoNFrameClass (AllFrameClass α) := by +lemma N_defines : (Hilbert.N α).DefinesPLoNFrameClass (AllFrameClass α) := by intro F; simp [Hilbert.theorems, System.theory, PLoN.ValidOnFrame, PLoN.ValidOnModel]; intro φ hp; diff --git a/Foundation/Modal/PLoN/Soundness.lean b/Foundation/Modal/PLoN/Soundness.lean index 5cc891c8..343a301c 100644 --- a/Foundation/Modal/PLoN/Soundness.lean +++ b/Foundation/Modal/PLoN/Soundness.lean @@ -25,9 +25,9 @@ lemma consistent_of_defines (defines : Λ.DefinesPLoNFrameClass 𝔽) (nonempty exact unprovable_bot_of_nonempty_frameclass defines nonempty; -instance : Sound 𝐍 (AllFrameClass α) := sound_of_defines N_defines +instance : Sound (Hilbert.N α) (AllFrameClass α) := sound_of_defines N_defines -instance : System.Consistent (𝐍 : Hilbert α) := consistent_of_defines N_defines AllFrameClass.nonempty +instance : System.Consistent (Hilbert.N α) := consistent_of_defines N_defines AllFrameClass.nonempty end PLoN