feat(Modal): Basic properties of Translation for 𝐓𝐫𝐢𝐯 and 𝐕𝐞𝐫

Logic/Logic/HilbertStyle/Supplemental.lean

@@ -211,6 +211,11 @@ def tne : 𝓢 ⊢ ~(~~p) ⟶ ~p := contra₀' dni
 def tne' (b : 𝓢 ⊢ ~(~~p)) : 𝓢 ⊢ ~p := tne ⨀ b
 lemma tne'! (b : 𝓢 ⊢! ~(~~p)) : 𝓢 ⊢! ~p := ⟨tne' b.some⟩
 
+def implyLeftReplace (h : 𝓢 ⊢ q ⟶ p) : 𝓢 ⊢ (p ⟶ r) ⟶ (q ⟶ r) := by
+  apply deduct';
+  exact impTrans (of h) id;
+lemma imply_left_replace! (h : 𝓢 ⊢! q ⟶ p) : 𝓢 ⊢! (p ⟶ r) ⟶ (q ⟶ r) := ⟨implyLeftReplace h.some⟩
+
 
 lemma implyLeftReplaceIff'! (h : 𝓢 ⊢! p ⟷ q) : 𝓢 ⊢! p ⟶ r ↔ 𝓢 ⊢! q ⟶ r := by
   constructor;

Logic/Logic/System.lean

@@ -95,6 +95,8 @@ variable {𝓢 : S} {𝓣 : T} {𝓤 : U}
 lemma reducible_iff : 𝓢 ≤ₛ 𝓣 ↔ (∀ {f}, 𝓢 ⊢! f → 𝓣 ⊢! f) :=
   ⟨fun h _ hf ↦ h hf, fun h _ hf ↦ h hf⟩
 
+lemma not_reducible_iff : ¬𝓢 ≤ₛ 𝓣 ↔ (∃ f, 𝓢 ⊢! f ∧ 𝓣 ⊬! f) := by simp [reducible_iff, Unprovable];
+
 lemma strictReducible_iff : 𝓢 <ₛ 𝓣 ↔ (∀ {f}, 𝓢 ⊢! f → 𝓣 ⊢! f) ∧ (∃ f, 𝓢 ⊬! f ∧ 𝓣 ⊢! f) := by
   simp [StrictReducible, reducible_iff]; intro _
   exact exists_congr (fun _ ↦ by simp [and_comm])

Logic/Modal/Standard.lean

@@ -1,4 +1,5 @@
 import Logic.Modal.Standard.Boxdot
+import Logic.Modal.Standard.Maximal
 
 import Logic.Modal.Standard.Kripke.Morphism
 import Logic.Modal.Standard.Kripke.Soundness

Logic/Modal/Standard/Boxdot.lean

@@ -7,6 +7,7 @@ variable [DecidableEq α]
 
 def Formula.BoxdotTranslation : Formula α → Formula α
   | atom p => .atom p
+  | ⊤ => ⊤
   | ⊥ => ⊥
   | p ⟶ q => (BoxdotTranslation p) ⟶ (BoxdotTranslation q)
   | p ⋏ q => (BoxdotTranslation p) ⋏ (BoxdotTranslation q)
@@ -36,7 +37,7 @@ lemma boxdotTranslatedK4_of_S4 (h : 𝐒𝟒 ⊢! p) : 𝐊𝟒 ⊢! pᵇ := by
   | _ =>
     dsimp [BoxdotTranslation];
     try first
-    | apply imp_id!;
+    | apply verum!;
     | apply conj₁!;
     | apply conj₂!;
     | apply conj₃!;

Logic/Modal/Standard/Deduction.lean

@@ -2,6 +2,7 @@ import Logic.Logic.HilbertStyle.Basic
 import Logic.Logic.HilbertStyle.Supplemental
 import Logic.Modal.Standard.System
 import Logic.Modal.Standard.Formula
+import Logic.Modal.Standard.HilbertStyle
 
 namespace LO.Modal.Standard
 
@@ -194,7 +195,8 @@ instance : Normal (α := α) 𝐊𝐓𝟒𝐁 where
 protected abbrev GL : DeductionParameter α := NecOnly (𝗞 ∪ 𝗟)
 notation "𝐆𝐋" => DeductionParameter.GL
 instance : Normal (α := α) 𝐆𝐋 where
-
+instance : System.GL (𝐆𝐋 : DeductionParameter α) where
+  L _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp)
 
 protected abbrev S4Dot2 : DeductionParameter α := NecOnly (𝗞 ∪ 𝗧 ∪ 𝟰 ∪ .𝟮)
 notation "𝐒𝟒.𝟐" => DeductionParameter.S4Dot2
@@ -211,6 +213,20 @@ notation "𝐒𝟒𝐆𝐫𝐳" => DeductionParameter.S4Grz
 instance : Normal (α := α) 𝐒𝟒𝐆𝐫𝐳 where
 
 
+protected abbrev Triv : DeductionParameter α := NecOnly (𝗞 ∪ 𝗧 ∪ 𝗧𝗰)
+notation "𝐓𝐫𝐢𝐯" => DeductionParameter.Triv
+instance : Normal (α := α) 𝐓𝐫𝐢𝐯 where
+instance : System.Triv (𝐓𝐫𝐢𝐯 : DeductionParameter α) 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 : DeductionParameter α := NecOnly (𝗞 ∪ 𝗩𝗲𝗿)
+notation "𝐕𝐞𝐫" => DeductionParameter.Ver
+instance : Normal (α := α) 𝐕𝐞𝐫 where
+instance : System.Ver (𝐕𝐞𝐫 : DeductionParameter α) where
+  Ver _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp)
+
+
 /-- Logic of Pure Necessitation -/
 protected abbrev N : DeductionParameter α := NecOnly ∅
 notation "𝐍" => DeductionParameter.N
@@ -233,4 +249,42 @@ end DeductionParameter
 
 @[simp] lemma reducible_K_GL : (𝐊 : DeductionParameter α) ≤ₛ 𝐆𝐋 := by simp
 
+open System
+
+lemma normal_reducible
+  {𝓓₁ 𝓓₂ : DeductionParameter α} [𝓓₁.Normal] [𝓓₂.Normal]
+  (hsubset : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p) : (𝓓₁ : DeductionParameter α) ≤ₛ 𝓓₂ := by
+  apply System.reducible_iff.mpr;
+  intro p h;
+  induction h.some using Deduction.inducition_with_nec with
+  | hMaxm hp => exact hsubset hp;
+  | hMdp hpq hp ihpq ihp => exact (ihpq ⟨hpq⟩) ⨀ (ihp ⟨hp⟩)
+  | hNec hp ihp => exact Necessitation.nec! (ihp ⟨hp⟩)
+  | _ =>
+    try first
+    | apply verum!;
+    | apply imply₁!;
+    | apply imply₂!;
+    | apply conj₁!;
+    | apply conj₂!;
+    | apply conj₃!;
+    | apply disj₁!;
+    | apply disj₂!;
+    | apply disj₃!;
+    | apply dne!;
+
+lemma reducible_K4_Triv : (𝐊𝟒 : DeductionParameter α) ≤ₛ 𝐓𝐫𝐢𝐯 := by
+  apply normal_reducible;
+  intro p hp;
+  rcases hp with (hK | hFour)
+  . obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
+  . obtain ⟨_, _, e⟩ := hFour; subst_vars; exact axiomFour!;
+
+lemma reducible_K4_GL : (𝐊𝟒 : DeductionParameter α) ≤ₛ 𝐆𝐋 := by
+  apply normal_reducible;
+  intro p hp;
+  rcases hp with (hK | hFour)
+  . obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
+  . obtain ⟨_, _, e⟩ := hFour; subst_vars; exact axiomFour!;
+
 end LO.Modal.Standard

Logic/Modal/Standard/Formula.lean

@@ -6,6 +6,7 @@ namespace LO.Modal.Standard
 
 inductive Formula (α : Type u) : Type u where
   | atom   : α → Formula α
+  | verum  : Formula α
   | falsum : Formula α
   | imp    : Formula α → Formula α → Formula α
   | and    : Formula α → Formula α → Formula α
@@ -19,8 +20,6 @@ variable {α : Type u}
 
 @[simp] def neg (p : Formula α) : Formula α := imp p falsum
 
-@[simp] def verum : Formula α := neg falsum
-
 @[simp] def dia (p : Formula α) : Formula α := neg (box (neg p))
 
 instance : StandardModalLogicalConnective (Formula α) where
@@ -82,6 +81,7 @@ lemma dia_eq (p : Formula α) : ◇p = ~(□(~p)) := rfl
 
 def complexity : Formula α → ℕ
 | atom _  => 0
+| ⊤       => 0
 | ⊥       => 0
 | p ⟶ q   => max p.complexity q.complexity + 1
 | p ⋏ q   => max p.complexity q.complexity + 1
@@ -98,15 +98,36 @@ def complexity : Formula α → ℕ
 @[simp] lemma complexity_box (p : Formula α) : complexity (□p) = p.complexity + 1 := rfl
 @[simp] lemma complexity_box' (p : Formula α) : complexity (box p) = p.complexity + 1 := rfl
 
+/-- Max numbers of `□` -/
+def degree : Formula α → Nat
+  | atom _ => 0
+  | ⊤ => 0
+  | ⊥ => 0
+  | box p => p.degree + 1
+  | p ⟶ q => max p.degree q.degree
+  | p ⋏ q => max p.degree q.degree
+  | p ⋎ q => max p.degree q.degree
+
+@[simp] lemma degree_bot : degree (⊥ : Formula α) = 0 := rfl
+@[simp] lemma degree_top : degree (⊤ : Formula α) = 0 := rfl
+@[simp] lemma degree_atom {a : α} : degree (atom a) = 0 := rfl
+@[simp] lemma degree_imp {p q : Formula α} : degree (p ⟶ q) = max p.degree q.degree := rfl
+@[simp] lemma degree_box {p : Formula α} : degree (□p) = p.degree + 1 := rfl
+@[simp] lemma degree_and {p q : Formula α} : degree (p ⋏ q) = max p.degree q.degree := rfl
+@[simp] lemma degree_or {p q : Formula α} : degree (p ⋎ q) = max p.degree q.degree := rfl
+@[simp] lemma degree_not {p : Formula α} : degree (~p) = p.degree := by simp [NegDefinition.neg]
+
 @[elab_as_elim]
 def cases' {C : Formula α → Sort w}
+    (hVerum  : C ⊤)
     (hfalsum : C ⊥)
     (hatom   : ∀ a : α, C (atom a))
     (himp    : ∀ (p q : Formula α), C (p ⟶ q))
     (hand    : ∀ (p q : Formula α), C (p ⋏ q))
     (hor     : ∀ (p q : Formula α), C (p ⋎ q))
     (hbox    : ∀ (p : Formula α), C (□p))
     : (p : Formula α) → C p
+  | ⊤       => hVerum
   | ⊥       => hfalsum
   | atom a  => hatom a
   | p ⟶ q  => himp p q
@@ -116,19 +137,21 @@ def cases' {C : Formula α → Sort w}
 
 @[elab_as_elim]
 def rec' {C : Formula α → Sort w}
+  (hVerum  : C ⊤)
   (hfalsum : C ⊥)
   (hatom   : ∀ a : α, C (atom a))
   (himp    : ∀ (p q : Formula α), C p → C q → C (p ⟶ q))
   (hand   : ∀ (p q : Formula α), C p → C q → C (p ⋏ q))
   (hor    : ∀ (p q : Formula α), C p → C q → C (p ⋎ q))
   (hbox    : ∀ (p : Formula α), C p → C (□p))
   : (p : Formula α) → C p
+  | ⊤      => hVerum
   | ⊥      => hfalsum
   | atom a => hatom a
-  | p ⟶ q  => himp p q (rec' hfalsum hatom himp hand hor hbox p) (rec' hfalsum hatom himp hand hor hbox q)
-  | p ⋏ q  => hand p q (rec' hfalsum hatom himp hand hor hbox p) (rec' hfalsum hatom himp hand hor hbox q)
-  | p ⋎ q  => hor p q (rec' hfalsum hatom himp hand hor hbox p) (rec' hfalsum hatom himp hand hor hbox q)
-  | box p     => hbox p (rec' hfalsum hatom himp hand hor hbox p)
+  | p ⟶ q  => himp p q (rec' hVerum hfalsum hatom himp hand hor hbox p) (rec' hVerum hfalsum hatom himp hand hor hbox q)
+  | p ⋏ q  => hand p q (rec' hVerum hfalsum hatom himp hand hor hbox p) (rec' hVerum hfalsum hatom himp hand hor hbox q)
+  | p ⋎ q  => hor p q (rec' hVerum hfalsum hatom himp hand hor hbox p) (rec' hVerum hfalsum hatom himp hand hor hbox q)
+  | box p     => hbox p (rec' hVerum hfalsum hatom himp hand hor hbox p)
 
 -- @[simp] lemma complexity_neg (p : Formula α) : complexity (~p) = p.complexity + 1 :=
 --   by induction p using rec' <;> try { simp[neg_eq, neg, *]; rfl;}
@@ -138,6 +161,9 @@ section Decidable
 variable [DecidableEq α]
 
 def hasDecEq : (p q : Formula α) → Decidable (p = q)
+  | ⊤, q => by
+    cases q using cases' <;>
+    { simp; try { exact isFalse not_false }; try { exact isTrue trivial } }
   | ⊥, q => by
     cases q using cases' <;>
     { simp; try { exact isFalse not_false }; try { exact isTrue trivial } }
@@ -240,6 +266,12 @@ notation "𝗖𝗗" => AxiomSet.CD
 protected abbrev C4 : AxiomSet α := { Axioms.C4 p | p }
 notation "𝗖𝟰" => AxiomSet.C4
 
+protected abbrev Ver : AxiomSet α := { Axioms.Ver p | p }
+notation "𝗩𝗲𝗿" => AxiomSet.Ver
+
+protected abbrev Tc : AxiomSet α := { Axioms.Tc p | p }
+notation "𝗧𝗰" => AxiomSet.Tc
+
 end AxiomSet
 
 end LO.Modal.Standard

Logic/Modal/Standard/HilbertStyle.lean

@@ -290,6 +290,8 @@ lemma boxdot_nec! (d : 𝓢 ⊢! p) : 𝓢 ⊢! ⊡p := ⟨boxdotNec d.some⟩
 def boxdotBox : 𝓢 ⊢ ⊡p ⟶ □p := by exact conj₂;
 lemma boxdot_box! : 𝓢 ⊢! ⊡p ⟶ □p := ⟨boxdotBox⟩
 
+def BoxBoxdot_BoxDotbox : 𝓢 ⊢ □⊡p ⟶ ⊡□p := impTrans distribute_box_and (impId _)
+lemma boxboxdot_boxdotbox : 𝓢 ⊢! □⊡p ⟶ ⊡□p := ⟨BoxBoxdot_BoxDotbox⟩
 
 def axiomT [HasAxiomT 𝓢] : 𝓢 ⊢ □p ⟶ p := HasAxiomT.T _
 @[simp] lemma axiomT! [HasAxiomT 𝓢] : 𝓢 ⊢! □p ⟶ p := ⟨axiomT⟩
@@ -321,12 +323,16 @@ def axiomFour [HasAxiomFour 𝓢] : 𝓢 ⊢ □p ⟶ □□p := HasAxiomFour.Fo
 instance [HasAxiomFour 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomFour Γ := ⟨fun _ ↦ FiniteContext.of axiomFour⟩
 instance [HasAxiomFour 𝓢] (Γ : Context F 𝓢) : HasAxiomFour Γ := ⟨fun _ ↦ Context.of axiomFour⟩
 
+def imply_BoxBoxdot_Box: 𝓢 ⊢  □⊡p ⟶ □p := by
+  simp [boxdot];
+  exact impTrans distribute_box_and conj₁
+@[simp] lemma imply_boxboxdot_box : 𝓢 ⊢! □⊡p ⟶ □p := ⟨imply_BoxBoxdot_Box⟩
 
 def iff_Box_BoxBoxdot [HasAxiomFour 𝓢] : 𝓢 ⊢ □p ⟷ □⊡p := by
   simp [boxdot];
   apply iffIntro;
   . exact impTrans (implyRightAnd (impId _) axiomFour) collect_box_and
-  . exact impTrans distribute_box_and conj₁
+  . exact imply_BoxBoxdot_Box;
 @[simp] lemma iff_box_boxboxdot! [HasAxiomFour 𝓢] : 𝓢 ⊢! □p ⟷ □⊡p := ⟨iff_Box_BoxBoxdot⟩
 
 def iff_Box_BoxdotBox [HasAxiomFour 𝓢] : 𝓢 ⊢ □p ⟷ ⊡□p := by
@@ -358,9 +364,53 @@ def axiomFive [HasAxiomFive 𝓢] : 𝓢 ⊢ ◇p ⟶ □◇p := HasAxiomFive.Fi
 instance [HasAxiomFive 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomFive Γ := ⟨fun _ ↦ FiniteContext.of axiomFive⟩
 instance [HasAxiomFive 𝓢] (Γ : Context F 𝓢) : HasAxiomFive Γ := ⟨fun _ ↦ Context.of axiomFive⟩
 
+
+def axiomTc [HasAxiomTc 𝓢] : 𝓢 ⊢ p ⟶ □p := HasAxiomTc.Tc _
+@[simp] lemma axiomTc! [HasAxiomTc 𝓢] : 𝓢 ⊢! p ⟶ □p := ⟨axiomTc⟩
+
+instance [HasAxiomTc 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomTc Γ := ⟨fun _ ↦ FiniteContext.of axiomTc⟩
+instance [HasAxiomTc 𝓢] (Γ : Context F 𝓢) : HasAxiomTc Γ := ⟨fun _ ↦ Context.of axiomTc⟩
+
+private def axiomFour_of_Tc [HasAxiomTc 𝓢]  : 𝓢 ⊢ Axioms.Four p := axiomTc
+instance [HasAxiomTc 𝓢] : HasAxiomFour 𝓢 := ⟨fun _ ↦ axiomFour_of_Tc⟩
+
+
+
+
+def axiomVer [HasAxiomVer 𝓢] : 𝓢 ⊢ □p := HasAxiomVer.Ver _
+@[simp] lemma axiomVer! [HasAxiomVer 𝓢] : 𝓢 ⊢! □p := ⟨axiomVer⟩
+
+instance [HasAxiomVer 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomVer Γ := ⟨fun _ ↦ FiniteContext.of axiomVer⟩
+instance [HasAxiomVer 𝓢] (Γ : Context F 𝓢) : HasAxiomVer Γ := ⟨fun _ ↦ Context.of axiomVer⟩
+
+private def axiomTc_of_Ver [HasAxiomVer 𝓢] : 𝓢 ⊢ Axioms.Tc p := dhyp _ axiomVer
+instance [HasAxiomVer 𝓢] : HasAxiomTc 𝓢 := ⟨fun _ ↦ axiomTc_of_Ver⟩
+
+private def axiomL_of_Ver [HasAxiomVer 𝓢] : 𝓢 ⊢ Axioms.L p := dhyp _ axiomVer
+instance [HasAxiomVer 𝓢] : HasAxiomL 𝓢 := ⟨fun _ ↦ axiomL_of_Ver⟩
+
 -- axiomTriv : 𝓢 ⊢ p ⟶ □p はネセシテーションを無意味にするはず
 -- instance [Necessitation 𝓢] (Γ : FiniteContext F 𝓢) (h : 𝓢 ⊢ Γ.ctx.conj ⟶ □Γ.ctx.conj) : Necessitation Γ := ⟨
 --   by intro p hp; exact ofDef $ impTrans h (implyBoxDistribute' $ toDef hp);
 -- ⟩
 
+
+def axiomL [HasAxiomL 𝓢] : 𝓢 ⊢ □(□p ⟶ p) ⟶ □p := HasAxiomL.L _
+@[simp] lemma axiomL! [HasAxiomL 𝓢] : 𝓢 ⊢! □(□p ⟶ p) ⟶ □p := ⟨axiomL⟩
+
+instance [HasAxiomL 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomL Γ := ⟨fun _ ↦ FiniteContext.of axiomL⟩
+instance [HasAxiomL 𝓢] (Γ : Context F 𝓢) : HasAxiomL Γ := ⟨fun _ ↦ Context.of axiomL⟩
+
+private def axiomFour_of_L [HasAxiomL 𝓢] : 𝓢 ⊢ Axioms.Four p := by
+  dsimp [Axioms.Four];
+  have : 𝓢 ⊢ p ⟶ (⊡□p ⟶ ⊡p) := by
+    dsimp [boxdot];
+    apply deduct';
+    apply deduct;
+    exact conj₃' (FiniteContext.byAxm) (conj₁' (q := □□p) $ FiniteContext.byAxm);
+  have : 𝓢 ⊢ p ⟶ (□⊡p ⟶ ⊡p) := impTrans this (implyLeftReplace BoxBoxdot_BoxDotbox);
+  exact impTrans (impTrans (implyBoxDistribute' this) axiomL) (implyBoxDistribute' $ conj₂);
+
+instance [HasAxiomL 𝓢] : HasAxiomFour 𝓢 := ⟨fun _ ↦ axiomFour_of_L⟩
+
 end LO.System

Logic/Modal/Standard/Kripke/Completeness.lean

@@ -264,6 +264,9 @@ lemma membership_iff : (p ∈ Ω.theory) ↔ (Ω.theory *⊢[L]! p) := by
 @[simp]
 lemma not_mem_falsum : ⊥ ∉ Ω.theory := not_mem_falsum_of_Lconsistent Ω.consistent
 
+@[simp]
+lemma mem_verum : ⊤ ∈ Ω.theory := by apply membership_iff.mpr; apply verum!;
+
 @[simp]
 lemma unprovable_falsum : Ω.theory *⊬[L]! ⊥ := by apply membership_iff.not.mp; simp
 
@@ -614,6 +617,7 @@ lemma truthlemma : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ (p ∈ Ω.t
       apply ih.mpr;
       exact CanonicalFrame.frame_def_box.mp hΩ' h;
   | hfalsum => simp [Formula.Kripke.Satisfies.bot_def (M := (CanonicalModel L))];
+  | hVerum => simp [Formula.Kripke.Satisfies.top_def (M := (CanonicalModel L))];
   | _ => simp_all
 
 lemma iff_valid_on_canonicalModel_deducible : (CanonicalModel L) ⊧ p ↔ (L ⊢! p) := by

Logic/Modal/Standard/Kripke/GL/Definability.lean

@@ -109,6 +109,6 @@ instance : FiniteFrameClass.IsNonempty (𝔽ꟳ(Ax(𝐆𝐋)) : FiniteFrameClass
       |>.mpr;
     simp [Transitive, Irreflexive];
 
-instance : System.Consistent (𝐆𝐋 : DeductionParameter α) := inferInstance
+instance instGLConsistencyViaFrameClassNonemptiness : System.Consistent (𝐆𝐋 : DeductionParameter α) := inferInstance
 
 end LO.Modal.Standard

Logic/Modal/Standard/Kripke/Semantics.lean

@@ -102,6 +102,7 @@ open Standard.Kripke
 
 def Formula.Kripke.Satisfies (M : Kripke.Model α) (w : M.World) : Formula α → Prop
   | atom a  => M.Valuation w a
+  | verum   => True
   | falsum  => False
   | and p q => (Kripke.Satisfies M w p) ∧ (Kripke.Satisfies M w q)
   | or p q  => (Kripke.Satisfies M w p) ∨ (Kripke.Satisfies M w q)