feat(Normal Modal): Strength of Logics Part.1 (iehality#23)

* feat(Normal Modal): semantics lemmata and explicit soundness proof

* refactor(Normal Modal): satisfy notation

* feat(Normal Modal): Logic equivalence, `𝐒𝟓 = 𝐊𝐓𝟒𝐁`

* refactor(Normal Modal):FrameClassDefinability

* refactor(Normal Modal):

* feat(wip): string soundness wip

* feat(Normal Modal): StrictLogicalStrong, `𝐒𝟒 <ᴸ 𝐒𝟓`

* refactor(Normal Modal): consequence and remove nonempty

* fix(Normal Modal)

* fix(Normal Modal)

* refactor(Normal Modal): remove Proof/Provable

* feat(Normal Modal): DeducibleEquivalent wip

* strict sounds

* fix for review

* rebase fix

Logic/Logic/Deduction.lean

@@ -224,7 +224,7 @@ def neg_iff' {Γ p q} (d : Bew Γ (p ⟷ q)) : Bew Γ (~p ⟷ ~q) := by
   . apply contra₀';
     apply iff_mp' d
 
-def trans' {Γ p q r} (h₁ : Bew Γ (p ⟶ q)) (h₂ : Bew Γ (q ⟶ r)) : Bew Γ (p ⟶ r) := by
+def imp_trans' {Γ p q r} (h₁ : Bew Γ (p ⟶ q)) (h₂ : Bew Γ (q ⟶ r)) : Bew Γ (p ⟶ r) := by
   apply dtr;
   have : Bew (insert p Γ) p := axm (by simp);
   have : Bew (insert p Γ) q := modus_ponens' (weakening' (by simp) h₁) this;
@@ -265,6 +265,14 @@ def conj_symm (Γ p q) : Bew Γ ((p ⋏ q) ⟶ (q ⋏ p)) := by
 
 def conj_symm_iff (Γ p q) : Bew Γ ((p ⋏ q) ⟷ (q ⋏ p)) := iff_intro (by apply conj_symm) (by apply conj_symm)
 
+def iff_id (Γ p) : Bew Γ (p ⟷ p) := iff_intro (by apply imp_id) (by apply imp_id)
+
+def imp_top {Γ p} (d : Bew Γ (⊤ ⟶ p)) : Bew Γ p := d ⨀ (verum Γ)
+
+def iff_left_top {Γ p} (d : Bew Γ (⊤ ⟷ p)) : Bew Γ p := imp_top (iff_mp' d)
+
+def iff_right_top {Γ p} (d : Bew Γ (p ⟷ ⊤)) : Bew Γ p := imp_top (iff_mpr' d)
+
 end Minimal
 
 section Classical
@@ -388,6 +396,15 @@ lemma dtl_not! {Γ : Set F} {p q : F} : ((insert p Γ) ⊬! q) → (Γ ⊬! (p 
   intro d;
   exact ⟨dtl d⟩
 
+lemma imp_id! (Γ : Set F) (p : F) : Γ ⊢! (p ⟶ p) := ⟨imp_id Γ p⟩
+
+lemma imp_top! {Γ : Set F} {p : F} (d : Γ ⊢! (⊤ ⟶ p)) : Γ ⊢! p := ⟨imp_top d.some⟩
+
+lemma iff_left_top! {Γ : Set F} {p : F} (d : Γ ⊢! (⊤ ⟷ p)) : Γ ⊢! p := ⟨iff_left_top d.some⟩
+lemma iff_right_top! {Γ : Set F} {p : F} (d : Γ ⊢! (p ⟷ ⊤)) : Γ ⊢! p := ⟨iff_right_top d.some⟩
+
+lemma imp_trans'! {Γ : Set F} {p q r : F} (h₁ : Γ ⊢! (p ⟶ q)) (h₂ : Γ ⊢! (q ⟶ r)) : Γ ⊢! (p ⟶ r) := ⟨imp_trans' h₁.some h₂.some⟩
+
 end Deducible
 
 section Consistency

Logic/Modal/Normal.lean

@@ -6,7 +6,7 @@ import Logic.Modal.Normal.Deduction
 import Logic.Modal.Normal.Semantics
 import Logic.Modal.Normal.Soundness
 import Logic.Modal.Normal.Completeness
--- import Logic.Modal.Normal.ModalCube
+import Logic.Modal.Normal.ModalCube
 
 import Logic.Modal.Normal.GL.Semantics
 import Logic.Modal.Normal.GL.Soundness

Logic/Modal/Normal/Completeness.lean

@@ -1,5 +1,6 @@
 import Logic.Modal.Normal.Deduction
 import Logic.Modal.Normal.Semantics
+import Logic.Modal.Normal.Soundness
 
 namespace LO.Modal.Normal
 
@@ -18,7 +19,7 @@ variable (Λ : AxiomSet β) (Γ : Theory β)
 
 def Theory.Maximal := ∀ p, (p ∈ Γ) ∨ (~p ∈ Γ)
 
-def WeakCompleteness := ∀ (p : Formula β), (⊧ᴹ[(𝔽(Λ) : FrameClass α)] p) → (⊢ᴹ[Λ]! p)
+-- def WeakCompleteness := ∀ (p : Formula β), (⊧ᴹ[(𝔽(Λ) : FrameClass α)] p) → (∅ ⊢ᴹ[Λ]! p)
 
 def Completeness (𝔽 : FrameClass α) := ∀ (Γ : Theory β) (p : Formula β), (Γ ⊨ᴹ[𝔽] p) → (Γ ⊢ᴹ[Λ]! p)
 
@@ -300,9 +301,15 @@ lemma exists_maximal_consistent_theory : ∃ (Ω : MaximalConsistentTheory Λ),
 
 end Lindenbaum
 
+variable (hK : 𝐊 ⊆ Λ)
+
 open MaximalConsistentTheory
 
-variable (hK : 𝐊 ⊆ Λ)
+/-
+lemma MaximalConsistentTheory.inhabited (h : AxiomSet.Consistent Λ) : Inhabited (MaximalConsistentTheory Λ) := ⟨
+  exists_maximal_consistent_theory (by simp only [Theory.Consistent, Theory.Inconsistent];) |>.choose
+⟩
+-/
 
 lemma mct_mem_box_iff {Ω : MaximalConsistentTheory Λ} {p : Formula β} : (□p ∈ Ω) ↔ (∀ (Ω' : MaximalConsistentTheory Λ), (□⁻¹Ω ⊆ Ω'.theory) → (p ∈ Ω')) := by
   have := Deduction.instBoxedNecessitation hK;

Logic/Modal/Normal/Deduction.lean

@@ -42,15 +42,6 @@ notation:45 Γ " ⊢ᴹ[" Λ "]! " p => Deducible Λ Γ p
 abbrev Undeducible := ¬(Γ ⊢ᴹ[Λ]! p)
 notation:45 Γ " ⊬ᴹ[" Λ "]! " p => Undeducible Λ Γ p
 
-abbrev Proof := ∅ ⊢ᴹ[Λ] p
-notation:45 "⊢ᴹ[" Λ "] " p => Proof Λ p
-
-abbrev Provable := Nonempty (⊢ᴹ[Λ] p)
-notation:45 "⊢ᴹ[" Λ "]! " p => Provable Λ p
-
-abbrev Unprovable := IsEmpty (⊢ᴹ[Λ] p)
-notation:45 "⊬ᴹ[" Λ "]! " p => Unprovable Λ p
-
 abbrev Theory.Consistent := Deduction.Consistent (@Deduction α Λ) Γ
 abbrev Theory.Inconsistent := Deduction.Inconsistent (@Deduction α Λ) Γ
 
@@ -210,52 +201,6 @@ lemma compact {Γ p} (d : Γ ⊢ᴹ[Λ]! p) : ∃ (Δ : Context α), ↑Δ ⊆ 
 
 end Deducible
 
-def Proof.length (d : ⊢ᴹ[Λ] p) : ℕ := Deduction.length (by simpa using d)
-
-lemma Provable.dne : (⊢ᴹ[Λ]! ~~p) → (⊢ᴹ[Λ]! p) := by
-  intro d;
-  have h₁ : ⊢ᴹ[Λ] ~~p ⟶ p := Deduction.dne ∅ p;
-  have h₂ := d.some; simp [Proof, Deduction] at h₂;
-  simp_all [Provable, Proof, Deduction];
-  exact ⟨(Deduction.modus_ponens' h₁ h₂)⟩
-
-lemma Provable.consistent_no_bot : (⊬ᴹ[Λ]! ⊥) → (⊥ ∉ Λ) := by
-  intro h; by_contra hC;
-  have : ⊢ᴹ[Λ]! ⊥ := ⟨Deduction.maxm hC⟩;
-  aesop;
-
--- TODO: 直接有限モデルを構成する方法（鹿島『コンピュータサイエンスにおける様相論理』2.8参照）で必要になる筈の定義だが，使わないかも知れない．
-/-
-section
-
-variable [IsCommutative _ (λ (p q : Formula α) => p ⋏ q)]
-         [IsCommutative _ (λ (p q : Formula α) => p ⋎ q)]
-         [IsAssociative _ (λ (p q : Formula α) => p ⋏ q)]
-         [IsAssociative _ (λ (p q : Formula α) => p ⋎ q)]
-
-def Sequent (Γ Δ : (Theory α)) : Formula α := ((Γ.fold (· ⋏ ·) ⊤ id) ⟶ (Δ.fold (· ⋎ ·) ⊥ id))
-
-notation "⟪" Γ "⟹" Δ "⟫" => Sequent Γ Δ
-
-notation "⟪" "⟹" Δ "⟫" => Sequent ∅ Δ
-
-notation "⟪" Γ "⟹" "⟫" => Sequent Γ ∅
-
-def ProofS (Γ Δ : (Theory α)) := ⊢ᴹ[Λ] ⟪Γ ⟹ Δ⟫
-
-variable [Union ((Theory α))] [Inter ((Theory α))]
-variable (Γ₁ Γ₂ Δ : (Theory α))
-
-structure Partial where
-  union : (Γ₁ ∪ Γ₂) = Δ
-  inter : (Γ₁ ∩ Γ₂) = ∅
-
-structure UnprovablePartial extends Partial Γ₁ Γ₂ Δ where
-  unprovable := ⊬ᴹ[Λ]! ⟪Γ₁ ⟹ Γ₂⟫
-
-end
--/
-
 variable [DecidableEq α]
 
 open Deduction Hilbert
@@ -328,6 +273,144 @@ def Deduction.ofS5Subset (_ : 𝐒𝟓 ⊆ Λ) : (Hilbert.S5 (Deduction (Λ : Ax
 instance : Hilbert.S5 (Deduction (𝐒𝟓 : AxiomSet α)) := Deduction.ofS5Subset 𝐒𝟓 (by rfl)
 -/
 
+namespace Formula
+
+open LO.Hilbert
+
+def DeducibleEquivalent (Λ : AxiomSet α) (Γ : Theory α) (p q : Formula α) : Prop := Γ ⊢ᴹ[Λ]! (p ⟷ q)
+notation p:80 " ⟷[" Λ "," Γ "] " q:80 => DeducibleEquivalent Λ Γ p q
+
+namespace DeducibleEquivalent
+
+variable {Λ : AxiomSet α} {Γ : Theory α} {p q r : Formula α}
+
+@[refl]
+protected lemma refl : p ⟷[Λ, Γ] p := by
+  simp [DeducibleEquivalent];
+  apply iff_intro!;
+  all_goals apply imp_id!
+
+@[symm]
+protected lemma symm : (p ⟷[Λ, Γ] q) → (q ⟷[Λ, Γ] p) := by
+  simp only [DeducibleEquivalent];
+  intro dpq;
+  exact iff_symm'! dpq;
+
+@[trans]
+protected lemma trans : (p ⟷[Λ, Γ] q) → (q ⟷[Λ, Γ] r) → (p ⟷[Λ, Γ] r) := by
+  simp only [DeducibleEquivalent];
+  intro dpq dqr;
+  apply iff_intro!;
+  . exact imp_trans'! (iff_mp'! dpq) (iff_mp'! dqr);
+  . exact imp_trans'! (iff_mpr'! dqr) (iff_mpr'! dpq);
+
+instance : IsEquiv (Formula α) (· ⟷[Λ, Γ] ·) where
+  refl := by apply DeducibleEquivalent.refl
+  symm := by apply DeducibleEquivalent.symm
+  trans := by apply DeducibleEquivalent.trans
+
+@[simp]
+lemma tauto : p ⟷[Λ, Γ] p := by simp [DeducibleEquivalent]; apply iff_intro!; all_goals apply imp_id!
+
+lemma _root_.Set.subset_insert_insert {α} {s : Set α} {a b} : s ⊆ insert a (insert b s) := by
+  have h₁ := Set.subset_insert a s;
+  have h₂ : (insert a s) ⊆ (insert a (insert b s)) := Set.insert_subset_insert (by simp);
+  exact subset_trans h₁ h₂
+
+lemma or (hp : p₁ ⟷[Λ, Γ] p₂) (hq : q₁ ⟷[Λ, Γ] q₂) : ((p₁ ⋎ q₁) ⟷[Λ, Γ] (p₂ ⋎ q₂)) := by
+  simp_all only [DeducibleEquivalent];
+  apply iff_intro!
+  . apply dtr!;
+    exact disj₃'!
+      (by
+        apply dtr!;
+        have d₁ : (insert p₁ (insert (p₁ ⋎ q₁) Γ)) ⊢ᴹ[Λ]! p₁ := axm! (by simp);
+        have d₂ : (insert p₁ (insert (p₁ ⋎ q₁) Γ)) ⊢ᴹ[Λ]! p₁ ⟶ p₂ := weakening! Set.subset_insert_insert (iff_mp'! hp);
+        exact disj₁'! $ modus_ponens'! d₂ d₁;
+      )
+      (by
+        apply dtr!;
+        have d₁ : (insert q₁ (insert (p₁ ⋎ q₁) Γ)) ⊢ᴹ[Λ]! q₁ := axm! (by simp);
+        have d₂ : (insert q₁ (insert (p₁ ⋎ q₁) Γ)) ⊢ᴹ[Λ]! q₁ ⟶ q₂ := weakening! Set.subset_insert_insert (iff_mp'! hq);
+        exact disj₂'! $ modus_ponens'! d₂ d₁;
+      )
+      (show insert (p₁ ⋎ q₁) Γ ⊢ᴹ[Λ]! (p₁ ⋎ q₁) by exact axm! (by simp));
+  . apply dtr!;
+    exact disj₃'!
+      (by
+        apply dtr!;
+        have d₁ : (insert p₂ (insert (p₂ ⋎ q₂) Γ)) ⊢ᴹ[Λ]! p₂ := axm! (by simp);
+        have d₂ : (insert p₂ (insert (p₂ ⋎ q₂) Γ)) ⊢ᴹ[Λ]! p₂ ⟶ p₁ := weakening! Set.subset_insert_insert (iff_mpr'! hp);
+        exact disj₁'! $ modus_ponens'! d₂ d₁;
+      )
+      (by
+        apply dtr!;
+        have d₁ : (insert q₂ (insert (p₂ ⋎ q₂) Γ)) ⊢ᴹ[Λ]! q₂ := axm! (by simp);
+        have d₂ : (insert q₂ (insert (p₂ ⋎ q₂) Γ)) ⊢ᴹ[Λ]! q₂ ⟶ q₁ := weakening! Set.subset_insert_insert (iff_mpr'! hq);
+        exact disj₂'! $ modus_ponens'! d₂ d₁;
+      )
+      (show insert (p₂ ⋎ q₂) Γ ⊢ᴹ[Λ]! (p₂ ⋎ q₂) by exact axm! (by simp));
+
+lemma and (hp : p₁ ⟷[Λ, Γ] p₂) (hq : q₁ ⟷[Λ, Γ] q₂) : ((p₁ ⋏ q₁) ⟷[Λ, Γ] (p₂ ⋏ q₂)) := by
+  simp_all only [DeducibleEquivalent];
+  apply iff_intro!;
+  . apply dtr!;
+    have d : insert (p₁ ⋏ q₁) Γ ⊢ᴹ[Λ]!(p₁ ⋏ q₁) := axm! (by simp)
+    exact conj₃'!
+      (modus_ponens'! (weakening! (by simp) $ iff_mp'! hp) (conj₁'! d))
+      (modus_ponens'! (weakening! (by simp) $ iff_mp'! hq) (conj₂'! d));
+  . apply dtr!;
+    have d : insert (p₂ ⋏ q₂) Γ ⊢ᴹ[Λ]!(p₂ ⋏ q₂) := axm! (by simp)
+    exact conj₃'!
+      (modus_ponens'! (weakening! (by simp) $ iff_mpr'! hp) (conj₁'! d))
+      (modus_ponens'! (weakening! (by simp) $ iff_mpr'! hq) (conj₂'! d));
+
+lemma and_comm (p q : Formula α) : ((p ⋏ q) ⟷[Λ, Γ] (q ⋏ p)) := by
+  simp_all only [DeducibleEquivalent];
+  apply iff_intro!;
+  . apply dtr!;
+    have d₁ : insert (p ⋏ q) Γ ⊢ᴹ[Λ]! (p ⋏ q) := axm! (by simp);
+    exact conj₃'! (conj₂'! d₁) (conj₁'! d₁);
+  . apply dtr!;
+    have d₁ : insert (q ⋏ p) Γ ⊢ᴹ[Λ]! (q ⋏ p) := axm! (by simp);
+    exact conj₃'! (conj₂'! d₁) (conj₁'! d₁);
+
+lemma imp (hp : p₁ ⟷[Λ, Γ] p₂) (hq : q₁ ⟷[Λ, Γ] q₂) : ((p₁ ⟶ q₁) ⟷[Λ, Γ] (p₂ ⟶ q₂)) := by
+  simp_all only [DeducibleEquivalent];
+  apply iff_intro!;
+  . apply dtr!;
+    apply dtr!;
+    have d₁ : insert p₂ (insert (p₁ ⟶ q₁) Γ) ⊢ᴹ[Λ]! (p₁ ⟶ q₁) := axm! (by simp)
+    have d₂ : insert p₂ (insert (p₁ ⟶ q₁) Γ) ⊢ᴹ[Λ]! p₂ := axm! (by simp)
+    have d₃ : insert p₂ (insert (p₁ ⟶ q₁) Γ) ⊢ᴹ[Λ]! q₁ := modus_ponens'! d₁ $ modus_ponens'! (weakening! Set.subset_insert_insert (iff_mpr'! hp)) d₂;
+    exact modus_ponens'! (weakening! Set.subset_insert_insert (iff_mp'! hq)) d₃;
+  . apply dtr!;
+    apply dtr!;
+    have d₁ : insert p₁ (insert (p₂ ⟶ q₂) Γ) ⊢ᴹ[Λ]! (p₂ ⟶ q₂) := axm! (by simp)
+    have d₂ : insert p₁ (insert (p₂ ⟶ q₂) Γ) ⊢ᴹ[Λ]! p₁ := axm! (by simp)
+    have d₃ : insert p₁ (insert (p₂ ⟶ q₂) Γ) ⊢ᴹ[Λ]! q₂ := modus_ponens'! d₁ $ modus_ponens'! (weakening! Set.subset_insert_insert (iff_mp'! hp)) d₂;
+    exact modus_ponens'! (weakening! Set.subset_insert_insert (iff_mpr'! hq)) d₃;
+
+lemma neg (h : p ⟷[Λ, Γ] q) : ((~p) ⟷[Λ, Γ] (~q)) := by
+  simp [DeducibleEquivalent];
+  exact imp h (by simp);
+
+variable [Hilbert.K (Deduction Λ)]
+
+lemma box (h : p ⟷[Λ, ∅] q) : ((□p) ⟷[Λ, Γ] (□q)) := by
+  simp_all only [DeducibleEquivalent];
+  apply iff_intro!;
+  . have d₁ : Γ ⊢ᴹ[Λ]! □(p ⟶ q) := necessitation! (iff_mp'! h);
+    have d₂ : Γ ⊢ᴹ[Λ]! □(p ⟶ q) ⟶ (□p ⟶ □q) := Hilbert.axiomK! Γ p q;
+    exact modus_ponens'! d₂ d₁;
+  . have d₁ : Γ ⊢ᴹ[Λ]! □(q ⟶ p) := necessitation! (iff_mpr'! h);
+    have d₂ : Γ ⊢ᴹ[Λ]! □(q ⟶ p) ⟶ (□q ⟶ □p) := Hilbert.axiomK! Γ q p;
+    exact modus_ponens'! d₂ d₁;
+
+end DeducibleEquivalent
+
+end Formula
+
 end Modal.Normal
 
 end LO

Logic/Modal/Normal/HilbertStyle.lean

@@ -66,9 +66,9 @@ variable [Classical Bew]
 
 open HasNecessitation
 
-def necessitation {Γ : Set F} {p} (d : Bew ∅ p) : Γ ⊢ □p := HasNecessitation.necessitation d
+def necessitation {Γ : Set F} {p} (d : (∅ : Set F) ⊢ p) : Γ ⊢ □p := HasNecessitation.necessitation d
 
-def necessitation! {Γ : Set F} {p} (d : Bew ∅ p) : Γ ⊢! □p := ⟨necessitation d⟩
+def necessitation! {Γ : Set F} {p} (d : (∅ : Set F) ⊢! p) : Γ ⊢! □p := ⟨necessitation d.some⟩
 
 open HasBoxedNecessitation
 
@@ -85,17 +85,19 @@ def preboxed_necessitation! {Γ : Set F} {p} (d : Γ.prebox ⊢! p) : Γ ⊢! 
 
 open HasAxiomK
 
-def AxiomK (Γ : Set F) (p q) :  Γ ⊢ (AxiomK p q) := HasAxiomK.K Γ p q
-def AxiomK' {Γ : Set F} {p q} (d₁ : Γ ⊢ (□(p ⟶ q))) (d₂ : Γ ⊢ □p) : Γ ⊢ □q := ((AxiomK Γ p q) ⨀ d₁) ⨀ d₂
+protected def axiomK (Γ : Set F) (p q) :  Γ ⊢ (AxiomK p q) := HasAxiomK.K Γ p q
+def axiomK' {Γ : Set F} {p q} (d₁ : Γ ⊢ (□(p ⟶ q))) (d₂ : Γ ⊢ □p) : Γ ⊢ □q := ((Hilbert.axiomK Γ p q) ⨀ d₁) ⨀ d₂
+
+lemma axiomK! (Γ : Set F) (p q) : Γ ⊢! (AxiomK p q) := ⟨Hilbert.axiomK Γ p q⟩
 
 def boxverum (Γ : Set F) : Γ ⊢ □⊤ := necessitation (verum _)
 lemma boxverum! (Γ : Set F) : Γ ⊢! □⊤ := ⟨boxverum Γ⟩
 
 def box_iff' {Γ : Set F} {p q : F} (d : ∅ ⊢ p ⟷ q) : Γ ⊢ (□p ⟷ □q) := by
-  have dp₁ : ∅ ⊢ (□(p ⟶ q) ⟶ (□p ⟶ □q)) := AxiomK ∅ p q;
+  have dp₁ : ∅ ⊢ (□(p ⟶ q) ⟶ (□p ⟶ □q)) := Hilbert.axiomK ∅ p q;
   have dp₂ : ∅ ⊢ (□(p ⟶ q)) := necessitation $ iff_mp' d;
 
-  have dq₁ : ∅ ⊢ (□(q ⟶ p) ⟶ (□q ⟶ □p)) := AxiomK ∅ q p;
+  have dq₁ : ∅ ⊢ (□(q ⟶ p) ⟶ (□q ⟶ □p)) := Hilbert.axiomK ∅ q p;
   have dq₂ : ∅ ⊢ (□(q ⟶ p)) := necessitation $ iff_mpr' d;
 
   exact iff_intro