From 625c054a6df62a94e86f7ebddac174a7b6b466fd Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Sun, 16 Jun 2024 14:32:51 +0900
Subject: [PATCH 1/8] =?UTF-8?q?Some=20extensons=20of=20`=F0=9D=90=8D`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Logic/Modal/Standard/Deduction.lean      | 28 +++++++++++++++++++++
 Logic/Modal/Standard/PLoN/Semantics.lean | 11 +++++---
 Logic/Modal/Standard/PLoN/Soundness.lean | 32 ++++++++++++++++--------
 3 files changed, 58 insertions(+), 13 deletions(-)

diff --git a/Logic/Modal/Standard/Deduction.lean b/Logic/Modal/Standard/Deduction.lean
index a8b4dff5..028f6cda 100644
--- a/Logic/Modal/Standard/Deduction.lean
+++ b/Logic/Modal/Standard/Deduction.lean
@@ -28,6 +28,12 @@ notation "⟮Loeb⟯" => LoebRule
 abbrev HenkinRule {α} : InferenceRules α := { { antecedents := [□p ⟷ p], consequence := p }| (p) }
 notation "⟮Henkin⟯" => HenkinRule
 
+/--
+
+  | rosser {p}     : (𝓓.rules.rosser = true) → Deduction 𝓓 (~p) → Deduction 𝓓 (~(□p))
+  | rosser_box {p} : (𝓓.rules.rosser_box = true) → Deduction 𝓓 (~(□p)) → Deduction 𝓓 (~(□□p))
+-/
+
 structure DeductionParameter (α : Type*) where
   axioms : AxiomSet α
   rules : InferenceRules α
@@ -333,6 +339,28 @@ instance : 𝐍.HasNecOnly (α := α) where
 
 end PLoN
 
+protected abbrev N4 : DeductionParameter α where
+  axiomSet := 𝟰
+  rules := { nec := true }
+notation "𝐍𝟒" => DeductionParameter.N4
+instance : HasNecOnly (α := α) 𝐍𝟒 where
+instance : System.HasAxiomFour (𝐍𝟒 : DeductionParameter α) where
+  Four _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp)
+
+protected abbrev NRosser : DeductionParameter α where
+  axiomSet := ∅
+  rules := { nec := true, rosser := true }
+notation "𝐍(𝐑)" => DeductionParameter.NRosser
+instance : HasNec (α := α) 𝐍(𝐑) where
+
+protected abbrev N4Rosser : DeductionParameter α where
+  axiomSet := 𝟰
+  rules := { nec := true, rosser := true }
+notation "𝐍𝟒(𝐑)" => DeductionParameter.N4Rosser
+instance : HasNec (α := α) 𝐍𝟒(𝐑) where
+instance : System.HasAxiomFour (𝐍𝟒(𝐑) : DeductionParameter α) where
+  Four _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp)
+
 end DeductionParameter
 
 open System
diff --git a/Logic/Modal/Standard/PLoN/Semantics.lean b/Logic/Modal/Standard/PLoN/Semantics.lean
index 2d3596dd..95433c7b 100644
--- a/Logic/Modal/Standard/PLoN/Semantics.lean
+++ b/Logic/Modal/Standard/PLoN/Semantics.lean
@@ -1,7 +1,6 @@
+import Logic.Vorspiel.BinaryRelations
 import Logic.Modal.Standard.Deduction
 
-universe u v
-
 namespace LO.Modal.Standard
 
 namespace PLoN
@@ -44,6 +43,8 @@ structure Model (α) where
 abbrev Model.World (M : PLoN.Model α) := M.Frame.World
 instance : CoeSort (PLoN.Model α) (Type _) := ⟨Model.World⟩
 
+
+
 end PLoN
 
 variable {α : Type*}
@@ -175,10 +176,14 @@ protected lemma elim_contra : 𝔽 ⊧ (Axioms.ElimContra p q) := by intro _ _;
 end Formula.PLoN.ValidOnFrameClass
 
 
+def DeductionParameter.CharacterizedByPLoNFrameClass (𝓓 : DeductionParameter α) (𝔽 : PLoN.FrameClass α) := ∀ {F : Frame α}, F ∈ 𝔽 → F ⊧* 𝓓.theory
+
+-- MEMO: `←`方向は成り立たない可能性がある
 def DeductionParameter.DefinesPLoNFrameClass (𝓓 : DeductionParameter α) (𝔽 : PLoN.FrameClass α) := ∀ {F : Frame α}, F ⊧* 𝓓.theory ↔ F ∈ 𝔽
 
 namespace PLoN
 
+open Formula.PLoN
 
 abbrev AllFrameClass (α) : FrameClass α := Set.univ
 
@@ -188,7 +193,7 @@ lemma AllFrameClass.nonempty : (AllFrameClass.{_, 0} α).Nonempty := by
 
 open Formula
 
-lemma N_defines : 𝐍.DefinesPLoNFrameClass (AllFrameClass α) := by
+lemma N_characterized : 𝐍.CharacterizedByPLoNFrameClass (AllFrameClass α) := by
   intro F;
   simp [DeductionParameter.theory, System.theory, PLoN.ValidOnFrame, PLoN.ValidOnModel];
   intro p hp;
diff --git a/Logic/Modal/Standard/PLoN/Soundness.lean b/Logic/Modal/Standard/PLoN/Soundness.lean
index 7e39ef4c..11afd5fc 100644
--- a/Logic/Modal/Standard/PLoN/Soundness.lean
+++ b/Logic/Modal/Standard/PLoN/Soundness.lean
@@ -4,30 +4,42 @@ namespace LO.Modal.Standard
 
 namespace PLoN
 
-open Formula
+open System Formula
 
 variable {p : Formula α} {Λ : DeductionParameter α}
 
-lemma sound (defines : Λ.DefinesPLoNFrameClass 𝔽) (d : Λ ⊢! p) : 𝔽 ⊧ p := by
+lemma sound (characterized : Λ.CharacterizedByPLoNFrameClass 𝔽) (d : Λ ⊢! p) : 𝔽 ⊧ p := by
   intro F hF;
-  have := defines.mpr hF;
+  have := characterized hF;
   exact Semantics.RealizeSet.setOf_iff.mp this p d;
 
-lemma sound_of_defines (defines : Λ.DefinesPLoNFrameClass 𝔽) : Sound Λ 𝔽 := ⟨sound defines⟩
+lemma sound_of_characterized (defines : Λ.CharacterizedByPLoNFrameClass 𝔽) : Sound Λ 𝔽 := ⟨sound defines⟩
 
-lemma unprovable_bot_of_nonempty_frameclass (defines : Λ.DefinesPLoNFrameClass 𝔽) (nonempty : 𝔽.Nonempty) : Λ ⊬! ⊥ := by
+lemma unprovable_bot_of_nonempty_frameclass (characterized : Λ.CharacterizedByPLoNFrameClass 𝔽) (nonempty : 𝔽.Nonempty) : Λ ⊬! ⊥ := by
   intro h;
   obtain ⟨⟨_, F⟩, hF⟩ := nonempty;
-  simpa using sound defines h hF;
+  simpa using sound characterized h hF;
 
-lemma consistent_of_defines (defines : Λ.DefinesPLoNFrameClass 𝔽) (nonempty : 𝔽.Nonempty) : System.Consistent Λ := by
+lemma consistent_of_characterized (characterized : Λ.CharacterizedByPLoNFrameClass 𝔽) (nonempty : 𝔽.Nonempty) : System.Consistent Λ := by
   apply System.Consistent.of_unprovable;
-  exact unprovable_bot_of_nonempty_frameclass defines nonempty;
+  exact unprovable_bot_of_nonempty_frameclass characterized nonempty;
 
 
-instance : Sound 𝐍 (AllFrameClass α) := sound_of_defines N_defines
+instance : Sound 𝐍 (AllFrameClass α) := sound_of_characterized N_characterized
 
-instance : System.Consistent (𝐍 : DeductionParameter α) := consistent_of_defines N_defines AllFrameClass.nonempty
+instance : Sound 𝐍𝟒 (TransitiveFrameClass α) := sound_of_characterized N4_characterized
+
+instance : Sound 𝐍(𝐑) (SerialFrameClass α) := sound_of_characterized NRosser_characterized
+
+instance : Sound 𝐍𝟒(𝐑) (TransitiveSerialFrameClass α) := sound_of_characterized N4Rosser_characterized
+
+instance : System.Consistent (𝐍 : DeductionParameter α) := consistent_of_characterized N_characterized AllFrameClass.nonempty
+
+instance : System.Consistent (𝐍𝟒 : DeductionParameter α) := consistent_of_characterized N4_characterized TransitiveFrameClass.nonempty
+
+instance : System.Consistent (𝐍(𝐑) : DeductionParameter α) := consistent_of_characterized NRosser_characterized SerialFrameClass.nonempty
+
+instance : System.Consistent (𝐍𝟒(𝐑) : DeductionParameter α) := consistent_of_characterized N4Rosser_characterized TransitiveSerialFrameClass.nonempty
 
 end PLoN
 

From acaf6d72c343694dc31558fc869ef90f854c43e4 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Sun, 30 Jun 2024 23:10:56 +0900
Subject: [PATCH 2/8] fix about system change

---
 Logic/Modal/Standard/Deduction.lean      |  24 ++---
 Logic/Modal/Standard/PLoN/Semantics.lean | 106 +++++++++++++++++++++++
 2 files changed, 118 insertions(+), 12 deletions(-)

diff --git a/Logic/Modal/Standard/Deduction.lean b/Logic/Modal/Standard/Deduction.lean
index 028f6cda..540b855f 100644
--- a/Logic/Modal/Standard/Deduction.lean
+++ b/Logic/Modal/Standard/Deduction.lean
@@ -28,11 +28,11 @@ notation "⟮Loeb⟯" => LoebRule
 abbrev HenkinRule {α} : InferenceRules α := { { antecedents := [□p ⟷ p], consequence := p }| (p) }
 notation "⟮Henkin⟯" => HenkinRule
 
-/--
+abbrev RosserRule {α} : InferenceRules α := { { antecedents := [~p], consequence := ~(□p) } | (p) }
+notation "⟮Rosser⟯" => RosserRule
 
-  | rosser {p}     : (𝓓.rules.rosser = true) → Deduction 𝓓 (~p) → Deduction 𝓓 (~(□p))
-  | rosser_box {p} : (𝓓.rules.rosser_box = true) → Deduction 𝓓 (~(□p)) → Deduction 𝓓 (~(□□p))
--/
+abbrev RosserBoxRule {α} : InferenceRules α := { { antecedents := [~(□p)], consequence := ~(□□p) } | (p) }
+notation "⟮Rosser□⟯" => RosserBoxRule
 
 structure DeductionParameter (α : Type*) where
   axioms : AxiomSet α
@@ -340,24 +340,24 @@ instance : 𝐍.HasNecOnly (α := α) where
 end PLoN
 
 protected abbrev N4 : DeductionParameter α where
-  axiomSet := 𝟰
-  rules := { nec := true }
+  axioms := 𝟰
+  rules := ⟮Nec⟯
 notation "𝐍𝟒" => DeductionParameter.N4
 instance : HasNecOnly (α := α) 𝐍𝟒 where
 instance : System.HasAxiomFour (𝐍𝟒 : DeductionParameter α) where
   Four _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp)
 
 protected abbrev NRosser : DeductionParameter α where
-  axiomSet := ∅
-  rules := { nec := true, rosser := true }
+  axioms := ∅
+  rules := ⟮Nec⟯ ∪ ⟮Rosser⟯
 notation "𝐍(𝐑)" => DeductionParameter.NRosser
-instance : HasNec (α := α) 𝐍(𝐑) where
+instance : 𝐍(𝐑).HasNecessitation (α := α) where
 
 protected abbrev N4Rosser : DeductionParameter α where
-  axiomSet := 𝟰
-  rules := { nec := true, rosser := true }
+  axioms := 𝟰
+  rules := ⟮Nec⟯ ∪ ⟮Rosser□⟯
 notation "𝐍𝟒(𝐑)" => DeductionParameter.N4Rosser
-instance : HasNec (α := α) 𝐍𝟒(𝐑) where
+instance : 𝐍𝟒(𝐑).HasNecessitation (α := α) where
 instance : System.HasAxiomFour (𝐍𝟒(𝐑) : DeductionParameter α) where
   Four _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp)
 
diff --git a/Logic/Modal/Standard/PLoN/Semantics.lean b/Logic/Modal/Standard/PLoN/Semantics.lean
index 95433c7b..ae41fb98 100644
--- a/Logic/Modal/Standard/PLoN/Semantics.lean
+++ b/Logic/Modal/Standard/PLoN/Semantics.lean
@@ -209,6 +209,112 @@ lemma N_characterized : 𝐍.CharacterizedByPLoNFrameClass (AllFrameClass α) :=
     simp_all [PLoN.Satisfies];
     try tauto;
 
+
+namespace Frame
+
+variable (F : Frame α)
+
+def SerialOnFormula (p : Formula α) : Prop := Serial (F.Rel' p)
+
+def SerialOnTheory (T : Theory α) : Prop := ∀ p ∈ T, F.SerialOnFormula p
+
+protected def Serial : Prop := ∀ p, F.SerialOnFormula p
+
+
+def TransitiveOnFormula (p : Formula α) : Prop := ∀ {x y z : F.World}, x ≺[□p] y → y ≺[p] z → x ≺[p] z
+
+def TransitiveOnTheory (T : Theory α) : Prop := ∀ p ∈ T, F.SerialOnFormula p
+
+protected def Transitive (F : Frame α) := ∀ p, F.TransitiveOnFormula p
+
+end Frame
+
+
+open System
+
+lemma validRosserRule_of_serial {p : Formula α} {F : PLoN.Frame α} (hSerial : F.SerialOnFormula p) (h : F ⊧ ~p) : F ⊧ ~(□p) := by
+  intro V x;
+  obtain ⟨y, hy⟩ := hSerial x;
+  simp [Formula.PLoN.Satisfies];
+  use y, hy;
+  exact h V y;
+
+lemma validAxiomFour_of_transitive {p : Formula α} {F : PLoN.Frame α} (hTrans : F.TransitiveOnFormula p) : F ⊧ Axioms.Four p := by
+  dsimp [Axioms.Four];
+  intro V x h y rxy z ryz;
+  exact h (hTrans rxy ryz);
+
+
+abbrev TransitiveFrameClass (α) : PLoN.FrameClass α := { F | Frame.Transitive F }
+
+lemma TransitiveFrameClass.nonempty : (TransitiveFrameClass.{_, 0} α).Nonempty := by
+  use terminalFrame α;
+  simp [Frame.Transitive, Frame.TransitiveOnFormula];
+
+
+abbrev SerialFrameClass (α) : PLoN.FrameClass α := { F | Frame.Serial F }
+
+lemma SerialFrameClass.nonempty : (SerialFrameClass.{_, 0} α).Nonempty := by
+  use terminalFrame α;
+  intro p x; use x;
+
+
+abbrev TransitiveSerialFrameClass (α) : PLoN.FrameClass α := { F | F.Transitive ∧ F.Serial }
+
+lemma TransitiveSerialFrameClass.nonempty : (TransitiveSerialFrameClass.{_, 0} α).Nonempty := by
+  use terminalFrame α;
+  simp [Frame.Transitive, Frame.Serial, Frame.TransitiveOnFormula, Frame.SerialOnFormula];
+  intro p x; use x;
+
+
+lemma N4_characterized : 𝐍𝟒.CharacterizedByPLoNFrameClass (TransitiveFrameClass α) := by
+  intro F;
+  simp [DeductionParameter.theory, System.theory, PLoN.ValidOnFrame, PLoN.ValidOnModel];
+  intro hTrans p hp;
+  induction hp using Deduction.inducition_with_necOnly! with
+  | hMaxm h =>
+    obtain ⟨p, e⟩ := h; subst e;
+    exact validAxiomFour_of_transitive (hTrans p);
+  | hMdp ihpq ihp => exact PLoN.ValidOnFrame.mdp ihpq ihp;
+  | hNec ihp => exact PLoN.ValidOnFrame.nec ihp;
+  | hOrElim => exact PLoN.ValidOnFrame.disj₃;
+  | _ => simp_all [PLoN.Satisfies];
+
+lemma NRosser_characterized : 𝐍(𝐑).CharacterizedByPLoNFrameClass (SerialFrameClass α) := by
+  intro F;
+  simp [DeductionParameter.theory, System.theory, PLoN.ValidOnFrame, PLoN.ValidOnModel];
+  intro hSerial p hp;
+  induction hp using Deduction.inducition! with
+  | hMaxm h => simp at h;
+  | hMdp ihpq ihp => exact PLoN.ValidOnFrame.mdp ihpq ihp;
+  | hRules rl hrl hant ih =>
+    rcases hrl with (hNec | hRosser)
+    . obtain ⟨p, e⟩ := hNec; subst e; simp_all;
+      exact PLoN.ValidOnFrame.nec ih;
+    . obtain ⟨p, e⟩ := hRosser; subst e; simp_all;
+      exact validRosserRule_of_serial (hSerial _) ih;
+  | hOrElim => exact PLoN.ValidOnFrame.disj₃;
+  | _ => simp_all [PLoN.Satisfies];
+
+-- TODO: `theory 𝐍𝟒 ∪ theory 𝐍(𝐑) = theory 𝐍𝟒(𝐑)`という事実を示せば共通部分だけで簡単に特徴づけられる気がする
+lemma N4Rosser_characterized : 𝐍𝟒(𝐑).CharacterizedByPLoNFrameClass (TransitiveSerialFrameClass α) := by
+  intro F;
+  simp [DeductionParameter.theory, System.theory, PLoN.ValidOnFrame, PLoN.ValidOnModel];
+  intro hTrans hSerial p hp;
+  induction hp using Deduction.inducition! with
+  | hMaxm h =>
+    obtain ⟨p, e⟩ := h; subst e;
+    exact validAxiomFour_of_transitive (hTrans p);
+  | hMdp ihpq ihp => exact PLoN.ValidOnFrame.mdp ihpq ihp;
+  | hRules rl hrl hant ih =>
+    rcases hrl with (hNec | hRosser)
+    . obtain ⟨p, e⟩ := hNec; subst e; simp_all;
+      exact PLoN.ValidOnFrame.nec ih;
+    . obtain ⟨p, e⟩ := hRosser; subst e; simp_all;
+      exact validRosserRule_of_serial (hSerial _) ih;
+  | hOrElim => exact PLoN.ValidOnFrame.disj₃;
+  | _ => simp_all [PLoN.Satisfies];
+
 end PLoN
 
 end LO.Modal.Standard

From 1963a1fd0e2648386604523a6d9850b3a17da32f Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Mon, 1 Jul 2024 21:52:43 +0900
Subject: [PATCH 3/8] fix(Modal): Remove neg abbrev (wip)

---
 Logic/Modal/Standard/Maximal.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Logic/Modal/Standard/Maximal.lean b/Logic/Modal/Standard/Maximal.lean
index df7abea8..7b6f42a4 100644
--- a/Logic/Modal/Standard/Maximal.lean
+++ b/Logic/Modal/Standard/Maximal.lean
@@ -54,7 +54,7 @@ postfix:75 "ᵀ" => TrivTranslation
 namespace TrivTranslation
 
 @[simp] lemma degree_zero : pᵀ.degree = 0 := by induction p <;> simp [TrivTranslation, degree, *];
-@[simp] lemma back : pᵀᴾᴹ = pᵀ := by induction p using rec' <;> simp [Superintuitionistic.Formula.toModalFormula, TrivTranslation, *];
+@[simp] lemma back : pᵀᴾᴹ = pᵀ := by sorry; -- induction p using rec' <;> simp [Superintuitionistic.Formula.toModalFormula, TrivTranslation, *];
 
 end TrivTranslation
 

From 95cb51c6192055fca102879e6bfcff0ec3399891 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Tue, 2 Jul 2024 02:22:51 +0900
Subject: [PATCH 4/8] intuitional rewrite

---
 Logic/Modal/Standard/Maximal.lean                    | 3 ++-
 Logic/Propositional/Superintuitionistic/Formula.lean | 2 ++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/Logic/Modal/Standard/Maximal.lean b/Logic/Modal/Standard/Maximal.lean
index 7b6f42a4..060aa634 100644
--- a/Logic/Modal/Standard/Maximal.lean
+++ b/Logic/Modal/Standard/Maximal.lean
@@ -15,6 +15,7 @@ def Formula.toModalFormula : Formula α → Modal.Standard.Formula α
   | ⊥ => ⊥
   | ~p => ~(toModalFormula p)
   | p ⟶ q => (toModalFormula p) ⟶ (toModalFormula q)
+  | ~p => ~(toModalFormula p)
   | p ⋏ q => (toModalFormula p) ⋏ (toModalFormula q)
   | p ⋎ q => (toModalFormula p) ⋎ (toModalFormula q)
 postfix:75 "ᴹ" => Formula.toModalFormula
@@ -54,7 +55,7 @@ postfix:75 "ᵀ" => TrivTranslation
 namespace TrivTranslation
 
 @[simp] lemma degree_zero : pᵀ.degree = 0 := by induction p <;> simp [TrivTranslation, degree, *];
-@[simp] lemma back : pᵀᴾᴹ = pᵀ := by sorry; -- induction p using rec' <;> simp [Superintuitionistic.Formula.toModalFormula, TrivTranslation, *];
+@[simp] lemma back : pᵀᴾᴹ = pᵀ := by induction p using rec' <;> simp [Superintuitionistic.Formula.toModalFormula, TrivTranslation, *];
 
 end TrivTranslation
 
diff --git a/Logic/Propositional/Superintuitionistic/Formula.lean b/Logic/Propositional/Superintuitionistic/Formula.lean
index 112f56a3..afbf7299 100644
--- a/Logic/Propositional/Superintuitionistic/Formula.lean
+++ b/Logic/Propositional/Superintuitionistic/Formula.lean
@@ -161,6 +161,7 @@ instance : DecidableEq (Formula α) := hasDecEq
 
 end Decidable
 
+/-
 section Encodable
 
 open Sum
@@ -231,6 +232,7 @@ variable [Encodable α]
 instance : Encodable (Formula α) := Encodable.ofEquiv (WType (Edge α)) (equivW α)
 
 end Encodable
+-/
 
 end Formula
 

From 8fac973a7564cee95ced5ec6d6fb49c294b614a4 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Tue, 2 Jul 2024 04:40:39 +0900
Subject: [PATCH 5/8] update

---
 Logic/Propositional/Superintuitionistic/Formula.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Logic/Propositional/Superintuitionistic/Formula.lean b/Logic/Propositional/Superintuitionistic/Formula.lean
index afbf7299..112f56a3 100644
--- a/Logic/Propositional/Superintuitionistic/Formula.lean
+++ b/Logic/Propositional/Superintuitionistic/Formula.lean
@@ -161,7 +161,6 @@ instance : DecidableEq (Formula α) := hasDecEq
 
 end Decidable
 
-/-
 section Encodable
 
 open Sum
@@ -232,7 +231,6 @@ variable [Encodable α]
 instance : Encodable (Formula α) := Encodable.ofEquiv (WType (Edge α)) (equivW α)
 
 end Encodable
--/
 
 end Formula
 

From b08fe65d4389ec647480c88924b10729b3a772dc Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Thu, 4 Jul 2024 12:04:44 +0900
Subject: [PATCH 6/8] Update

---
 Logic/Modal/Standard/Maximal.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Logic/Modal/Standard/Maximal.lean b/Logic/Modal/Standard/Maximal.lean
index 060aa634..df7abea8 100644
--- a/Logic/Modal/Standard/Maximal.lean
+++ b/Logic/Modal/Standard/Maximal.lean
@@ -15,7 +15,6 @@ def Formula.toModalFormula : Formula α → Modal.Standard.Formula α
   | ⊥ => ⊥
   | ~p => ~(toModalFormula p)
   | p ⟶ q => (toModalFormula p) ⟶ (toModalFormula q)
-  | ~p => ~(toModalFormula p)
   | p ⋏ q => (toModalFormula p) ⋏ (toModalFormula q)
   | p ⋎ q => (toModalFormula p) ⋎ (toModalFormula q)
 postfix:75 "ᴹ" => Formula.toModalFormula

From 986589686acba36ef682a3063471352339ecb3aa Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Fri, 5 Jul 2024 05:17:21 +0900
Subject: [PATCH 7/8] wip

---
 Logic/Logic/HilbertStyle/Supplemental.lean  |  10 +-
 Logic/Modal/Standard/Deduction.lean         |  29 +-
 Logic/Modal/Standard/PLoN/Completeness.lean | 395 ++++++++++++++++++++
 Logic/Modal/Standard/PLoN/Semantics.lean    |  49 ++-
 Logic/Modal/Standard/PLoN/Soundness.lean    |  11 +-
 Logic/Modal/Standard/System.lean            |   6 +
 6 files changed, 480 insertions(+), 20 deletions(-)

diff --git a/Logic/Logic/HilbertStyle/Supplemental.lean b/Logic/Logic/HilbertStyle/Supplemental.lean
index ff26eb0e..42491c9a 100644
--- a/Logic/Logic/HilbertStyle/Supplemental.lean
+++ b/Logic/Logic/HilbertStyle/Supplemental.lean
@@ -322,8 +322,14 @@ def negneg_equiv : 𝓢 ⊢ ~~p ⟷ ((p ⟶ ⊥) ⟶ ⊥) := by
   . exact impTrans'' (and₂' neg_equiv) (by apply contra₀'; exact and₁' neg_equiv)
 @[simp] lemma negneg_equiv! : 𝓢 ⊢! ~~p ⟷ ((p ⟶ ⊥) ⟶ ⊥) := ⟨negneg_equiv⟩
 
-def negneg_equiv_dne [HasAxiomDNE 𝓢] : 𝓢 ⊢ p ⟷ ((p ⟶ ⊥) ⟶ ⊥) := iffTrans'' dn negneg_equiv
-lemma negneg_equiv_dne! [HasAxiomDNE 𝓢] : 𝓢 ⊢! p ⟷ ((p ⟶ ⊥) ⟶ ⊥) := ⟨negneg_equiv_dne⟩
+def negneg_equiv'.mp [NegationEquiv 𝓢] : 𝓢 ⊢ ~~p → 𝓢 ⊢ ((p ⟶ ⊥) ⟶ ⊥) := λ h => (and₁' negneg_equiv) ⨀ h
+def negneg_equiv'.mpr [NegationEquiv 𝓢] : 𝓢 ⊢ ((p ⟶ ⊥) ⟶ ⊥) → 𝓢 ⊢ ~~p := λ h => (and₂' negneg_equiv) ⨀ h
+lemma negneg_equiv'! [HasAxiomDNE 𝓢] : 𝓢 ⊢! ~~p ↔ 𝓢 ⊢! ((p ⟶ ⊥) ⟶ ⊥) :=
+  ⟨λ ⟨h⟩ => ⟨negneg_equiv'.mp h⟩, λ ⟨h⟩ => ⟨negneg_equiv'.mpr h⟩⟩
+
+def negneg_equiv_dn [HasAxiomDNE 𝓢] : 𝓢 ⊢ p ⟷ ((p ⟶ ⊥) ⟶ ⊥) := iffTrans'' dn negneg_equiv
+lemma negneg_equiv_dn! [HasAxiomDNE 𝓢] : 𝓢 ⊢! p ⟷ ((p ⟶ ⊥) ⟶ ⊥) := ⟨negneg_equiv_dn⟩
+
 
 end NegationEquiv
 
diff --git a/Logic/Modal/Standard/Deduction.lean b/Logic/Modal/Standard/Deduction.lean
index 540b855f..ff030b92 100644
--- a/Logic/Modal/Standard/Deduction.lean
+++ b/Logic/Modal/Standard/Deduction.lean
@@ -100,6 +100,17 @@ class HasHenkinRule (𝓓 : DeductionParameter α) where
 instance [HasHenkinRule 𝓓] : System.HenkinRule 𝓓 where
   henkin := @λ p d => rule (show { antecedents := [□p ⟷ p], consequence := p } ∈ Rl(𝓓) by apply HasHenkinRule.has_henkin; simp_all) (by aesop);
 
+class HasRosserRule (𝓓 : DeductionParameter α) where
+  has_rosser : ⟮Rosser⟯ ⊆ Rl(𝓓) := by aesop
+
+instance [HasRosserRule 𝓓] : System.RosserRule 𝓓 where
+  rosser := @λ p d => rule (show { antecedents := [~p], consequence := ~(□p) } ∈ Rl(𝓓) by apply HasRosserRule.has_rosser; simp_all) (by aesop);
+
+class HasRosserBoxRule (𝓓 : DeductionParameter α) where
+  has_rosser_box : ⟮Rosser□⟯ ⊆ Rl(𝓓) := by aesop
+
+instance [HasRosserBoxRule 𝓓] : System.RosserBoxRule 𝓓 where
+  rosser_box := @λ p d => rule (show { antecedents := [~(□p)], consequence := ~(□□p) } ∈ Rl(𝓓) by apply HasRosserBoxRule.has_rosser_box; simp_all) (by aesop);
 
 class HasNecOnly (𝓓 : DeductionParameter α) where
   has_necessitation_only : Rl(𝓓) = ⟮Nec⟯ := by rfl
@@ -115,6 +126,11 @@ instance [HasAxiomK 𝓓] : System.HasAxiomK 𝓓 where
 
 class IsNormal (𝓓 : DeductionParameter α) extends 𝓓.HasNecOnly, 𝓓.HasAxiomK where
 
+class HasAxiomFour (𝓓 : DeductionParameter α) where
+  has_axiomFour : 𝟰 ⊆ Ax(𝓓) := by aesop
+
+instance [HasAxiomFour 𝓓] : System.HasAxiomFour 𝓓 where
+  Four _ := maxm (by apply HasAxiomFour.has_axiomFour; simp_all)
 
 end DeductionParameter
 
@@ -222,8 +238,7 @@ notation "𝐊𝐓𝐁" => DeductionParameter.KTB
 
 protected abbrev K4 : DeductionParameter α := 𝝂𝟰
 notation "𝐊𝟒" => DeductionParameter.K4
-instance : System.K4 (𝐊𝟒 : DeductionParameter α) where
-  Four _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp)
+instance : 𝐊𝟒.HasAxiomFour (α := α) where
 
 
 protected abbrev K5 : DeductionParameter α := 𝝂𝟱
@@ -343,23 +358,23 @@ protected abbrev N4 : DeductionParameter α where
   axioms := 𝟰
   rules := ⟮Nec⟯
 notation "𝐍𝟒" => DeductionParameter.N4
-instance : HasNecOnly (α := α) 𝐍𝟒 where
-instance : System.HasAxiomFour (𝐍𝟒 : DeductionParameter α) where
-  Four _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp)
+instance : 𝐍𝟒.HasNecOnly (α := α)  where
+instance : 𝐍𝟒.HasAxiomFour (α := α) where
 
 protected abbrev NRosser : DeductionParameter α where
   axioms := ∅
   rules := ⟮Nec⟯ ∪ ⟮Rosser⟯
 notation "𝐍(𝐑)" => DeductionParameter.NRosser
 instance : 𝐍(𝐑).HasNecessitation (α := α) where
+instance : 𝐍(𝐑).HasRosserRule (α := α) where
 
 protected abbrev N4Rosser : DeductionParameter α where
   axioms := 𝟰
   rules := ⟮Nec⟯ ∪ ⟮Rosser□⟯
 notation "𝐍𝟒(𝐑)" => DeductionParameter.N4Rosser
 instance : 𝐍𝟒(𝐑).HasNecessitation (α := α) where
-instance : System.HasAxiomFour (𝐍𝟒(𝐑) : DeductionParameter α) where
-  Four _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) (by simp)
+instance : 𝐍𝟒(𝐑).HasRosserBoxRule (α := α) where
+instance : 𝐍𝟒(𝐑).HasAxiomFour (α := α) where
 
 end DeductionParameter
 
diff --git a/Logic/Modal/Standard/PLoN/Completeness.lean b/Logic/Modal/Standard/PLoN/Completeness.lean
index 8de0e01f..caaa4065 100644
--- a/Logic/Modal/Standard/PLoN/Completeness.lean
+++ b/Logic/Modal/Standard/PLoN/Completeness.lean
@@ -12,6 +12,8 @@ open Formula
 open Theory
 open MaximalConsistentTheory
 
+section forN
+
 abbrev CanonicalFrame (Λ : DeductionParameter α) [Inhabited (Λ)-MCT] : PLoN.Frame α where
   World := (Λ)-MCT
   Rel := λ p Ω₁ Ω₂ => ~(□p) ∈ Ω₁.theory ∧ ~p ∈ Ω₂.theory
@@ -71,6 +73,399 @@ lemma instComplete_of_mem_canonicalFrame {𝔽 : FrameClass α} (hFC : Canonical
 
 instance : Complete 𝐍 (AllFrameClass.{u, u} α) := instComplete_of_mem_canonicalFrame (by simp)
 
+end forN
+
+
+section Others
+
+abbrev RestrictedFrame (F : PLoN.FiniteFrame α) (p : Formula α) : PLoN.FiniteFrame α where
+  World := F.World
+  World_inhabited := F.World_inhabited
+  World_finite := F.World_finite
+  Rel := λ q x y =>
+    if □q ∈ Sub p then x ≺[q] y
+    else x = y
+
+namespace RestrictedFrame
+
+variable {F : PLoN.FiniteFrame α} {p : Formula α} {x y : F.World} -- {x y : (RestrictedFrame F p).World}
+
+lemma def_rel_mem_sub {q : Formula α} (h : □q ∈ p.Subformulas) {x y : F.World} : F.Rel q x y ↔ (RestrictedFrame F p).Rel q x y := by aesop;
+
+lemma def_rel_mem_sub' {q : Formula α} (h : □q ∈ p.Subformulas) {x y : (RestrictedFrame F p).World} : F.Rel q x y ↔ (RestrictedFrame F p).Rel q x y := by
+  simp_all;
+
+lemma def_rel_not_mem_sub {q : Formula α} (h : □q ∉ p.Subformulas) {x y : F.World} : x = y ↔ (RestrictedFrame F p).Rel q x y := by aesop;
+
+open Formula.Subformulas RestrictedFrame
+
+lemma restricted_serial_of_serial (F_serial : F.toFrame.Serial) : (RestrictedFrame F p).toFrame.Serial := by
+  intro q hq x;
+  by_cases h : □q ∈ p.Subformulas;
+  . obtain ⟨y, rxy⟩ := @F_serial q hq x;
+    use y; exact def_rel_mem_sub h |>.mp rxy;
+  . use x; apply def_rel_not_mem_sub h |>.mp; rfl;
+
+lemma subformula_restricted_serial_of_serial (p : Formula α) (F_serial : F.toFrame.Serial) : (RestrictedFrame F p).SerialOnTheory p.Subformulas  := by
+  sorry;
+  -- apply Frame.serialOnTheory_of_serial;
+  -- simp only [Frame.SerialOnTheory];
+  -- exact restricted_serial_of_serial F_serial;
+
+lemma transitive_of_base_transitive (F_transitive : F.toFrame.Transitive) : (RestrictedFrame F p).toFrame.Transitive := by
+  intro q hq x y z rxy ryz;
+  by_cases h : □(□q) ∈ p.Subformulas
+  . have := @F_transitive q hq x y z;
+    replace rxy := def_rel_mem_sub' h |>.mpr rxy;
+    replace ryz := def_rel_mem_sub' (mem_box h) |>.mpr ryz;
+    have rxz := this rxy ryz;
+    sorry;
+  . have := def_rel_not_mem_sub h |>.mpr rxy; subst_vars;
+    exact ryz;
+
+lemma subformula_restricted_transitive_of_transitive (p : Formula α) (F_transitive : F.toFrame.Transitive) : (RestrictedFrame F p).TransitiveOnTheory p.Subformulas := by
+  sorry;
+  -- apply Frame.transitiveOnTheory_of_transitive;
+  -- exact transitive_of_base_transitive F_transitive;
+
+abbrev RestrictedModel (M : PLoN.FiniteModel α) (p : Formula α) : PLoN.Model α where
+  Frame := RestrictedFrame M.FiniteFrame p
+  Valuation a x := M.Valuation a x
+
+end RestrictedFrame
+
+end Others
+
+end PLoN
+
+
+section
+
+open System
+open Formula
+
+variable {Λ : DeductionParameter α} [System.Classical Λ]
+
+namespace Formula
+
+variable [DecidableEq α]
+
+
+def complement : Formula α → Formula α
+  | ~p => p
+  | p  => ~p
+postfix:80 "ᶜ" => complement
+
+@[simp]
+lemma complement_complement (p : Formula α) : pᶜᶜ = p := by sorry;
+
+lemma complement_congr (p q : Formula α) : p = q ↔ pᶜ = qᶜ := by
+  constructor;
+  . intro h;
+    subst h;
+    rfl;
+  . intro h;
+    sorry;
+
+abbrev ComplementSubformula (p : Formula α) : Finset (Formula α) := (Sub p) ∪ (Finset.image (Formula.complement) $ Sub p)
+prefix:70 "Subᶜ " => ComplementSubformula
+
+namespace ComplementSubformula
+
+variable {p q : Formula α}
+
+@[simp]
+lemma mem_self : p ∈ Subᶜ p := by simp;
+
+@[simp]
+lemma mem_self_complement : pᶜ ∈ Subᶜ p := by
+  simp [ComplementSubformula];
+  right;
+  use p;
+  constructor;
+  . simp only [Subformulas.mem_self];
+  . rfl;
+
+lemma mem_complement : q ∈ Subᶜ p ↔ qᶜ ∈ Subᶜ p := by
+  constructor;
+  . simp_all [ComplementSubformula];
+    rintro (hl | hr);
+    . right; sorry;
+    . obtain ⟨r, hr₁, hr₂⟩ := hr;
+      left; rw [←hr₂];
+      sorry;
+  . simp_all [ComplementSubformula];
+    rintro (hl | hr);
+    . right; use qᶜ; simp_all;
+    . obtain ⟨r, hr₁, hr₂⟩ := hr;
+      left; sorry;
+
+lemma mem_box (h : □q ∈ Subᶜ p) : q ∈ Subᶜ p := by
+  simp_all;
+  rcases h with (hl | hr);
+  . left; exact Subformulas.mem_box hl;
+  . obtain ⟨r, hr₁, hr₂⟩ := hr;
+    sorry;
+
+end ComplementSubformula
+
+end Formula
+
+variable [DecidableEq α]
+
+
+namespace Theory
+
+variable {Λ : DeductionParameter α} {p : Formula α} {T : Theory α} (T_consis : (Λ)-Consistent T) (T_subset : T ⊆ Subᶜ p)
+
+lemma exists_maximal_cs_consistent_theory
+  : ∃ Z, ((Λ)-Consistent Z ∧ Z ⊆ Subᶜ p) ∧ T ⊆ Z ∧ (∀ U, ((Λ)-Consistent U ∧ U ⊆ Subᶜ p) → Z ⊆ U → U = Z)
+  := zorn_subset_nonempty { T : Theory α | (Λ)-Consistent T ∧ T ⊆ Subᶜ p } (by
+    intro c hc chain hnc;
+    existsi (⋃₀ c);
+    simp only [Consistent, Set.mem_setOf_eq, Set.mem_sUnion];
+    refine ⟨⟨?h₁, ?h₂⟩, ?h₃⟩;
+    . intro Γ;
+      by_contra hC; simp at hC;
+      have ⟨hΓs, hΓd⟩ := hC;
+      obtain ⟨U, hUc, hUs⟩ :=
+        Set.subset_mem_chain_of_finite c hnc chain
+          (s := ↑Γ.toFinset) (by simp)
+          (by intro p hp; simp_all);
+      simp [List.coe_toFinset] at hUs;
+      have : (Λ)-Consistent U := hc hUc |>.1;
+      have : ¬(Λ)-Consistent U := by
+        simp only [Consistent, not_forall, not_not, exists_prop];
+        existsi Γ;
+        constructor;
+        . apply hUs;
+        . assumption;
+      contradiction;
+    . apply Set.sUnion_subset;
+      intro T hT;
+      apply hc hT |>.2;
+    . intro s a;
+      exact Set.subset_sUnion_of_mem a;
+  ) T ⟨T_consis, T_subset⟩
+
+lemma complement_consistent [System.Consistent Λ] {p : Formula α} (h : Λ ⊬! p) : (Λ)-Consistent {pᶜ} := by
+  simp [Theory.Consistent];
+  intro Γ hΓ; by_contra hC;
+  have := imply_left_remove_conj'! (p := pᶜ) hC;
+  -- have a : (List.remove (pᶜ) Γ) = [] := by sorry;
+  sorry;
+  /-
+  induction p using Formula.rec' with
+  | himp q r =>
+    simp [complement] at d;
+    split at d;
+    . rename_i heq;
+      simp at heq;
+    . have := dne'! $ negneg_equiv'!.mpr d;
+      contradiction;
+  | _ => sorry;
+  -/
+  /-
+  | _ =>
+    simp [complement] at d;
+    have := dne'! $ negneg_equiv'!.mpr d;
+    contradiction;
+  -/
+
+end Theory
+
+structure ComplementClosedMaximalConsistentTheory (Λ : DeductionParameter α) (p : Formula α) where
+  theory : Theory α
+  subset : theory ⊆ Subᶜ p
+  consistent : (Λ)-Consistent theory
+  maximal : ∀ {U}, U ⊆ ↑(Subᶜ p) → theory ⊂ U → ¬(Λ)-Consistent U
+
+notation "(" Λ "," p ")-MCT" => ComplementClosedMaximalConsistentTheory Λ p
+
+namespace ComplementClosedMaximalConsistentTheory
+
+open Theory
+
+
+lemma exists_maximal_Lconsistented_theory {T : Theory α} {p : Formula α} (T_subset : T ⊆ Subᶜ p) (T_consis : (𝓓)-Consistent T)
+  : ∃ Ω : (𝓓, p)-MCT, (T ⊆ Ω.theory) := by
+  have ⟨Ω, ⟨Ω_consis, Ω_subset⟩, T_Ω, Ω_maximal⟩ := Theory.exists_maximal_cs_consistent_theory T_consis T_subset;
+  existsi {
+    theory := Ω,
+    consistent := Ω_consis,
+    subset := Ω_subset,
+    maximal := by
+      rintro U hU₁ hU₂; by_contra hC;
+      rw [Ω_maximal U ⟨hC, hU₁⟩ hU₂.subset] at hU₂;
+      simp [Set.ssubset_def] at hU₂;
+  };
+  exact T_Ω;
+alias lindenbaum := exists_maximal_Lconsistented_theory
+
+-- noncomputable instance [System.Consistent Λ] : Inhabited (Λ, p)-MCT := ⟨lindenbaum (T := Subᶜ p) (by rfl) (by sorry) |>.choose⟩
+
+variable {Ω Ω₁ Ω₂ : (Λ, p)-MCT}
+variable {q r : Formula α}
+
+@[simp]
+lemma mem_sub_of_mem (h : q ∈ Ω.theory) : q ∈ Subᶜ p := by apply Ω.subset; assumption;
+
+lemma either_mem (Ω : (Λ, p)-MCT) {q} (hq : q ∈ Subᶜ p) : q ∈ Ω.theory ∨ ~q ∈ Ω.theory := by
+  by_contra hC; push_neg at hC;
+  cases either_consistent Ω.consistent q with
+  | inl h =>
+    have := Ω.maximal (show insert q Ω.theory ⊆ ↑(Subᶜ p) by
+      apply Set.insert_subset_iff.mpr;
+      constructor;
+      . sorry;
+      . exact Ω.subset;
+    ) (Set.ssubset_insert hC.1);
+    contradiction;
+  | inr h =>
+    have := Ω.maximal (show insert (~q) Ω.theory ⊆ ↑(Subᶜ p) by sorry) (Set.ssubset_insert hC.2);
+    contradiction;
+
+variable (q_sub : q ∈ Subᶜ p)
+
+lemma membership_iff : (q ∈ Ω.theory) ↔ (Ω.theory *⊢[Λ]! q) := by
+  constructor;
+  . intro h; exact Context.by_axm! h;
+  . intro hp;
+    suffices ~q ∉ Ω.theory by apply or_iff_not_imp_right.mp $ (either_mem Ω q_sub); assumption;
+    by_contra hC;
+    have hnp : Ω.theory *⊢[Λ]! ~q := Context.by_axm! hC;
+    have := neg_mdp! hnp hp;
+    have := not_provable_falsum Ω.consistent;
+    contradiction;
+
+@[simp]
+lemma not_mem_falsum : ⊥ ∉ Ω.theory := not_mem_falsum_of_Consistent Ω.consistent
+
+@[simp]
+lemma unprovable_falsum : Ω.theory *⊬[Λ]! ⊥ := by apply membership_iff (by sorry) |>.not.mp; simp;
+
+lemma iff_mem_neg : (~q ∈ Ω.theory) ↔ (q ∉ Ω.theory) := by
+  constructor;
+  . intro hnp;
+    by_contra hp;
+    replace hp := membership_iff q_sub |>.mp hp;
+    replace hnp := membership_iff (by sorry) |>.mp hnp;
+    have : Ω.theory *⊢[Λ]! ⊥ := neg_mdp! hnp hp;
+    have : Ω.theory *⊬[Λ]! ⊥ := unprovable_falsum;
+    contradiction;
+  . intro hp;
+    by_contra hnp;
+    sorry;
+
+/-
+lemma mem_neg_of_not_mem : q ∉ Ω.theory → ~q ∈ Ω.theory := by
+  intro h;
+  have := Ω.maximal
+-/
+
+end ComplementClosedMaximalConsistentTheory
+
+namespace PLoN
+
+abbrev CanonicalFrame2 (Λ : DeductionParameter α) (p : Formula α) [Inhabited (Λ, p)-MCT] : PLoN.FiniteFrame α where
+  World := (Λ, p)-MCT
+  Rel := λ q Ω₁ Ω₂ => □q ∉ Ω₁.theory ∨ q ∈ Ω₂.theory
+  World_finite := by
+    simp;
+    sorry;
+
+abbrev CanonicalModel2 (Λ : DeductionParameter α) (p : Formula α) [Inhabited (Λ, p)-MCT] : PLoN.FiniteModel α where
+  Frame := CanonicalFrame2 Λ p
+  Valuation Ω a := (atom a) ∈ Ω.theory
+
+namespace CanonicalModel2
+
+variable {p : Formula α} [Inhabited (Λ, p)-MCT]
+
+@[reducible]
+instance : Semantics (Formula α) (CanonicalModel2 Λ p).World := Formula.PLoN.Satisfies.semantics (M := (CanonicalModel2 Λ p).toModel)
+
+end CanonicalModel2
+
+variable {p q : Formula α} [Λ.HasNecessitation] [Inhabited (Λ, p)-MCT]
+
+open ComplementClosedMaximalConsistentTheory
+
+lemma truthlemma2 : ∀ {X : (CanonicalModel2 Λ p).World}, X ⊧ q ↔ (q ∈ X.theory) := by
+  intro X;
+  induction q using Formula.rec' with
+  | hbox s ih =>
+    constructor;
+    . contrapose;
+      intro hr;
+      have : ~(□s) ∈ X.theory := by
+        by_contra hC;
+        have h := X.maximal (U := (insert (□s) X.theory)) (by sorry) (by
+          apply Set.ssubset_iff_of_subset (by simp) |>.mpr;
+          use (□s); simpa;
+        );
+        sorry;
+      have d₁ := membership_iff (mem_sub_of_mem this) |>.mp this;
+      obtain ⟨Y, hY⟩ := lindenbaum (𝓓 := Λ) (p := p) (T := {~s}) (T_subset := by sorry) $ by
+        intro Γ hΓ hC;
+        have : Λ ⊢! ~s ⟶ ⊥ := replace_imply_left_conj'! hΓ hC;
+        have : Λ ⊢! □s := nec! $ dne'! $ neg_equiv'!.mpr this;
+        have : X.theory *⊢[Λ]! ⊥ := neg_mdp! d₁ (Context.of! this);
+        have : X.theory *⊬[Λ]! ⊥ := unprovable_falsum;
+        contradiction;
+
+      simp only [PLoN.Satisfies.iff_models, PLoN.Satisfies]; push_neg;
+      use Y;
+      constructor;
+      . constructor;
+        . sorry;
+        . sorry;
+      . sorry;
+    . intro h;
+      by_contra hC;
+      simp [PLoN.Satisfies] at hC;
+      simp_all only [PLoN.Satisfies.iff_models];
+  | _ =>
+    simp_all [PLoN.Satisfies];
+    try sorry;
+
+-- set_option pp.universes true in
+lemma complete_of_N : (AllFrameClass.{u, u} α)ꟳ ⊧ p → 𝐍 ⊢! p := by
+  contrapose; simp [PLoN.ValidOnFrameClass, PLoN.ValidOnFrame, PLoN.ValidOnModel];
+  intro h;
+  have : Inhabited (𝐍, p)-MCT := by sorry;
+  use (CanonicalFrame2 𝐍 p);
+  constructor;
+  . use (CanonicalFrame2 𝐍 p); simp;
+  . obtain ⟨Ω, hΩ⟩ := lindenbaum (p := p) (by simp; right; use p; simp) (Theory.complement_consistent h);
+    use (CanonicalModel2 𝐍 p).Valuation, Ω;
+    apply truthlemma2.not.mpr;
+    sorry;
+
+lemma serial_CanonicalFrame₂ [Λ.HasRosserRule] : (CanonicalFrame2 Λ p).toFrame.SerialOnTheory (Sub p) := by
+  intro q hq X; simp at hq;
+  by_cases h : (□q ∈ X.theory);
+  . obtain ⟨Y, hY⟩ := lindenbaum (𝓓 := Λ) (p := p) (T := {q}) (T_subset := by sorry) $ by sorry;
+    use Y; right; simp_all;
+  . use X; left; assumption;
+
+lemma transitive_CanonicalFrame₂ [Λ.HasAxiomFour] : (CanonicalFrame2 Λ p).toFrame.TransitiveOnTheory (Sub p) := by
+  intro q hq X Y Z hXY hYZ;
+  simp at hq;
+  by_cases h : (□q) ∈ X.theory;
+  . replace h := membership_iff (by sorry) |>.mp h;
+    have : □□q ∈ X.theory := by
+      apply membership_iff (by simp; left; exact hq) |>.mpr;
+      sorry;
+      -- exact axiomFour! h;
+    have : □q ∈ Y.theory := by rcases hXY with ⟨_⟩ | ⟨_⟩ <;> rcases hYZ with ⟨_⟩ | ⟨_⟩ <;> simp_all only
+    have : q ∈ Z.theory := by rcases hXY with ⟨_⟩ | ⟨_⟩ <;> rcases hYZ with ⟨_⟩ | ⟨_⟩ <;> simp_all only;
+    right; assumption;
+  . left; assumption;
+
+
 end PLoN
 
+end
+
 end LO.Modal.Standard
diff --git a/Logic/Modal/Standard/PLoN/Semantics.lean b/Logic/Modal/Standard/PLoN/Semantics.lean
index ae41fb98..952e22f8 100644
--- a/Logic/Modal/Standard/PLoN/Semantics.lean
+++ b/Logic/Modal/Standard/PLoN/Semantics.lean
@@ -33,6 +33,20 @@ abbrev terminalFrame (α) : FiniteFrame α where
 
 abbrev FrameClass (α : Type*) := Set (PLoN.Frame α)
 
+abbrev FiniteFrameClass (α : Type*) := Set (PLoN.FiniteFrame α)
+
+
+abbrev FrameClass.restrictFinite (𝔽 : FrameClass α) : FiniteFrameClass α := { F | F.toFrame ∈ 𝔽 }
+
+lemma FrameClass.iff_mem_restrictFinite {𝔽 : FrameClass α} (h : F ∈ 𝔽) : (finite : Finite F.World) → ⟨F⟩ ∈ 𝔽.restrictFinite := by
+  simp_all [FrameClass.restrictFinite];
+
+@[simp]
+def FiniteFrameClass.toFrameClass (𝔽 : FiniteFrameClass α) : FrameClass α := { F | ∃ F', F' ∈ 𝔽 ∧ F'.toFrame = F }
+
+abbrev FrameClass.restrictFinite' (𝔽 : FrameClass α) : FrameClass α := 𝔽.restrictFinite.toFrameClass
+postfix:max "ꟳ" => FrameClass.restrictFinite'
+
 
 abbrev Valuation (F : PLoN.Frame α) (α : Type*) := F.World → α → Prop
 
@@ -43,7 +57,10 @@ structure Model (α) where
 abbrev Model.World (M : PLoN.Model α) := M.Frame.World
 instance : CoeSort (PLoN.Model α) (Type _) := ⟨Model.World⟩
 
+structure FiniteModel (α) extends Model α where
+  [World_finite : Finite World]
 
+abbrev FiniteModel.FiniteFrame (M : PLoN.FiniteModel α) : PLoN.FiniteFrame α := { toFrame := M.Frame, World_finite := M.World_finite }
 
 end PLoN
 
@@ -216,16 +233,26 @@ variable (F : Frame α)
 
 def SerialOnFormula (p : Formula α) : Prop := Serial (F.Rel' p)
 
-def SerialOnTheory (T : Theory α) : Prop := ∀ p ∈ T, F.SerialOnFormula p
+def SerialOnTheory (T : Theory α) : Prop := ∀ p ∈ □''⁻¹T, F.SerialOnFormula p
 
-protected def Serial : Prop := ∀ p, F.SerialOnFormula p
+protected def Serial : Prop := F.SerialOnTheory Set.univ
 
+/-
+lemma serialOnTheory_of_serial (hSerial : F.Serial) : F.SerialOnTheory T := by
+  intro q _;
+  exact hSerial q;
+-/
 
 def TransitiveOnFormula (p : Formula α) : Prop := ∀ {x y z : F.World}, x ≺[□p] y → y ≺[p] z → x ≺[p] z
 
-def TransitiveOnTheory (T : Theory α) : Prop := ∀ p ∈ T, F.SerialOnFormula p
+def TransitiveOnTheory (T : Theory α) : Prop := ∀ p ∈ □''⁻¹^[2]T, F.TransitiveOnFormula p
 
-protected def Transitive (F : Frame α) := ∀ p, F.TransitiveOnFormula p
+protected def Transitive (F : Frame α) := F.TransitiveOnTheory Set.univ
+
+/-
+lemma transitiveOnTheory_of_transitive (hTrans : F.Transitive) : F.TransitiveOnTheory T := by
+  intro q _; exact hTrans q;
+-/
 
 end Frame
 
@@ -249,13 +276,14 @@ abbrev TransitiveFrameClass (α) : PLoN.FrameClass α := { F | Frame.Transitive
 
 lemma TransitiveFrameClass.nonempty : (TransitiveFrameClass.{_, 0} α).Nonempty := by
   use terminalFrame α;
-  simp [Frame.Transitive, Frame.TransitiveOnFormula];
+  simp [Frame.Transitive, Frame.TransitiveOnTheory, Frame.TransitiveOnFormula];
 
 
 abbrev SerialFrameClass (α) : PLoN.FrameClass α := { F | Frame.Serial F }
 
 lemma SerialFrameClass.nonempty : (SerialFrameClass.{_, 0} α).Nonempty := by
   use terminalFrame α;
+  simp [Frame.Serial, Frame.SerialOnTheory, Frame.SerialOnFormula];
   intro p x; use x;
 
 
@@ -263,7 +291,7 @@ abbrev TransitiveSerialFrameClass (α) : PLoN.FrameClass α := { F | F.Transitiv
 
 lemma TransitiveSerialFrameClass.nonempty : (TransitiveSerialFrameClass.{_, 0} α).Nonempty := by
   use terminalFrame α;
-  simp [Frame.Transitive, Frame.Serial, Frame.TransitiveOnFormula, Frame.SerialOnFormula];
+  simp [Frame.Transitive, Frame.TransitiveOnTheory, Frame.TransitiveOnFormula, Frame.Serial, Frame.SerialOnTheory, Frame.SerialOnFormula];
   intro p x; use x;
 
 
@@ -274,7 +302,7 @@ lemma N4_characterized : 𝐍𝟒.CharacterizedByPLoNFrameClass (TransitiveFrame
   induction hp using Deduction.inducition_with_necOnly! with
   | hMaxm h =>
     obtain ⟨p, e⟩ := h; subst e;
-    exact validAxiomFour_of_transitive (hTrans p);
+    exact validAxiomFour_of_transitive $ hTrans p (by simp_all);
   | hMdp ihpq ihp => exact PLoN.ValidOnFrame.mdp ihpq ihp;
   | hNec ihp => exact PLoN.ValidOnFrame.nec ihp;
   | hOrElim => exact PLoN.ValidOnFrame.disj₃;
@@ -292,7 +320,7 @@ lemma NRosser_characterized : 𝐍(𝐑).CharacterizedByPLoNFrameClass (SerialFr
     . obtain ⟨p, e⟩ := hNec; subst e; simp_all;
       exact PLoN.ValidOnFrame.nec ih;
     . obtain ⟨p, e⟩ := hRosser; subst e; simp_all;
-      exact validRosserRule_of_serial (hSerial _) ih;
+      exact validRosserRule_of_serial (hSerial p (by simp_all)) ih;
   | hOrElim => exact PLoN.ValidOnFrame.disj₃;
   | _ => simp_all [PLoN.Satisfies];
 
@@ -304,17 +332,18 @@ lemma N4Rosser_characterized : 𝐍𝟒(𝐑).CharacterizedByPLoNFrameClass (Tra
   induction hp using Deduction.inducition! with
   | hMaxm h =>
     obtain ⟨p, e⟩ := h; subst e;
-    exact validAxiomFour_of_transitive (hTrans p);
+    exact validAxiomFour_of_transitive $ hTrans p (by simp_all);
   | hMdp ihpq ihp => exact PLoN.ValidOnFrame.mdp ihpq ihp;
   | hRules rl hrl hant ih =>
     rcases hrl with (hNec | hRosser)
     . obtain ⟨p, e⟩ := hNec; subst e; simp_all;
       exact PLoN.ValidOnFrame.nec ih;
     . obtain ⟨p, e⟩ := hRosser; subst e; simp_all;
-      exact validRosserRule_of_serial (hSerial _) ih;
+      exact validRosserRule_of_serial (hSerial (□p) (by simp_all)) ih;
   | hOrElim => exact PLoN.ValidOnFrame.disj₃;
   | _ => simp_all [PLoN.Satisfies];
 
+
 end PLoN
 
 end LO.Modal.Standard
diff --git a/Logic/Modal/Standard/PLoN/Soundness.lean b/Logic/Modal/Standard/PLoN/Soundness.lean
index 11afd5fc..b2ed96f0 100644
--- a/Logic/Modal/Standard/PLoN/Soundness.lean
+++ b/Logic/Modal/Standard/PLoN/Soundness.lean
@@ -24,7 +24,6 @@ lemma consistent_of_characterized (characterized : Λ.CharacterizedByPLoNFrameCl
   apply System.Consistent.of_unprovable;
   exact unprovable_bot_of_nonempty_frameclass characterized nonempty;
 
-
 instance : Sound 𝐍 (AllFrameClass α) := sound_of_characterized N_characterized
 
 instance : Sound 𝐍𝟒 (TransitiveFrameClass α) := sound_of_characterized N4_characterized
@@ -41,6 +40,16 @@ instance : System.Consistent (𝐍(𝐑) : DeductionParameter α) := consistent_
 
 instance : System.Consistent (𝐍𝟒(𝐑) : DeductionParameter α) := consistent_of_characterized N4Rosser_characterized TransitiveSerialFrameClass.nonempty
 
+lemma restrict_finite : 𝔽 ⊧ p → 𝔽ꟳ ⊧ p := by
+  intro h F hF;
+  obtain ⟨fF, hfF, e⟩ := hF; subst e;
+  exact h hfF;
+
+instance {𝔽 : FrameClass α} [sound : Sound Λ 𝔽] : Sound Λ 𝔽ꟳ := ⟨by
+  intro p h;
+  exact restrict_finite $ sound.sound h;
+⟩
+
 end PLoN
 
 end LO.Modal.Standard
diff --git a/Logic/Modal/Standard/System.lean b/Logic/Modal/Standard/System.lean
index 23d2b913..4c39ffeb 100644
--- a/Logic/Modal/Standard/System.lean
+++ b/Logic/Modal/Standard/System.lean
@@ -23,6 +23,12 @@ class LoebRule where
 class HenkinRule where
   henkin {p : F} : 𝓢 ⊢ □p ⟷ p → 𝓢 ⊢ p
 
+class RosserRule where
+  rosser {p : F} : 𝓢 ⊢ ~p → 𝓢 ⊢ ~(□p)
+
+class RosserBoxRule where
+  rosser_box {p : F} : 𝓢 ⊢ ~(□p) → 𝓢 ⊢ ~(□□p)
+
 class HasAxiomK where
   K (p q : F) : 𝓢 ⊢ Axioms.K p q
 

From b9359b30ad20bce39fcea9102b48522d603eeafc Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Tue, 27 Aug 2024 21:13:28 +0900
Subject: [PATCH 8/8] fx

---
 Logic/Modal/Standard/PLoN/Semantics.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Logic/Modal/Standard/PLoN/Semantics.lean b/Logic/Modal/Standard/PLoN/Semantics.lean
index 952e22f8..8c6a74d0 100644
--- a/Logic/Modal/Standard/PLoN/Semantics.lean
+++ b/Logic/Modal/Standard/PLoN/Semantics.lean
@@ -305,7 +305,7 @@ lemma N4_characterized : 𝐍𝟒.CharacterizedByPLoNFrameClass (TransitiveFrame
     exact validAxiomFour_of_transitive $ hTrans p (by simp_all);
   | hMdp ihpq ihp => exact PLoN.ValidOnFrame.mdp ihpq ihp;
   | hNec ihp => exact PLoN.ValidOnFrame.nec ihp;
-  | hOrElim => exact PLoN.ValidOnFrame.disj₃;
+  | hElimContra => exact PLoN.ValidOnFrame.elim_contra;
   | _ => simp_all [PLoN.Satisfies];
 
 lemma NRosser_characterized : 𝐍(𝐑).CharacterizedByPLoNFrameClass (SerialFrameClass α) := by
@@ -321,7 +321,7 @@ lemma NRosser_characterized : 𝐍(𝐑).CharacterizedByPLoNFrameClass (SerialFr
       exact PLoN.ValidOnFrame.nec ih;
     . obtain ⟨p, e⟩ := hRosser; subst e; simp_all;
       exact validRosserRule_of_serial (hSerial p (by simp_all)) ih;
-  | hOrElim => exact PLoN.ValidOnFrame.disj₃;
+  | hElimContra => exact PLoN.ValidOnFrame.elim_contra;
   | _ => simp_all [PLoN.Satisfies];
 
 -- TODO: `theory 𝐍𝟒 ∪ theory 𝐍(𝐑) = theory 𝐍𝟒(𝐑)`という事実を示せば共通部分だけで簡単に特徴づけられる気がする
@@ -340,7 +340,7 @@ lemma N4Rosser_characterized : 𝐍𝟒(𝐑).CharacterizedByPLoNFrameClass (Tra
       exact PLoN.ValidOnFrame.nec ih;
     . obtain ⟨p, e⟩ := hRosser; subst e; simp_all;
       exact validRosserRule_of_serial (hSerial (□p) (by simp_all)) ih;
-  | hOrElim => exact PLoN.ValidOnFrame.disj₃;
+  | hElimContra => exact PLoN.ValidOnFrame.elim_contra;
   | _ => simp_all [PLoN.Satisfies];