From 625c054a6df62a94e86f7ebddac174a7b6b466fd Mon Sep 17 00:00:00 2001 From: SnO2WMaN 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 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 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 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 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 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 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 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];