From a93da70394e6e3fe0217fad15644bb94e8d0c324 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Sun, 2 Mar 2025 04:37:15 +0900 Subject: [PATCH] Soundness of KD4.3Z wip --- Foundation.lean | 1 + Foundation/Modal/Axioms.lean | 2 + Foundation/Modal/Entailment/Basic.lean | 19 +++++ Foundation/Modal/Hilbert/WellKnown.lean | 21 +++++ Foundation/Modal/Kripke/AxiomGeach.lean | 25 +++--- Foundation/Modal/Kripke/AxiomGrz.lean | 4 +- Foundation/Modal/Kripke/AxiomWeakDot3.lean | 6 +- .../Modal/Kripke/Hilbert/KD4Point3Z.lean | 84 +++++++++++++++++++ Foundation/Modal/Logic/WellKnown.lean | 1 + 9 files changed, 147 insertions(+), 16 deletions(-) create mode 100644 Foundation/Modal/Kripke/Hilbert/KD4Point3Z.lean diff --git a/Foundation.lean b/Foundation.lean index aa9f0e58..3628ed90 100644 --- a/Foundation.lean +++ b/Foundation.lean @@ -80,6 +80,7 @@ import Foundation.Modal.Kripke.Hilbert.S4Dot3 import Foundation.Modal.Kripke.Hilbert.S5 import Foundation.Modal.Kripke.Hilbert.Triv import Foundation.Modal.Kripke.Hilbert.Ver +import Foundation.Modal.Kripke.Hilbert.KD4Point3Z import Foundation.Modal.Kripke.Hilbert.GL.Unnecessitation import Foundation.Modal.Kripke.Hilbert.GL.MDP diff --git a/Foundation/Modal/Axioms.lean b/Foundation/Modal/Axioms.lean index 2bb027ff..20ccb147 100644 --- a/Foundation/Modal/Axioms.lean +++ b/Foundation/Modal/Axioms.lean @@ -109,6 +109,8 @@ protected abbrev H := □(□φ ⭤ φ) ➝ □φ abbrev H.set : Set F := { Axioms.H φ | (φ) } notation:max "𝗛" => H.set +protected abbrev Z := □(□φ ➝ φ) ➝ (◇□φ ➝ □φ) + end Basic protected abbrev Geach (t : Geachean.Taple) (φ : F) := ◇^[t.i](□^[t.m]φ) ➝ □^[t.j](◇^[t.n]φ) diff --git a/Foundation/Modal/Entailment/Basic.lean b/Foundation/Modal/Entailment/Basic.lean index 498ae0ee..a9a9cb34 100644 --- a/Foundation/Modal/Entailment/Basic.lean +++ b/Foundation/Modal/Entailment/Basic.lean @@ -441,6 +441,23 @@ instance (Γ : Context F 𝓢) : HasAxiomH Γ := ⟨fun _ ↦ Context.of axiomH end +class HasAxiomZ (𝓢 : S) where + Z (φ : F) : 𝓢 ⊢ Axioms.Z φ + +section + +variable [HasAxiomZ 𝓢] + +def axiomZ : 𝓢 ⊢ □(□φ ➝ φ) ➝ (◇□φ ➝ □φ) := HasAxiomZ.Z _ +@[simp] lemma axiomZ! : 𝓢 ⊢! □(□φ ➝ φ) ➝ (◇□φ ➝ □φ) := ⟨axiomZ⟩ + +variable [Entailment.Minimal 𝓢] + +instance (Γ : FiniteContext F 𝓢) : HasAxiomZ Γ := ⟨fun _ ↦ FiniteContext.of axiomZ⟩ +instance (Γ : Context F 𝓢) : HasAxiomZ Γ := ⟨fun _ ↦ Context.of axiomZ⟩ + +end + section variable [BasicModalLogicalConnective F] [DecidableEq F] @@ -513,6 +530,8 @@ protected class K4 extends Entailment.K 𝓢, HasAxiomFour 𝓢 protected class K4Dot2 extends Entailment.K 𝓢, HasAxiomFour 𝓢, HasAxiomWeakDot2 𝓢 protected class K4Dot3 extends Entailment.K 𝓢, HasAxiomFour 𝓢, HasAxiomWeakDot3 𝓢 +protected class KD4Point3Z extends Entailment.K 𝓢, HasAxiomD 𝓢, HasAxiomFour 𝓢, HasAxiomWeakDot3 𝓢, HasAxiomZ 𝓢 + protected class K5 extends Entailment.K 𝓢, HasAxiomFive 𝓢 protected class S4 extends Entailment.K 𝓢, HasAxiomT 𝓢, HasAxiomFour 𝓢 diff --git a/Foundation/Modal/Hilbert/WellKnown.lean b/Foundation/Modal/Hilbert/WellKnown.lean index 585f8da7..b63a54c7 100644 --- a/Foundation/Modal/Hilbert/WellKnown.lean +++ b/Foundation/Modal/Hilbert/WellKnown.lean @@ -214,6 +214,19 @@ instance [hH : H.HasH] : Entailment.HasAxiomH H where . use (λ b => if hH.p = b then φ else (.atom b)); simp; +class HasZ (H : Hilbert α) where + p : α + mem_Z : Axioms.Z (.atom p) ∈ H.axioms := by tauto; + +instance [hZ : H.HasZ] : Entailment.HasAxiomZ H where + Z φ := by + apply maxm; + use Axioms.Z (.atom hZ.p); + constructor; + . exact hZ.mem_Z; + . use (λ b => if hZ.p = b then φ else (.atom b)); + simp; + end protected abbrev KT : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.T (.atom 0)}⟩ @@ -265,6 +278,14 @@ instance : (Hilbert.K4Dot3).HasFour where p := 0 instance : (Hilbert.K4Dot3).HasWeakDot3 where p := 0; q := 1; instance : Entailment.K4Dot3 (Hilbert.K4Dot3) where +protected abbrev KD4Point3Z : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.D (.atom 0), Axioms.Four (.atom 0), Axioms.WeakDot3 (.atom 0) (.atom 1), Axioms.Z (.atom 0)}⟩ +instance : (Hilbert.KD4Point3Z).HasK where p := 0; q := 1; +instance : (Hilbert.KD4Point3Z).HasD where p := 0 +instance : (Hilbert.KD4Point3Z).HasFour where p := 0 +instance : (Hilbert.KD4Point3Z).HasWeakDot3 where p := 0; q := 1; +instance : (Hilbert.KD4Point3Z).HasZ where p := 0 +instance : Entailment.KD4Point3Z (Hilbert.KD4Point3Z) where + protected abbrev KT4B : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.T (.atom 0), Axioms.Four (.atom 0), Axioms.B (.atom 0)}⟩ instance : (Hilbert.KT4B).HasK where p := 0; q := 1; instance : (Hilbert.KT4B).HasT where p := 0 diff --git a/Foundation/Modal/Kripke/AxiomGeach.lean b/Foundation/Modal/Kripke/AxiomGeach.lean index f06318aa..07b14924 100644 --- a/Foundation/Modal/Kripke/AxiomGeach.lean +++ b/Foundation/Modal/Kripke/AxiomGeach.lean @@ -51,17 +51,20 @@ section variable {F : Frame} -lemma reflexive_of_validate_AxiomT (h : F ⊧ (Axioms.T (.atom 0))) : Reflexive F.Rel := by - have : ValidOnFrame F (Axioms.T (.atom 0)) → Reflexive F.Rel := by - simpa [Axioms.Geach, MultiGeachean, ←Geachean.reflexive_def] using - MultiGeacheanFrameClass.isDefinedByGeachAxioms {⟨0, 0, 1, 0⟩} |>.defines F |>.mpr; - exact this h; - -lemma transitive_of_validate_AxiomFour (h : F ⊧ (Axioms.Four (.atom 0))) : Transitive F.Rel := by - have : ValidOnFrame F (Axioms.Four (.atom 0)) → Transitive F.Rel := by - simpa [Axioms.Geach, MultiGeachean, ←Geachean.transitive_def] using - MultiGeacheanFrameClass.isDefinedByGeachAxioms {⟨0, 2, 1, 0⟩} |>.defines F |>.mpr; - exact this h; +lemma defines_reflexive : Reflexive F.Rel ↔ F ⊧ (Axioms.T (.atom 0)) := by + simpa [MultiGeachean, ←Geachean.reflexive_def, Axioms.Geach] using + MultiGeacheanFrameClass.isDefinedByGeachAxioms {⟨0, 0, 1, 0⟩} |>.defines F +alias ⟨validate_axiomT_of_reflexive, reflexive_of_validate_axiomT⟩ := defines_reflexive + +lemma deines_transitive : Transitive F.Rel ↔ F ⊧ (Axioms.Four (.atom 0)) := by + simpa [MultiGeachean, ←Geachean.transitive_def, Axioms.Geach] using + MultiGeacheanFrameClass.isDefinedByGeachAxioms {⟨0, 2, 1, 0⟩} |>.defines F +alias ⟨validate_axiomFour_of_transitive, transitive_of_validate_axiomFour⟩ := deines_transitive + +lemma defines_serial : Serial F.Rel ↔ F ⊧ (Axioms.D (.atom 0)) := by + simpa [MultiGeachean, ←Geachean.serial_def, Axioms.Geach] using + MultiGeacheanFrameClass.isDefinedByGeachAxioms {⟨0, 0, 1, 1⟩} |>.defines F +alias ⟨validate_axiomD_of_serial, serial_of_validate_axiomD⟩ := defines_serial end diff --git a/Foundation/Modal/Kripke/AxiomGrz.lean b/Foundation/Modal/Kripke/AxiomGrz.lean index 6023e611..15513336 100644 --- a/Foundation/Modal/Kripke/AxiomGrz.lean +++ b/Foundation/Modal/Kripke/AxiomGrz.lean @@ -96,7 +96,7 @@ lemma validate_T_of_validate_Grz (h : F ⊧ Axioms.Grz (.atom 0)) : F ⊧ (Axiom exact Satisfies.and_def.mp (validate_T_Four_of_validate_Grz h V x hx) |>.1; lemma reflexive_of_validate_Grz (h : F ⊧ Axioms.Grz (.atom 0)) : Reflexive F := by - apply reflexive_of_validate_AxiomT; + apply reflexive_of_validate_axiomT; simpa using validate_T_of_validate_Grz h; lemma validate_Four_of_validate_Grz (h : F ⊧ Axioms.Grz (.atom 0)) : F ⊧ (Axioms.Four (.atom 0)) := by @@ -104,7 +104,7 @@ lemma validate_Four_of_validate_Grz (h : F ⊧ Axioms.Grz (.atom 0)) : F ⊧ (Ax exact Satisfies.and_def.mp (validate_T_Four_of_validate_Grz h V x hx) |>.2; lemma transitive_of_validate_Grz (h : F ⊧ Axioms.Grz (.atom 0)) : Transitive F := by - apply transitive_of_validate_AxiomFour; + apply transitive_of_validate_axiomFour; simpa using validate_Four_of_validate_Grz h; lemma WCWF_of_validate_Grz (h : F ⊧ Axioms.Grz (.atom 0)) : WCWF F := by diff --git a/Foundation/Modal/Kripke/AxiomWeakDot3.lean b/Foundation/Modal/Kripke/AxiomWeakDot3.lean index d6d5dc69..3be7b49a 100644 --- a/Foundation/Modal/Kripke/AxiomWeakDot3.lean +++ b/Foundation/Modal/Kripke/AxiomWeakDot3.lean @@ -12,7 +12,7 @@ open Formula.Kripke variable {F : Kripke.Frame} -lemma weakConnected_of_validate_WeakDot3 (hCon : WeakConnected F) : F ⊧ (Axioms.WeakDot3 (.atom 0) (.atom 1)) := by +lemma validate_WeakDot3_of_weakConnected (hCon : WeakConnected F) : F ⊧ (Axioms.WeakDot3 (.atom 0) (.atom 1)) := by rintro V x; apply Satisfies.or_def.mpr; suffices @@ -30,7 +30,7 @@ lemma weakConnected_of_validate_WeakDot3 (hCon : WeakConnected F) : F ⊧ (Axiom . have := hz _ Ryz; contradiction; . have := hy _ Rzy; contradiction; -lemma validate_WeakDot3_of_weakConnected : F ⊧ (Axioms.WeakDot3 (.atom 0) (.atom 1)) → WeakConnected F := by +lemma weakConnected_of_validate_WeakDot3 : F ⊧ (Axioms.WeakDot3 (.atom 0) (.atom 1)) → WeakConnected F := by contrapose; intro hCon; obtain ⟨x, y, Rxy, z, Rxz, nyz, nRyz, nRzy⟩ := by simpa [WeakConnected] using hCon; @@ -64,8 +64,8 @@ instance : WeakConnectedFrameClass.IsNonempty := by instance WeakConnectedFrameClass.DefinedByWeakDot3 : WeakConnectedFrameClass.DefinedBy {Axioms.WeakDot3 (.atom 0) (.atom 1)} := ⟨by intro F; constructor; - . simpa using weakConnected_of_validate_WeakDot3; . simpa using validate_WeakDot3_of_weakConnected; + . simpa using weakConnected_of_validate_WeakDot3; ⟩ end definability diff --git a/Foundation/Modal/Kripke/Hilbert/KD4Point3Z.lean b/Foundation/Modal/Kripke/Hilbert/KD4Point3Z.lean new file mode 100644 index 00000000..eeb8c852 --- /dev/null +++ b/Foundation/Modal/Kripke/Hilbert/KD4Point3Z.lean @@ -0,0 +1,84 @@ +import Foundation.Modal.Kripke.Completeness +import Foundation.Modal.Hilbert.WellKnown +import Foundation.Modal.Kripke.AxiomWeakDot3 +import Foundation.Modal.Kripke.AxiomGeach +import Mathlib.Order.Interval.Finset.Nat + +namespace LO.Modal + +namespace Kripke + + +section definability + +open Formula (atom) +open Formula.Kripke + +variable {F : Kripke.Frame} + +def natLtFrame : Kripke.Frame where + World := ℕ + Rel x y := x < y + +namespace natLtFrame + +protected lemma serial : Serial natLtFrame.Rel := by + rintro x; + unfold natLtFrame at *; + use x + 1; + omega; + +protected lemma transitive : Transitive natLtFrame.Rel := by simp [Transitive, natLtFrame]; omega; + +protected lemma wellConnected : WeakConnected natLtFrame.Rel := by + rintro x y z ⟨Rxy, Rxz, hyz⟩; + unfold natLtFrame at x y z; + rcases lt_trichotomy y z with (Ryz | rfl | Rzy) <;> tauto; + +end natLtFrame + +lemma natLtFrame_validates_axiomZ : natLtFrame ⊧ (Axioms.Z (.atom 0)) := by + rintro V x; + intro h₁ h₂ y Rxy; + obtain ⟨z, Rxz, h₃⟩ := Satisfies.dia_def.mp h₂; + unfold natLtFrame at x y z; + rcases lt_trichotomy y z with (Ryz | rfl | Rzy); + . apply h₁ _ Rxy; + suffices ∀ i ∈ Finset.Ioo y z, Satisfies ⟨natLtFrame, V⟩ i (.atom 0) by + intro u Ryu; + simp only [natLtFrame, Frame.Rel'] at u Ryu; + rcases (lt_trichotomy u z) with (Ruz | rfl | Rzu); + . apply this; simp_all [Finset.mem_Ioo]; + . exact h₁ _ Rxz $ h₃; + . apply h₃ _ Rzu; + /- + Now consider z - 1. + We know z ⊧ 0 and z ⊧ □0, imedeiately proves any u > z, u ⊧ 0, so z - 1 ⊧ □0. + By hypothesis, z - 1 ⊧ □0 ➝ 0, so z - 1 ⊧ 0. + By similar arguents (by induction), z - 2, z - 3, ... y ⊧ 0. + -/ + sorry; + . exact h₁ y Rxy $ h₃; + . exact h₃ _ Rzy; + +lemma Hilbert.KD4Point3Z.Kripke.sound : Hilbert.KD4Point3Z ⊢! φ → natLtFrame ⊧ φ := by + intro hφ; + induction hφ using Hilbert.Deduction.rec! with + | maxm h => + rcases (by simpa using h) with ⟨s, rfl⟩ | ⟨s, rfl⟩ | ⟨s, rfl⟩ | ⟨s, rfl⟩ | ⟨s, rfl⟩; + . tauto; + . exact ValidOnFrame.subst $ validate_axiomD_of_serial natLtFrame.serial; + . exact ValidOnFrame.subst $ validate_axiomFour_of_transitive natLtFrame.transitive; + . exact ValidOnFrame.subst $ validate_WeakDot3_of_weakConnected natLtFrame.wellConnected; + . exact ValidOnFrame.subst $ natLtFrame_validates_axiomZ; + | mdp ihpq ihp => exact ValidOnFrame.mdp ihpq ihp; + | nec ih => exact ValidOnFrame.nec ih; + | imply₁ => exact ValidOnFrame.imply₁; + | imply₂ => exact ValidOnFrame.imply₂; + | ec => exact ValidOnFrame.elimContra; + +end definability + +end Kripke + +end LO.Modal diff --git a/Foundation/Modal/Logic/WellKnown.lean b/Foundation/Modal/Logic/WellKnown.lean index ad22a836..ebc254a6 100644 --- a/Foundation/Modal/Logic/WellKnown.lean +++ b/Foundation/Modal/Logic/WellKnown.lean @@ -81,6 +81,7 @@ protected abbrev KD4 : Logic := Hilbert.KD4.logic lemma KD4.eq_SerialTransitiveKripkeFrameClass_Logic : Logic.KD4 = Kripke.SerialTransitiveFrameClass.logic := eq_Hilbert_Logic_KripkeFrameClass_Logic +protected abbrev KD4Point3Z : Logic := Hilbert.KD4Point3Z.logic protected abbrev KD45 : Logic := Hilbert.KD45.logic lemma KD45.eq_SerialTransitiveEuclideanKripkeFrameClass_Logic : Logic.KD45 = Kripke.SerialTransitiveEuclideanFrameClass.logic