From b8e39aed3dd850a60a248755815bf358cbab9461 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?SnO=E2=82=82WMaN?= Date: Sun, 10 Nov 2024 23:34:36 +0900 Subject: [PATCH] Rewriting Kripke Semantics for IntProp (#155) * wip * wip * fix to N * frameclass hilbert * cleanup * disjunctive * fx4modal * wlem of dumeett * wip. remove LEM temporary * remove comment --- Foundation/IntProp/ConsistentTableau.lean | 4 +- Foundation/IntProp/Deduction.lean | 9 +- Foundation/IntProp/Formula.lean | 28 + Foundation/IntProp/Kripke/Classical.lean | 57 ++ Foundation/IntProp/Kripke/Completeness.lean | 153 ++--- Foundation/IntProp/Kripke/DP.lean | 169 +++-- Foundation/IntProp/Kripke/Kripke.lean | 5 +- Foundation/IntProp/Kripke/LEM.lean | 294 +++++---- Foundation/IntProp/Kripke/Semantics.lean | 594 +++++++++--------- Foundation/Logic/Axioms.lean | 6 +- Foundation/Logic/HilbertStyle/Basic.lean | 4 +- .../Logic/HilbertStyle/Supplemental.lean | 23 + Foundation/Logic/Kripke/Basic.lean | 2 +- Foundation/Modal/Geach.lean | 4 +- Foundation/Modal/Maximal.lean | 34 +- Foundation/Modal/ModalCompanion/GMT.lean | 38 +- Foundation/Vorspiel/BinaryRelations.lean | 31 +- 17 files changed, 806 insertions(+), 649 deletions(-) create mode 100644 Foundation/IntProp/Kripke/Classical.lean diff --git a/Foundation/IntProp/ConsistentTableau.lean b/Foundation/IntProp/ConsistentTableau.lean index 84bc071e..fde6f763 100644 --- a/Foundation/IntProp/ConsistentTableau.lean +++ b/Foundation/IntProp/ConsistentTableau.lean @@ -183,7 +183,7 @@ end Saturated variable [H.IncludeEFQ] -lemma self_consistent [h : System.Consistent H] : Tableau.Consistent H (H.axioms, ∅) := by +lemma self_consistent [h : H.Consistent] : Tableau.Consistent H (H.axioms, ∅) := by intro Γ Δ hΓ hΔ; replace hΔ : Δ = [] := List.nil_iff.mpr hΔ; obtain ⟨ψ, hq⟩ := h.exists_unprovable; @@ -339,7 +339,7 @@ lemma lindenbaum [H.IncludeEFQ] [Encodable α] (hCon : Tableau.Consistent H t₀ obtain ⟨t, ht, hCon, hMax⟩ := Tableau.lindenbaum hCon; exact ⟨⟨t, hMax, hCon⟩, ht⟩; -instance [System.Consistent H] [H.IncludeEFQ] [Encodable α] : Nonempty (SCT H) := ⟨lindenbaum Tableau.self_consistent |>.choose⟩ +instance [H.Consistent] [H.IncludeEFQ] [Encodable α] : Nonempty (SCT H) := ⟨lindenbaum Tableau.self_consistent |>.choose⟩ variable {t : SCT H} diff --git a/Foundation/IntProp/Deduction.lean b/Foundation/IntProp/Deduction.lean index 6a375a75..f38292f6 100644 --- a/Foundation/IntProp/Deduction.lean +++ b/Foundation/IntProp/Deduction.lean @@ -113,6 +113,7 @@ instance : IncludeEFQ (α := α) (Hilbert.LC α) where instance : System.HasAxiomDummett (Hilbert.LC α) where dummett φ ψ := by apply eaxm; aesop; + -- MEMO: Minimal <ₛ WeakMinimal <ₛ WeakClassical <ₛ Classical /-- @@ -129,6 +130,8 @@ protected abbrev WeakClassical : Hilbert α := ⟨𝗣𝗲⟩ end systems +abbrev Consistent (H : Hilbert α) := System.Consistent H + namespace Deduction @@ -189,7 +192,11 @@ lemma KC_weaker_than_Cl : (Hilbert.KC α) ≤ₛ (Hilbert.Cl α) := weaker_than_ lemma LC_weaker_than_Cl [DecidableEq α] : (Hilbert.LC α) ≤ₛ (Hilbert.Cl α) := by apply weaker_than_of_subset_axiomset'; - rintro φ (⟨_, rfl⟩ | ⟨_, _, rfl⟩) <;> simp; + rintro φ (⟨_, rfl⟩ | ⟨_, _, rfl⟩) <;> simp [efq!, dummett!]; + +lemma KC_weaker_than_LC [DecidableEq α] : (Hilbert.KC α) ≤ₛ (Hilbert.LC α) := by + apply weaker_than_of_subset_axiomset'; + rintro φ (⟨_, rfl⟩ | ⟨_, rfl⟩) <;> simp [efq!, wlem!]; end diff --git a/Foundation/IntProp/Formula.lean b/Foundation/IntProp/Formula.lean index f74ac39f..d68008e5 100644 --- a/Foundation/IntProp/Formula.lean +++ b/Foundation/IntProp/Formula.lean @@ -228,6 +228,34 @@ instance : Encodable (Formula α) where end Encodable + +section subst + +def subst (s : α → Formula α): Formula α → Formula α + | atom a => s a + | ⊤ => ⊤ + | ⊥ => ⊥ + | ∼φ => ∼(φ.subst s) + | φ ➝ ψ => φ.subst s ➝ ψ.subst s + | φ ⋏ ψ => φ.subst s ⋏ ψ.subst s + | φ ⋎ ψ => φ.subst s ⋎ ψ.subst s + +section + +variable {s : α → Formula α} {φ ψ : Formula α} + +@[simp] lemma subst_atom {a : α} : (atom a).subst s = s a := rfl +@[simp] lemma subst_and : (φ ⋏ ψ).subst s = φ.subst s ⋏ ψ.subst s := rfl +@[simp] lemma subst_or : (φ ⋎ ψ).subst s = φ.subst s ⋎ ψ.subst s := rfl +@[simp] lemma subst_imp : (φ ➝ ψ).subst s = φ.subst s ➝ ψ.subst s := rfl +@[simp] lemma subst_neg : (∼φ).subst s = ∼(φ.subst s) := rfl +@[simp] lemma subst_top : (⊤ : Formula α).subst s = ⊤ := rfl +@[simp] lemma subst_bot : (⊥ : Formula α).subst s = ⊥ := rfl + +end + +end subst + end Formula diff --git a/Foundation/IntProp/Kripke/Classical.lean b/Foundation/IntProp/Kripke/Classical.lean new file mode 100644 index 00000000..7d8d3f17 --- /dev/null +++ b/Foundation/IntProp/Kripke/Classical.lean @@ -0,0 +1,57 @@ +import Foundation.IntProp.Kripke.Semantics + +namespace LO.IntProp + + +namespace Kripke + +abbrev ClassicalValuation := ℕ → Prop + +end Kripke + + +namespace Formula.Kripke + +open IntProp.Kripke + +abbrev ClassicalSatisfies (V : ClassicalValuation) (φ : Formula ℕ) : Prop := Satisfies (⟨Kripke.pointFrame, ⟨λ _ => V, by tauto⟩⟩) () φ + +namespace ClassicalSatisfies + +instance : Semantics (Formula ℕ) (ClassicalValuation) := ⟨ClassicalSatisfies⟩ + +variable {V : ClassicalValuation} {a : ℕ} + +@[simp] lemma atom_def : V ⊧ atom a ↔ V a := by simp only [Semantics.Realize, Satisfies] + +instance : Semantics.Tarski (ClassicalValuation) where + realize_top := by simp [Semantics.Realize, ClassicalSatisfies, Satisfies]; + realize_bot := by simp [Semantics.Realize, ClassicalSatisfies, Satisfies]; + realize_or := by simp [Semantics.Realize, ClassicalSatisfies, Satisfies]; + realize_and := by simp [Semantics.Realize, ClassicalSatisfies, Satisfies]; + realize_imp := by simp [Semantics.Realize, Satisfies]; tauto; + realize_not := by simp [Semantics.Realize, Satisfies]; tauto; + +end ClassicalSatisfies + +end Formula.Kripke + + +open IntProp.Kripke +open Formula.Kripke (ClassicalSatisfies) + +namespace Hilbert.Cl + +lemma classical_sound : (Hilbert.Cl ℕ) ⊢! φ → (∀ V : ClassicalValuation, V ⊧ φ) := by + intro h V; + apply Hilbert.Cl.Kripke.sound.sound h Kripke.pointFrame; + simp [Euclidean]; + +lemma unprovable_of_exists_classicalValuation : (∃ V : ClassicalValuation, ¬(V ⊧ φ)) → (Hilbert.Cl ℕ) ⊬ φ := by + contrapose; + simp; + apply classical_sound; + +end Hilbert.Cl + +end LO.IntProp diff --git a/Foundation/IntProp/Kripke/Completeness.lean b/Foundation/IntProp/Kripke/Completeness.lean index 6c202f77..b84e47d2 100644 --- a/Foundation/IntProp/Kripke/Completeness.lean +++ b/Foundation/IntProp/Kripke/Completeness.lean @@ -2,48 +2,39 @@ import Foundation.IntProp.ConsistentTableau import Foundation.IntProp.Kripke.Semantics set_option autoImplicit false -universe u v +universe u namespace LO.IntProp +variable {H : Hilbert ℕ} +variable {t t₁ t₂ : SCT H} {φ ψ : Formula ℕ} + open System System.FiniteContext open Formula (atom) open Formula.Kripke (Satisfies ValidOnModel) open Kripke +open SaturatedConsistentTableau -namespace Kripke - -variable {α : Type u} - {H : Hilbert α} +namespace Hilbert -open SaturatedConsistentTableau +namespace Kripke -def CanonicalFrame (H : Hilbert α) [Nonempty (SCT H)] : Kripke.Frame.Dep α where +def canonicalFrameOf (H : Hilbert ℕ) [H.Consistent] [H.IncludeEFQ] : Kripke.Frame where World := SCT H Rel t₁ t₂ := t₁.tableau.1 ⊆ t₂.tableau.1 + rel_po := { + refl := by simp; + trans := fun x y z Sxy Syz => Set.Subset.trans Sxy Syz + antisymm := fun x y Sxy Syx => equality_of₁ (Set.Subset.antisymm Sxy Syx) + } -namespace CanonicalFrame +namespace canonicalFrame -variable [Nonempty (SCT H)] - -lemma reflexive : Reflexive (CanonicalFrame H) := by - simp [CanonicalFrame]; - intro x; - apply Set.Subset.refl; - -lemma antisymmetric : Antisymmetric (CanonicalFrame H) := by - simp [CanonicalFrame]; - intro x y Rxy Ryx; - exact equality_of₁ $ Set.Subset.antisymm Rxy Ryx; - -lemma transitive : Transitive (CanonicalFrame H) := by - simp [CanonicalFrame]; - intro x y z; - apply Set.Subset.trans; +variable {H : Hilbert ℕ} [H.IncludeEFQ] [H.Consistent] open Classical in -lemma confluent [Encodable α] [H.IncludeEFQ] [HasAxiomWeakLEM H] : Confluent (CanonicalFrame H) := by - simp [Confluent, CanonicalFrame]; +lemma is_confluent [HasAxiomWeakLEM H] : Confluent (Kripke.canonicalFrameOf H) := by + simp [Confluent, Kripke.canonicalFrameOf]; intro x y z Rxy Rxz; suffices Tableau.Consistent H (y.tableau.1 ∪ z.tableau.1, ∅) by obtain ⟨w, hw⟩ := lindenbaum (H := H) this; @@ -131,9 +122,8 @@ lemma confluent [Encodable α] [H.IncludeEFQ] [HasAxiomWeakLEM H] : Confluent (C exact mdp₁_mem mem_nnΘz_x $ mdp₁ mem_Θx_x d; - -lemma connected [DecidableEq α] [HasAxiomDummett H] : Connected (CanonicalFrame H) := by - simp [Connected, CanonicalFrame]; +lemma is_connected [HasAxiomDummett H] : Connected (Kripke.canonicalFrameOf H) := by + simp [Connected, Kripke.canonicalFrameOf]; intro x y z Rxy Ryz; apply or_iff_not_imp_left.mpr; intro nRyz; @@ -150,41 +140,39 @@ lemma connected [DecidableEq α] [HasAxiomDummett H] : Connected (CanonicalFrame have : ψ ∈ y.tableau.1 := mdp₁_mem hyp hpqy; exact this; -end CanonicalFrame - +end canonicalFrame -def CanonicalModel (H : Hilbert α) [Nonempty (SCT H)] : Kripke.Model α where - Frame := CanonicalFrame H - Valuation t a := (atom a) ∈ t.tableau.1 - -- hereditary := by aesop; -namespace CanonicalModel +def canonicalModelOf (H : Hilbert ℕ) [H.Consistent] [H.IncludeEFQ] : Kripke.Model where + toFrame := Kripke.canonicalFrameOf H + Val := ⟨λ t a => (atom a) ∈ t.tableau.1, by aesop⟩ -variable [Nonempty (SCT H)] {t t₁ t₂ : SCT H} +/- +namespace canonicalModelOf -lemma hereditary : (CanonicalModel H).Valuation.atomic_hereditary := by - intros _ _; - aesop; +variable [Nonempty (SCT H)] @[reducible] -instance : Semantics (Formula α) (CanonicalModel H).World := Formula.Kripke.Satisfies.semantics (CanonicalModel H) +instance : Semantics (Formula α) (Kripke.canonicalFrameOf H).World := Formula.Kripke.Satisfies.semantics $ Kripke.canonicalModelOf H -@[simp] lemma frame_def : (CanonicalModel H).Frame t₁ t₂ ↔ t₁.tableau.1 ⊆ t₂.tableau.1 := by rfl -@[simp] lemma valuation_def {a : α} : (CanonicalModel H).Valuation t a ↔ (atom a) ∈ t.tableau.1 := by rfl +@[simp] lemma frame_def : (Kripke.canonicalModelOf H).toFrame t₁ t₂ ↔ t₁.tableau.1 ⊆ t₂.tableau.1 := by rfl +@[simp] lemma valuation_def {a : α} : (Kripke.canonicalModelOf H).Valuation t a ↔ (atom a) ∈ t.tableau.1 := by rfl -end CanonicalModel +end canonicalModelOf +-/ -section +section lemmata -variable [Nonempty (SCT H)] +variable [H.IncludeEFQ] [H.Consistent] +variable {C : Kripke.FrameClass} + +section truthlemma -variable {t : SCT H} {φ ψ : Formula α} +variable {t : (Kripke.canonicalModelOf H).World} private lemma truthlemma.himp - [H.IncludeEFQ] [Encodable α] [DecidableEq α] - {t : (CanonicalModel H).World} - (ihp : ∀ {t : (CanonicalModel H).World}, t ⊧ φ ↔ φ ∈ t.tableau.1) - (ihq : ∀ {t : (CanonicalModel H).World}, t ⊧ ψ ↔ ψ ∈ t.tableau.1) + (ihp : ∀ {t : (Kripke.canonicalModelOf H).World}, t ⊧ φ ↔ φ ∈ t.tableau.1) + (ihq : ∀ {t : (Kripke.canonicalModelOf H).World}, t ⊧ ψ ↔ ψ ∈ t.tableau.1) : t ⊧ φ ➝ ψ ↔ φ ➝ ψ ∈ t.tableau.1 := by constructor; . contrapose; @@ -212,7 +200,7 @@ private lemma truthlemma.himp have ⟨_, _⟩ := Set.insert_subset_iff.mp h; use t'; constructor; - . simp_all only [Set.singleton_subset_iff]; + . assumption; . constructor; . assumption; . apply not_mem₁_iff_mem₂.mpr; @@ -234,9 +222,7 @@ private lemma truthlemma.himp ); private lemma truthlemma.hneg - [H.IncludeEFQ] [Encodable α] [DecidableEq α] - {t : (CanonicalModel H).World} - (ihp : ∀ {t : (CanonicalModel H).World}, t ⊧ φ ↔ φ ∈ t.tableau.1) + (ihp : ∀ {t : (Kripke.canonicalModelOf H).World}, t ⊧ φ ↔ φ ∈ t.tableau.1) : t ⊧ ∼φ ↔ ∼φ ∈ t.tableau.1 := by constructor; . contrapose; @@ -258,6 +244,7 @@ private lemma truthlemma.hneg contradiction; have ⟨_, _⟩ := Set.insert_subset_iff.mp h; use t'; + constructor <;> assumption; . simp; intro ht t' htt'; apply ihp.not.mpr; @@ -266,17 +253,16 @@ private lemma truthlemma.hneg have : H ⊢! φ ⋏ ∼φ ➝ ⊥ := intro_bot_of_and!; contradiction; -lemma truthlemma - [H.IncludeEFQ] [Encodable α] [DecidableEq α] - {t : (CanonicalModel H).World} : t ⊧ φ ↔ φ ∈ t.tableau.1 := by +lemma truthlemma : t ⊧ φ ↔ φ ∈ t.tableau.1 := by induction φ using Formula.rec' generalizing t with + | hatom => tauto; | himp φ ψ ihp ihq => exact truthlemma.himp ihp ihq | hneg φ ihp => exact truthlemma.hneg ihp; | _ => simp [Satisfies.iff_models, Satisfies, *]; -lemma deducible_of_validOnCanonicelModel - [H.IncludeEFQ] [Encodable α] [DecidableEq α] - : (CanonicalModel H) ⊧ φ ↔ H ⊢! φ := by +end truthlemma + +lemma deducible_of_validOnCanonicelModel : (Kripke.canonicalModelOf H) ⊧ φ ↔ H ⊢! φ := by constructor; . contrapose; intro h; @@ -298,48 +284,29 @@ lemma deducible_of_validOnCanonicelModel suffices φ ∈ t.tableau.1 by exact truthlemma.mpr this; exact mem₁_of_provable h; - -section - -variable [System.Consistent H] -variable [DecidableEq α] [Encodable α] [H.IncludeEFQ] -variable {𝔽 : Kripke.FrameClass} - -omit [Consistent H] in -lemma complete (hC : CanonicalFrame H ∈ 𝔽) {φ : Formula α} : 𝔽#α ⊧ φ → H ⊢! φ := by +lemma complete_of_canonical (hC : (Kripke.canonicalFrameOf H) ∈ C) : C ⊧ φ → H ⊢! φ := by intro h; apply deducible_of_validOnCanonicelModel.mp; apply h; - . exact hC; - . exact CanonicalModel.hereditary; + exact hC; -instance instComplete (hC : CanonicalFrame H ∈ 𝔽) : Complete H (𝔽#α) := ⟨complete hC⟩ +instance instCompleteOfCanonical (hC : (Kripke.canonicalFrameOf H) ∈ C) : Complete H C := ⟨complete_of_canonical hC⟩ -instance Int_complete : Complete (Hilbert.Int α) (Kripke.ReflexiveTransitiveFrameClass.{u}#α) := instComplete $ by - refine ⟨ - CanonicalFrame.reflexive, - CanonicalFrame.transitive, - ⟩ +end lemmata -instance LC_complete : Complete (Hilbert.LC α) (Kripke.ReflexiveTransitiveConnectedFrameClass.{u}#α) := instComplete $ by - refine ⟨ - CanonicalFrame.reflexive, - CanonicalFrame.transitive, - CanonicalFrame.connected - ⟩; +end Kripke -instance KC_complete : Complete (Hilbert.KC α) (Kripke.ReflexiveTransitiveConfluentFrameClass.{u}#α) := instComplete $ by - refine ⟨ - CanonicalFrame.reflexive, - CanonicalFrame.transitive, - CanonicalFrame.confluent - ⟩; -end +section completeness +instance Int.Kripke.complete : Complete (Hilbert.Int ℕ) AllFrameClass := Hilbert.Kripke.instCompleteOfCanonical $ by tauto -end +instance KC.Kripke.complete : Complete (Hilbert.KC ℕ) ConfluentFrameClass := Hilbert.Kripke.instCompleteOfCanonical $ Kripke.canonicalFrame.is_confluent -end Kripke +instance LC.Kripke.complete : Complete (Hilbert.LC ℕ) ConnectedFrameClass := Hilbert.Kripke.instCompleteOfCanonical $ Kripke.canonicalFrame.is_connected + +end completeness + +end Hilbert end LO.IntProp diff --git a/Foundation/IntProp/Kripke/DP.lean b/Foundation/IntProp/Kripke/DP.lean index 5fa284d1..958ff13e 100644 --- a/Foundation/IntProp/Kripke/DP.lean +++ b/Foundation/IntProp/Kripke/DP.lean @@ -8,10 +8,9 @@ open Formula Formula.Kripke namespace Kripke -variable {α} -variable {φ ψ : Formula α} +variable {φ ψ : Formula ℕ} -abbrev IntDPCounterexampleFrame (F₁ : Kripke.Frame) (F₂ : Kripke.Frame) (w₁ : F₁.World) (w₂ : F₂.World) : Kripke.Frame where +abbrev counterexampleDPFrame (F₁ : Kripke.Frame) (F₂ : Kripke.Frame) (w₁ : F₁.World) (w₂ : F₂.World) : Kripke.Frame where World := Unit ⊕ F₁.World ⊕ F₂.World; Rel x y := match x, y with @@ -21,127 +20,101 @@ abbrev IntDPCounterexampleFrame (F₁ : Kripke.Frame) (F₂ : Kripke.Frame) (w | (Sum.inr $ Sum.inl x), (Sum.inr $ Sum.inl y) => F₁.Rel x y | (Sum.inr $ Sum.inr x), (Sum.inr $ Sum.inr y) => F₂.Rel x y | _, _ => False - -lemma IntDPCounterexampleFrame.reflexive - {F₁ : Kripke.Frame} {F₂ : Kripke.Frame} - {w₁ : F₁.World} {w₂ : F₂.World} - (F₁_refl : Reflexive F₁.Rel) (F₂_refl : Reflexive F₂.Rel) - : Reflexive (IntDPCounterexampleFrame F₁ F₂ w₁ w₂).Rel := by - simp only [Reflexive, Sum.forall, forall_const, true_and]; - constructor; - . exact F₁_refl; - . exact F₂_refl; - -lemma IntDPCounterexampleFrame.transitive - {F₁ : Kripke.Frame} {F₂ : Kripke.Frame} - {w₁ : F₁.World} {w₂ : F₂.World} - (F₁_trans : Transitive F₁.Rel) (F₂_trans : Transitive F₂.Rel) - : Transitive (IntDPCounterexampleFrame F₁ F₂ w₁ w₂).Rel := by - simp only [Transitive, Sum.forall, forall_true_left, imp_self, forall_const, true_and, IsEmpty.forall_iff, implies_true, and_true, and_self, imp_false]; - constructor; - . constructor; - . intro _ _; apply F₁_trans; - . intro _ _; apply F₂_trans; - . constructor; - . intro _ _; apply F₁_trans; - . intro _ _; apply F₂_trans; - -lemma IntDPCounterexampleFrame.antisymmetric - {F₁ : Kripke.Frame} {F₂ : Kripke.Frame} - {w₁ : F₁.World} {w₂ : F₂.World} - (F₁_antisymm : Antisymmetric F₁.Rel) (F₂_antisymm : Antisymmetric F₂.Rel) - : Antisymmetric (IntDPCounterexampleFrame F₁ F₂ w₁ w₂).Rel := by - simp only [Antisymmetric, Sum.forall, forall_true_left, forall_const, IsEmpty.forall_iff, implies_true, and_self, imp_false, Sum.inr.injEq, true_and, Sum.inl.injEq, and_true]; - constructor; - . exact F₁_antisymm; - . exact F₂_antisymm; - -abbrev IntDPCounterexampleModel (M₁ : Kripke.Model α) (M₂ : Kripke.Model α) (w₁ : M₁.World) (w₂ : M₂.World) : Kripke.Model α where - Frame := IntDPCounterexampleFrame M₁.Frame M₂.Frame w₁ w₂; - Valuation w a := - match w with - | Sum.inr $ Sum.inl w => M₁.Valuation w a - | Sum.inr $ Sum.inr w => M₂.Valuation w a - | _ => False - -lemma IntDPCounterexampleModel.atomic_hereditary - {M₁ : Kripke.Model α} {M₂ : Kripke.Model α} - {w₁ : M₁.World} {w₂ : M₂.World} - (M₁_hered : M₁.Valuation.atomic_hereditary) (M₂_hered : M₂.Valuation.atomic_hereditary) - : (IntDPCounterexampleModel M₁ M₂ w₁ w₂).Valuation.atomic_hereditary := by - simp; - constructor; - . apply M₁_hered; - . apply M₂_hered; - -variable {M₁ : Kripke.Model α} {M₂ : Kripke.Model α} - -lemma satisfies_left_on_IntDPCounterexampleModel : - (Satisfies M₁ w φ) ↔ (Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr $ Sum.inl w) φ) := by + rel_po := { + refl := by simp only [Sum.forall, implies_true, Frame.rel_refl, and_self]; + trans := by + simp only [Sum.forall, true_implies, imp_self, implies_true, true_and, false_implies, and_true, and_self, forall_const, imp_false]; + constructor; + . constructor; + . intro _ _; apply F₁.rel_trans; + . intro _ _; apply F₂.rel_trans; + . constructor; + . intro _ _ _; apply F₁.rel_trans; + . intro _ _ _; apply F₂.rel_trans; + antisymm := by + simp only [Sum.forall, imp_self, implies_true, reduceCtorEq, and_self, imp_false, false_implies, Sum.inr.injEq, true_and, Sum.inl.injEq, and_true]; + constructor; + . intro _ _; apply F₁.rel_antisymm; + . intro _ _; apply F₂.rel_antisymm; + } + +abbrev counterexampleDPModel (M₁ : Kripke.Model) (M₂ : Kripke.Model) (w₁ : M₁.World) (w₂ : M₂.World) : Model where + toFrame := counterexampleDPFrame M₁.toFrame M₂.toFrame w₁ w₂; + Val := ⟨ + λ w a => + match w with + | Sum.inr $ Sum.inl w => M₁ w a + | Sum.inr $ Sum.inr w => M₂ w a + | _ => False, + by + simp only [Sum.forall, imp_false, not_false_eq_true, implies_true, imp_self, false_implies, and_self, and_true, true_and]; + constructor; + . intro _ _; apply M₁.Val.hereditary; + . intro _ _; apply M₂.Val.hereditary; + ⟩ + +variable {M₁ : Kripke.Model} {M₂ : Kripke.Model} + +lemma satisfies_left_on_counterexampleDPModel : + w ⊧ φ ↔ (Satisfies (counterexampleDPModel M₁ M₂ w₁ w₂) (Sum.inr $ Sum.inl w) φ) := by induction φ using rec' generalizing w with | himp φ ψ ihp ihq => constructor; . intro hpq X hWX hp; - obtain ⟨x, hx, ex⟩ : ∃ x, (M₁.Frame.Rel w x) ∧ (Sum.inr $ Sum.inl x) = X := by - replace hWX : (IntDPCounterexampleModel M₁ M₂ w₁ w₂).Frame.Rel _ X := hWX; - simp [IntDPCounterexampleFrame] at hWX; + obtain ⟨x, hx, ex⟩ : ∃ x, (M₁.Rel w x) ∧ (Sum.inr $ Sum.inl x) = X := by + replace hWX : (counterexampleDPModel M₁ M₂ w₁ w₂).Rel _ X := hWX; + simp [counterexampleDPModel] at hWX; split at hWX; all_goals simp_all; subst ex; exact ihq.mp $ hpq hx $ ihp.mpr hp; . intro h v Rwv hp; apply @ihq v |>.mpr $ h (by simpa) $ ihp.mp hp; - | _ => simp_all [IntDPCounterexampleModel, Satisfies.iff_models, Satisfies]; + | _ => simp_all [counterexampleDPModel, Satisfies.iff_models, Satisfies]; -lemma satisfies_right_on_IntDPCounterexampleModel : - (Satisfies M₂ w φ) ↔ (Satisfies (IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr $ Sum.inr w) φ) := by +lemma satisfies_right_on_counterexampleDPModel : + w ⊧ φ ↔ (Satisfies (counterexampleDPModel M₁ M₂ w₁ w₂) (Sum.inr $ Sum.inr w) φ) := by induction φ using rec' generalizing w with | himp φ ψ ihp ihq => constructor; . intro h X hWX hp; - obtain ⟨x, hx, ex⟩ : ∃ x, (M₂.Frame.Rel w x) ∧ (Sum.inr $ Sum.inr x) = X := by - replace hWX : (IntDPCounterexampleModel M₁ M₂ w₁ w₂).Frame.Rel _ X := hWX; - simp [IntDPCounterexampleFrame] at hWX; + obtain ⟨x, hx, ex⟩ : ∃ x, (M₂.Rel w x) ∧ (Sum.inr $ Sum.inr x) = X := by + replace hWX : (counterexampleDPModel M₁ M₂ w₁ w₂).Rel _ X := hWX; + simp [counterexampleDPModel] at hWX; split at hWX; all_goals simp_all; subst ex; exact ihq.mp $ h hx $ ihp.mpr hp; . intro h v Rwv hp; exact ihq.mpr $ h (by simpa) $ ihp.mp hp; - | _ => simp_all [IntDPCounterexampleModel, Satisfies.iff_models, Satisfies]; + | _ => simp_all [counterexampleDPModel, Satisfies.iff_models, Satisfies]; + +end Kripke + +namespace Hilbert.Int -theorem disjunctive_int [Inhabited α] [DecidableEq α] [Encodable α] : (Hilbert.Int α) ⊢! φ ⋎ ψ → (Hilbert.Int α) ⊢! φ ∨ (Hilbert.Int α) ⊢! ψ := by +theorem disjunctive : (Hilbert.Int ℕ) ⊢! φ ⋎ ψ → (Hilbert.Int ℕ) ⊢! φ ∨ (Hilbert.Int ℕ) ⊢! ψ := by contrapose; intro hC; push_neg at hC; - have ⟨hnp, hnq⟩ := hC; - obtain ⟨Fp, Fp_refl, Fp_trans, Vp, Vp_hered, wp, hp⟩ := by simpa [Semantics.Realize, ValidOnFrame, ValidOnModel] using not_imp_not.mpr Int_complete.complete hnp; - obtain ⟨Fq, Fq_refl, Fq_trans, Vq, Vq_hered, wq, hq⟩ := by simpa [Semantics.Realize, ValidOnFrame, ValidOnModel] using not_imp_not.mpr Int_complete.complete hnq; - apply (not_imp_not.mpr Int_sound.sound); - simp [Semantics.Realize, ValidOnFrame, ValidOnModel, Satisfies]; - use (IntDPCounterexampleFrame Fp Fq wp wq); - refine ⟨IntDPCounterexampleFrame.reflexive Fp_refl Fq_refl, IntDPCounterexampleFrame.transitive Fp_trans Fq_trans, ?_⟩; - use (IntDPCounterexampleModel ⟨Fp, Vp⟩ ⟨Fq, Vq⟩ wp wq).Valuation; + have ⟨hnφ, hnψ⟩ := hC; + obtain ⟨F₁, V₁, w₁, hφ⟩ := by simpa [ValidOnFrame, ValidOnModel] using not_imp_not.mpr Int.Kripke.complete.complete hnφ; + obtain ⟨F₂, V₂, w₂, hψ⟩ := by simpa [ValidOnFrame, ValidOnModel] using not_imp_not.mpr Int.Kripke.complete.complete hnψ; + apply (not_imp_not.mpr Int.Kripke.sound.sound); + simp [ValidOnFrame, ValidOnModel]; + let M := Kripke.counterexampleDPModel ⟨F₁, V₁⟩ ⟨F₂, V₂⟩ w₁ w₂; + use M.toFrame, M.Val, (Sum.inl ()); + apply Formula.Kripke.Satisfies.or_def.not.mpr; + push_neg; constructor; - . exact IntDPCounterexampleModel.atomic_hereditary (M₁ := ⟨Fp, Vp⟩) (M₂ := ⟨Fq, Vq⟩) Vp_hered Vq_hered; - . use (Sum.inl ()); - constructor; - . exact not_imp_not.mpr - (Satisfies.formula_hereditary - (M := IntDPCounterexampleModel ⟨Fp, Vp⟩ ⟨Fq, Vq⟩ wp wq) - (IntDPCounterexampleModel.atomic_hereditary Vp_hered Vq_hered) - (IntDPCounterexampleFrame.transitive Fp_trans Fq_trans) - (w := Sum.inl ()) (w' := Sum.inr $ Sum.inl wp) (by aesop)) - $ satisfies_left_on_IntDPCounterexampleModel |>.not.mp hp; - . exact not_imp_not.mpr - (Satisfies.formula_hereditary - (M := IntDPCounterexampleModel ⟨Fp, Vp⟩ ⟨Fq, Vq⟩ wp wq) - (IntDPCounterexampleModel.atomic_hereditary Vp_hered Vq_hered) - (IntDPCounterexampleFrame.transitive Fp_trans Fq_trans) - (w := Sum.inl ()) (w' := Sum.inr $ Sum.inr wq) (by aesop)) - $ satisfies_right_on_IntDPCounterexampleModel |>.not.mp hq; + . have := not_imp_not.mpr $ @Satisfies.formula_hereditary (M := M) (w := Sum.inl ()) (w' := Sum.inr $ Sum.inl w₁) φ (by simp); + apply this; + exact Kripke.satisfies_left_on_counterexampleDPModel.not.mp hφ; + . have := not_imp_not.mpr $ @Satisfies.formula_hereditary (M := M) (w := Sum.inl ()) (w' := Sum.inr $ Sum.inr w₂) ψ (by simp); + apply this; + exact Kripke.satisfies_right_on_counterexampleDPModel.not.mp hψ; -instance [DecidableEq α] [Inhabited α] [Encodable α] : Disjunctive (Hilbert.Int α) := ⟨disjunctive_int⟩ +instance : Disjunctive (Hilbert.Int ℕ) := ⟨disjunctive⟩ -end Kripke +end Hilbert.Int end LO.IntProp diff --git a/Foundation/IntProp/Kripke/Kripke.lean b/Foundation/IntProp/Kripke/Kripke.lean index 99c5e9af..e06f5837 100644 --- a/Foundation/IntProp/Kripke/Kripke.lean +++ b/Foundation/IntProp/Kripke/Kripke.lean @@ -1,3 +1,6 @@ import Foundation.IntProp.Kripke.Completeness import Foundation.IntProp.Kripke.DP -import Foundation.IntProp.Kripke.LEM + +-- import Foundation.IntProp.Kripke.LEM + +import Foundation.IntProp.Kripke.Classical diff --git a/Foundation/IntProp/Kripke/LEM.lean b/Foundation/IntProp/Kripke/LEM.lean index f75fd787..71c8da08 100644 --- a/Foundation/IntProp/Kripke/LEM.lean +++ b/Foundation/IntProp/Kripke/LEM.lean @@ -1,150 +1,202 @@ import Foundation.IntProp.Kripke.Semantics -/-! - # Counterexample to the Law of Excluded Middle in Intuitionistic Logic - - ## Theorems - - `noLEM`: LEM is not always valid in intuitionistic logic. --/ +-- TODO: prove `Formula.Kripke.ValidOnFrame.subst` namespace LO.IntProp open System open Formula Formula.Kripke - -variable {α : Type u} - -abbrev NoLEMFrame : Kripke.Frame where - World := PUnit ⊕ PUnit - Rel x y := - match x, y with - | .inl _, .inl _ => True - | .inr _, .inr _ => True - | .inl _, .inr _ => True - | _, _ => False - -namespace NoLEMFrame - -lemma is_transitive : Transitive NoLEMFrame.Rel := by simp [Transitive]; - -lemma is_reflexive : Reflexive NoLEMFrame.Rel := by simp [Reflexive]; - -lemma is_confluent : Confluent NoLEMFrame.Rel := by simp [Confluent]; - -lemma is_connected : Connected NoLEMFrame.Rel := by simp [Connected]; - -end NoLEMFrame - - -lemma Kripke.noLEM_on_frameclass [Inhabited α] : ∃ (φ : Formula α), ¬((Kripke.FrameClassOfHilbert.{u, 0} (Hilbert.Int α)) ⊧ φ ⋎ ∼φ) := by - use (atom default); - simp [Semantics.Realize]; - use NoLEMFrame; - constructor; - . apply Int_Characteraizable.characterize; - exact ⟨NoLEMFrame.is_reflexive, NoLEMFrame.is_transitive⟩; - . simp [ValidOnFrame]; - use (λ w _ => match w with | .inr _ => True | .inl _ => False); +-- TODO: 成り立つのか？ +lemma Formula.Kripke.ValidOnFrame.subst {F : Kripke.Frame} {φ : Formula ℕ} (h : F ⊧ φ) (s : ℕ → Formula ℕ) : F ⊧ φ.subst s := by sorry; + /- + induction φ using Formula.rec' with + | hatom => + intro V x; + refine h (V := ⟨λ x a => Satisfies ⟨F, V⟩ x (s a), ?_⟩) x; + intro x y Rxy a; + exact formula_hereditary Rxy; + | hverum => simp; + | hfalsum => simp at h; + | hand _ _ hφ hψ => + intro V x; + apply Satisfies.and_def.mp; constructor; - . simp; - . simp [ValidOnModel, Satisfies]; - - -/-- - Law of Excluded Middle is not always provable in intuitionistic logic. --/ -theorem Hilbert.Int.noLEM [Inhabited α] : ∃ (φ : Formula α), (Hilbert.Int α) ⊬ φ ⋎ ∼φ := by - obtain ⟨φ, hp⟩ := Kripke.noLEM_on_frameclass (α := α); - use φ; - by_contra hC; - have := @Kripke.sound _ _ _ hC; + . apply hφ; + intro V x; + exact h x |>.1; + . apply hψ; + intro V x; + exact h x |>.2; + | himp φ ψ hφ hψ => + apply Satisfies.imp_def.mp; + intro y Rxy hy; + apply hψ; + intro V' z; + have := @h V x; + have := @Satisfies.imp_def ⟨F, V⟩ x φ ψ |>.mp this Rxy; + apply h; + . sorry; + . sorry; + sorry; + | hor φ ψ hφ hψ => + intro V x; + rcases Satisfies.or_def.mp $ h x with (hl | hr); + . left; + apply hφ; + intro V' y; + sorry; + . sorry; + | hneg φ hφ => + intro V x; + apply Satisfies.neg_def.mpr; + intro y Rxy hyφ; + have := @h V y; + apply hφ; + -/ + +namespace Hilbert + +open Kripke + +variable {a b : ℕ} + +theorem Int.no_WeakLEM : ∃ a, (Hilbert.Int ℕ) ⊬ Axioms.WeakLEM (atom a) := by + by_contra hC; simp at hC; + let F : Kripke.Frame := { + World := Fin 3 + Rel := λ x y => + match x, y with + | 0, _ => True + | x, y => x = y + rel_po := { + refl := by aesop; + antisymm := by aesop; + trans := by aesop; + } + } + have : Confluent F := by + apply @Kripke.ConfluentFrameClass.defined_by_WLEM F |>.mpr; + simp [Semantics.RealizeSet.setOf_iff, ValidOnFrame.models_iff]; + intro φ; + suffices ValidOnFrame F (Axioms.WeakLEM (atom 0)) + from @Formula.Kripke.ValidOnFrame.subst F (Axioms.WeakLEM (atom 0)) this (λ a => match a with | 0 => φ | _ => atom a); + apply (Hilbert.Int.Kripke.sound.sound $ hC 0) F; + tauto; + have : ¬Confluent F := by + simp only [Confluent]; push_neg; + use 0, 1, 2; + simp; contradiction; -/-- - Intuitionistic logic is proper weaker than classical logic. --/ -theorem Hilbert.Int_strictly_weaker_than_Cl [DecidableEq α] [Inhabited α] : (Hilbert.Int α) <ₛ (Hilbert.Cl α) := by +theorem Int_strictly_weaker_than_LC : (Hilbert.Int ℕ) <ₛ (Hilbert.KC ℕ) := by constructor; - . exact Hilbert.Int_weaker_than_Cl; - . apply weakerThan_iff.not.mpr; + . exact Hilbert.Int_weaker_than_KC; + . obtain ⟨a, h⟩ := Int.no_WeakLEM; + apply weakerThan_iff.not.mpr; push_neg; - obtain ⟨φ, hp⟩ := Hilbert.Int.noLEM (α := α); - use (φ ⋎ ∼φ); - constructor; - . exact lem!; - . assumption; - - -section - -lemma Kripke.noLEM_on_frameclass_KC [DecidableEq α] [Inhabited α] : ∃ (φ : Formula α), ¬((Kripke.FrameClassOfHilbert.{u, 0} (Hilbert.KC α)) ⊧ φ ⋎ ∼φ) := by - use (atom default); - simp [Semantics.Realize]; - use NoLEMFrame; - constructor; - . apply Kripke.KC_Characteraizable.characterize; - exact ⟨NoLEMFrame.is_reflexive, NoLEMFrame.is_transitive, NoLEMFrame.is_confluent⟩; - . simp [ValidOnFrame]; - use (λ w _ => match w with | .inr _ => True | .inl _ => False); + use ∼(atom a) ⋎ ∼∼(atom a); constructor; - . simp; - . simp [ValidOnModel, Satisfies]; - -lemma Hilbert.KC.noLEM [DecidableEq α] [Inhabited α] : ∃ (φ : Formula α), (Hilbert.KC α) ⊬ φ ⋎ ∼φ := by - obtain ⟨φ, hp⟩ := Kripke.noLEM_on_frameclass_KC (α := α); - use φ; - by_contra hC; - have := @Kripke.sound _ _ _ hC; + . exact wlem!; + . exact h; + +theorem KC.no_Dummett : ∃ a b, (Hilbert.KC ℕ) ⊬ Axioms.Dummett (atom a) (atom b) := by + by_contra hC; simp at hC; + let F : Kripke.Frame := { + World := Fin 4 + Rel := λ x y => + match x, y with + | 1, 2 => False + | x, y => x ≤ y + rel_po := { + refl := by simp only [le_refl, implies_true]; + trans := by + intro x y z Rxy Ryx; + split at Rxy; + . contradiction; + . split at Ryx; + . contradiction; + . split; + . simp_all; omega; + . omega; + antisymm := by + intro x y Rxy Ryx; + split at Rxy; + . contradiction; + . split at Ryx; + . contradiction; + . exact LE.le.antisymm Rxy Ryx; + } + }; + have : Connected F := by + apply @Kripke.ConnectedFrameClass.defined_by_Dummett F |>.mpr; + simp [Semantics.RealizeSet.setOf_iff, ValidOnFrame.models_iff]; + rintro _ φ ψ rfl; + suffices ValidOnFrame F (Axioms.Dummett (atom 0) (atom 1)) + from @Formula.Kripke.ValidOnFrame.subst F (Axioms.Dummett (atom 0) (atom 1)) this (λ a => match a with | 0 => φ | 1 => ψ | _ => atom a); + apply (Hilbert.KC.Kripke.sound.sound $ hC 0 1) F; + simp [Confluent]; + intro x y z Rxy Ryz; + use 3; + split at Rxy; + . contradiction; + . split at Ryz; + . contradiction; + . constructor; + . simp_all; omega; + . simp_all; omega; + have : ¬Connected F := by + simp only [Connected]; push_neg; + use 0, 1, 2; + simp; contradiction; -theorem Hilbert.KC_strictly_weaker_than_Cl [DecidableEq α] [Inhabited α] : (Hilbert.KC α) <ₛ (Hilbert.Cl α) := by +theorem KC_strictly_weaker_than_LC : (Hilbert.KC ℕ) <ₛ (Hilbert.LC ℕ) := by constructor; - . exact Hilbert.KC_weaker_than_Cl; - . apply weakerThan_iff.not.mpr; + . exact Hilbert.KC_weaker_than_LC; + . obtain ⟨a, b, h⟩ := KC.no_Dummett; + apply weakerThan_iff.not.mpr; push_neg; - obtain ⟨φ, hp⟩ := Hilbert.KC.noLEM (α := α); - use (φ ⋎ ∼φ); + use Axioms.Dummett (atom a) (atom b); constructor; - . exact lem!; - . assumption; - -end - - -section - -lemma Kripke.noLEM_on_frameclass_LC [Inhabited α] : ∃ (φ : Formula α), ¬((Kripke.FrameClassOfHilbert.{u, 0} (Hilbert.LC α)) ⊧ φ ⋎ ∼φ) := by - use (atom default); - simp [Semantics.Realize]; - use NoLEMFrame; - constructor; - . apply LC_Characteraizable.characterize; - exact ⟨NoLEMFrame.is_reflexive, NoLEMFrame.is_transitive, NoLEMFrame.is_connected⟩; - . simp [ValidOnFrame]; - use (λ w _ => match w with | .inr _ => True | .inl _ => False); - constructor; - . simp; - . simp [ValidOnModel, Satisfies]; - -lemma Hilbert.LC.noLEM [Inhabited α] : ∃ (φ : Formula α), (Hilbert.LC α) ⊬ φ ⋎ ∼φ := by - obtain ⟨φ, hp⟩ := Kripke.noLEM_on_frameclass_LC (α := α); - use φ; - by_contra hC; - have := @Kripke.sound _ _ _ hC; + . exact dummett!; + . exact h; + +theorem LC.no_LEM : ∃ a, (Hilbert.LC ℕ) ⊬ Axioms.LEM (atom a) := by + by_contra hC; simp at hC; + let F : Kripke.Frame := { + World := Fin 2 + Rel := λ x y => x ≤ y + }; + have : Euclidean F := by + apply @Kripke.EuclideanFrameClass.defined_by_LEM F |>.mpr; + simp [Semantics.RealizeSet.setOf_iff, ValidOnFrame.models_iff]; + intro φ; + suffices ValidOnFrame F (Axioms.LEM (atom 0)) + from @Formula.Kripke.ValidOnFrame.subst F (Axioms.LEM (atom 0)) this (λ a => match a with | 0 => φ | _ => atom a); + apply (Hilbert.LC.Kripke.sound.sound $ hC 0) F; + simp [Connected]; + omega; + have : ¬Euclidean F := by + simp only [Euclidean]; push_neg; + use 0, 0, 1; + simp; contradiction; -theorem Hilbert.LC_strictly_weaker_than_Cl [DecidableEq α] [Inhabited α] : (Hilbert.LC α) <ₛ (Hilbert.Cl α) := by +theorem LC_strictly_weaker_than_Cl : (Hilbert.LC ℕ) <ₛ (Hilbert.Cl ℕ) := by constructor; . exact Hilbert.LC_weaker_than_Cl; - . apply weakerThan_iff.not.mpr; + . obtain ⟨a, h⟩ := LC.no_LEM; + apply weakerThan_iff.not.mpr; push_neg; - obtain ⟨φ, hp⟩ := Hilbert.LC.noLEM (α := α); - use (φ ⋎ ∼φ); + use Axioms.LEM (atom a); constructor; . exact lem!; - . assumption; + . exact h; + +theorem Int_strictly_weaker_than_Cl : (Hilbert.Int ℕ) <ₛ (Hilbert.Cl ℕ) := + strictlyWeakerThan.trans Int_strictly_weaker_than_LC $ strictlyWeakerThan.trans KC_strictly_weaker_than_LC LC_strictly_weaker_than_Cl -end +end Hilbert end LO.IntProp diff --git a/Foundation/IntProp/Kripke/Semantics.lean b/Foundation/IntProp/Kripke/Semantics.lean index 6090fbd1..2e7000aa 100644 --- a/Foundation/IntProp/Kripke/Semantics.lean +++ b/Foundation/IntProp/Kripke/Semantics.lean @@ -1,17 +1,88 @@ -import Foundation.Logic.Kripke.Basic +import Foundation.Vorspiel.BinaryRelations import Foundation.IntProp.Deduction +set_option autoImplicit false +universe u v + namespace LO.IntProp open System + + +namespace Kripke + +structure Frame where + World : Type + Rel : Rel World World + [world_nonempty : Nonempty World] + [rel_po : IsPartialOrder _ Rel] + +instance : CoeSort Frame (Type) := ⟨Frame.World⟩ +instance : CoeFun Frame (λ F => F.World → F.World → Prop) := ⟨Frame.Rel⟩ +instance {F : Frame} : Nonempty F.World := F.world_nonempty +instance {F : Frame} : IsPartialOrder _ F.Rel := F.rel_po + +abbrev Frame.Rel' {F : Frame} (x y : F.World) := F.Rel x y +infix:45 " ≺ " => Frame.Rel' + +namespace Frame + +variable {F : Frame} + +@[trans] lemma rel_trans {x y z : F.World} : x ≺ y → y ≺ z → x ≺ z := IsTrans.trans x y z +lemma rel_trans' : Transitive F.Rel := by apply rel_trans; + +@[refl, simp] lemma rel_refl {x : F.World} : x ≺ x := IsRefl.refl x +lemma rel_refl' : Reflexive F.Rel := by apply rel_refl + +@[simp] lemma rel_antisymm {x y : F.World} : x ≺ y → y ≺ x → x = y := IsAntisymm.antisymm x y +lemma rel_antisymm' : Antisymmetric F.Rel := by apply rel_antisymm + +end Frame + +abbrev pointFrame : Frame where + World := Unit + Rel := fun _ _ => True + + +abbrev FrameClass := Set (Frame) + +section + +abbrev AllFrameClass : FrameClass := Set.univ + +abbrev SymmetricFrameClass : FrameClass := { F : Kripke.Frame | Symmetric F } + +abbrev ConfluentFrameClass : FrameClass := { F : Kripke.Frame | Confluent F } + +abbrev ConnectedFrameClass : FrameClass := { F : Kripke.Frame | Connected F } + +abbrev EuclideanFrameClass : FrameClass := { F : Kripke.Frame | Euclidean F } + +end + + +structure Valuation (F : Frame) where + Val : F.World → ℕ → Prop + hereditary : ∀ {w₁ w₂ : F.World}, (w₁ ≺ w₂) → ∀ {a}, (Val w₁ a) → (Val w₂ a) +instance {F : Frame} : CoeFun (Valuation F) (λ _ => F.World → ℕ → Prop) := ⟨Valuation.Val⟩ + +structure Model extends Frame where + Val : Valuation toFrame +instance : CoeFun (Model) (λ M => M.World → ℕ → Prop) := ⟨fun m => m.Val⟩ + +end Kripke + + open Kripke -variable {α : Type u} + +open Formula namespace Formula.Kripke -def Satisfies (M : Kripke.Model.{u, v} α) (w : M.World) : Formula α → Prop - | atom a => M.Valuation w a +def Satisfies (M : Kripke.Model) (w : M.World) : Formula ℕ → Prop + | atom a => M w a | ⊤ => True | ⊥ => False | φ ⋏ ψ => Satisfies M w φ ∧ Satisfies M w ψ @@ -21,13 +92,13 @@ def Satisfies (M : Kripke.Model.{u, v} α) (w : M.World) : Formula α → Prop namespace Satisfies -instance semantics (M : Kripke.Model.{u, v} α) : Semantics (Formula α) (M.World) := ⟨fun w ↦ Formula.Kripke.Satisfies M w⟩ +instance semantics (M : Kripke.Model) : Semantics (Formula ℕ) (M.World) := ⟨fun w ↦ Formula.Kripke.Satisfies M w⟩ -variable {M : Model α} {w : M.World} {φ ψ χ : Formula α} +variable {M : Kripke.Model} {w w' : M.World} {a : ℕ} {φ ψ χ : Formula ℕ} @[simp] protected lemma iff_models : w ⊧ φ ↔ Formula.Kripke.Satisfies M w φ := iff_of_eq rfl -@[simp] lemma atom_def : w ⊧ atom a ↔ M.Valuation w a := by simp [Satisfies]; +@[simp] lemma atom_def : w ⊧ atom a ↔ M w a := by simp [Satisfies]; @[simp] lemma top_def : w ⊧ ⊤ ↔ True := by simp [Satisfies]; @[simp] lemma bot_def : w ⊧ ⊥ ↔ False := by simp [Satisfies]; @[simp] lemma and_def : w ⊧ φ ⋏ ψ ↔ w ⊧ φ ∧ w ⊧ ψ := by simp [Satisfies]; @@ -48,85 +119,77 @@ instance : Semantics.Or M.World where realize_or := by simp [Satisfies]; lemma formula_hereditary - (herditary : M.Valuation.atomic_hereditary) - (F_trans : Transitive M.Frame.Rel) (hw : w ≺ w') : w ⊧ φ → w' ⊧ φ := by induction φ using Formula.rec' with - | hatom => apply herditary hw; + | hatom => apply M.Val.hereditary hw; | himp => intro hpq v hv; - exact hpq $ F_trans hw hv; + exact hpq $ M.rel_trans hw hv; | hneg => intro hp v hv; - exact hp $ F_trans hw hv; + exact hp $ M.rel_trans hw hv; | hor => simp_all [Satisfies]; tauto; | _ => simp_all [Satisfies]; lemma neg_equiv : w ⊧ ∼φ ↔ w ⊧ φ ➝ ⊥ := by simp_all [Satisfies]; + end Satisfies open Satisfies -def ValidOnModel (M : Model α) (φ : Formula α) := ∀ w : M.World, w ⊧ φ +def ValidOnModel (M : Kripke.Model) (φ : Formula ℕ) := ∀ w : M.World, w ⊧ φ namespace ValidOnModel -instance semantics : Semantics (Formula α) (Model α) := ⟨fun M ↦ Formula.Kripke.ValidOnModel M⟩ +instance semantics : Semantics (Formula ℕ) (Model) := ⟨fun M ↦ Formula.Kripke.ValidOnModel M⟩ -variable {M : Model α} {φ ψ χ : Formula α} +variable {M : Model} {φ ψ χ : Formula ℕ} @[simp] protected lemma iff_models : M ⊧ φ ↔ Formula.Kripke.ValidOnModel M φ := iff_of_eq rfl protected lemma verum : M ⊧ ⊤ := by simp_all [ValidOnModel]; -protected lemma and₁ : M ⊧ φ ⋏ ψ ➝ φ := by simp_all [ValidOnModel, Satisfies]; +protected lemma andElim₁ : M ⊧ φ ⋏ ψ ➝ φ := by simp_all [ValidOnModel, Satisfies]; -protected lemma and₂ : M ⊧ φ ⋏ ψ ➝ ψ := by simp_all [ValidOnModel, Satisfies]; +protected lemma andElim₂ : M ⊧ φ ⋏ ψ ➝ ψ := by simp_all [ValidOnModel, Satisfies]; -protected lemma and₃ - (atom_hereditary : ∀ {w₁ w₂ : M.World}, (w₁ ≺ w₂) → ∀ {a}, (M.Valuation w₁ a) → (M.Valuation w₂ a)) - (F_trans : Transitive M.Frame.Rel) - : M ⊧ φ ➝ ψ ➝ φ ⋏ ψ := by +protected lemma andInst₃ : M ⊧ φ ➝ ψ ➝ φ ⋏ ψ := by intro x y _ hp z Ryz hq; - replace hp : Satisfies M z φ := formula_hereditary atom_hereditary F_trans Ryz hp; + replace hp : Satisfies M z φ := formula_hereditary Ryz hp; exact ⟨hp, hq⟩; -protected lemma or₁ : M ⊧ φ ➝ φ ⋎ ψ := by simp_all [ValidOnModel, Satisfies]; +protected lemma orInst₁ : M ⊧ φ ➝ φ ⋎ ψ := by simp_all [ValidOnModel, Satisfies]; -protected lemma or₂ : M ⊧ ψ ➝ φ ⋎ ψ := by simp_all [ValidOnModel, Satisfies]; +protected lemma orInst₂ : M ⊧ ψ ➝ φ ⋎ ψ := by simp_all [ValidOnModel, Satisfies]; -protected lemma or₃ - (F_trans : Transitive M.Frame.Rel) - : M ⊧ (φ ➝ χ) ➝ (ψ ➝ χ) ➝ (φ ⋎ ψ ➝ χ) := by +protected lemma orElim : M ⊧ (φ ➝ χ) ➝ (ψ ➝ χ) ➝ (φ ⋎ ψ ➝ χ) := by simp_all only [ValidOnModel.iff_models, ValidOnModel, Satisfies.iff_models, Satisfies.imp_def, Satisfies.or_def]; intro w₁ w₂ _ hpr w₃ hw₂₃ hqr w₄ hw₃₄ hpq; cases hpq with - | inl hp => exact hpr (F_trans hw₂₃ hw₃₄) hp; + | inl hp => exact hpr (M.rel_trans hw₂₃ hw₃₄) hp; | inr hq => exact hqr hw₃₄ hq; -protected lemma imply₁ - (atom_hereditary : ∀ {w₁ w₂ : M.World}, (w₁ ≺ w₂) → ∀ {a}, (M.Valuation w₁ a) → (M.Valuation w₂ a)) - (F_trans : Transitive M.Frame.Rel) - : M ⊧ φ ➝ ψ ➝ φ := by +protected lemma imply₁ : M ⊧ φ ➝ ψ ➝ φ := by intro x y _ hp z Ryz _; - exact formula_hereditary atom_hereditary F_trans Ryz hp; + exact formula_hereditary Ryz hp; -protected lemma imply₂ - (F_trans : Transitive M.Frame.Rel) - (F_refl : Reflexive M.Frame.Rel) - : M ⊧ (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ := by +protected lemma imply₂ : M ⊧ (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ := by intro x y _ hpqr z Ryz hpq w Rzw hp; - have Ryw := F_trans Ryz Rzw; - have Rww := F_refl w; + have Ryw : y ≺ w := by trans z <;> assumption; + have Rww : w ≺ w := by simp; exact hpqr Ryw hp Rww (hpq Rzw hp); -protected lemma mdp (F_refl : Reflexive M.Frame.Rel) (hpq : M ⊧ φ ➝ ψ) (hp : M ⊧ φ) : M ⊧ ψ := by +protected lemma mdp (hpq : M ⊧ φ ➝ ψ) (hp : M ⊧ φ) : M ⊧ ψ := by intro w; - exact hpq w (F_refl w) $ hp w; + exact hpq w Frame.rel_refl $ hp w; + +protected lemma bot : ¬M ⊧ ⊥ := by simp [ValidOnModel, Satisfies]; + +instance : Semantics.Bot (Kripke.Model) := ⟨λ _ => ValidOnModel.bot⟩ protected lemma efq : M ⊧ Axioms.EFQ φ := by simp [ValidOnModel, Satisfies]; @@ -137,10 +200,7 @@ protected lemma neg_equiv : M ⊧ Axioms.NegEquiv φ := by . intro x _ h y rxy hyp; exact h rxy hyp; . intro x _ h y rxy; exact h rxy; -protected lemma lem - (atom_hereditary : ∀ {w₁ w₂ : M.World}, (w₁ ≺ w₂) → ∀ {a}, (M.Valuation w₁ a) → (M.Valuation w₂ a)) - (F_trans : Transitive M.Frame.Rel) - : Symmetric M.Frame.Rel → M ⊧ Axioms.LEM φ := by +protected lemma lem : Symmetric M.Rel → M ⊧ Axioms.LEM φ := by simp_all [ValidOnModel, Satisfies, Symmetric]; contrapose; push_neg; rintro ⟨x, nhxp, ⟨y, Rxy, hyp⟩⟩; @@ -148,29 +208,23 @@ protected lemma lem constructor; . exact Rxy; . by_contra Ryx; - have := formula_hereditary atom_hereditary F_trans Ryx hyp; + have := formula_hereditary Ryx hyp; contradiction; -protected lemma dum - (atom_hereditary : ∀ {w₁ w₂ : M.World}, (w₁ ≺ w₂) → ∀ {a}, (M.Valuation w₁ a) → (M.Valuation w₂ a)) - (F_trans : Transitive M.Frame.Rel) - : Connected M.Frame.Rel → M ⊧ Axioms.GD φ ψ := by +protected lemma dum : Connected M.Rel → M ⊧ Axioms.Dummett φ ψ := by simp [ValidOnModel, Satisfies, Connected]; contrapose; push_neg; rintro ⟨x, ⟨y, Rxy, hyp, nhyq⟩, ⟨z, Ryz, hzq, nhyp⟩⟩; use x, y, z; refine ⟨Rxy, Ryz, ?_, ?_⟩; . by_contra Ryz; - have := formula_hereditary atom_hereditary F_trans Ryz hyp; + have := formula_hereditary Ryz hyp; contradiction; . by_contra Rzy; - have := formula_hereditary atom_hereditary F_trans Rzy hzq; + have := formula_hereditary Rzy hzq; contradiction; -protected lemma wlem - (atom_hereditary : ∀ {w₁ w₂ : M.World}, (w₁ ≺ w₂) → ∀ {a}, (M.Valuation w₁ a) → (M.Valuation w₂ a)) - (F_trans : Transitive M.Frame.Rel) - : Confluent M.Frame.Rel → M ⊧ Axioms.WeakLEM φ := by +protected lemma wlem : Confluent M.Rel → M ⊧ Axioms.WeakLEM φ := by simp [ValidOnModel, Satisfies, Confluent]; contrapose; push_neg; rintro ⟨x, ⟨y, Rxy, hyp⟩, ⟨z, Rxz, hz⟩⟩; @@ -178,320 +232,290 @@ protected lemma wlem refine ⟨Rxy, Rxz, ?_⟩; rintro w Ryw; by_contra Rzw; - have := formula_hereditary atom_hereditary F_trans Ryw hyp; + have := formula_hereditary Ryw hyp; have := hz w Rzw; contradiction; end ValidOnModel -def ValidOnFrame (F : Frame) (φ : Formula α) := ∀ {V : Valuation F α}, (_ : V.atomic_hereditary) → (⟨F, V⟩ : Kripke.Model α) ⊧ φ +def ValidOnFrame (F : Frame) (φ : Formula ℕ) := ∀ {V}, (⟨F, V⟩ : Kripke.Model) ⊧ φ namespace ValidOnFrame -instance semantics : Semantics (Formula α) (Frame.Dep α) := ⟨fun F ↦ Formula.Kripke.ValidOnFrame F⟩ +instance semantics : Semantics (Formula ℕ) (Frame) := ⟨fun F ↦ Formula.Kripke.ValidOnFrame F⟩ -variable {F : Frame.Dep α} +variable {F : Frame} {φ ψ χ : Formula ℕ} -@[simp] protected lemma models_iff : F ⊧ f ↔ ValidOnFrame F f := iff_of_eq rfl +@[simp] protected lemma models_iff : F ⊧ φ ↔ ValidOnFrame F φ := iff_of_eq rfl -variable {F : Frame.Dep α} {φ ψ χ : Formula α} +protected lemma verum : F ⊧ ⊤ := ValidOnModel.verum -protected lemma verum : F ⊧ ⊤ := fun _ => ValidOnModel.verum +protected lemma andElim₁ : F ⊧ φ ⋏ ψ ➝ φ := ValidOnModel.andElim₁ -protected lemma and₁ : F ⊧ φ ⋏ ψ ➝ φ := fun _ => ValidOnModel.and₁ +protected lemma andElim₂ : F ⊧ φ ⋏ ψ ➝ ψ := ValidOnModel.andElim₂ -protected lemma and₂ : F ⊧ φ ⋏ ψ ➝ ψ := fun _ => ValidOnModel.and₂ +protected lemma andInst₃ : F ⊧ φ ➝ ψ ➝ φ ⋏ ψ := ValidOnModel.andInst₃ -protected lemma and₃ (F_trans : Transitive F) : F ⊧ φ ➝ ψ ➝ φ ⋏ ψ := fun hV => ValidOnModel.and₃ hV F_trans +protected lemma orInst₁ : F ⊧ φ ➝ φ ⋎ ψ := ValidOnModel.orInst₁ -protected lemma or₁ : F ⊧ φ ➝ φ ⋎ ψ := fun _ => ValidOnModel.or₁ +protected lemma orInst₂ : F ⊧ ψ ➝ φ ⋎ ψ := ValidOnModel.orInst₂ -protected lemma or₂ : F ⊧ ψ ➝ φ ⋎ ψ := fun _ => ValidOnModel.or₂ +protected lemma orElim : F ⊧ (φ ➝ χ) ➝ (ψ ➝ χ) ➝ (φ ⋎ ψ ➝ χ) := ValidOnModel.orElim -protected lemma or₃ (F_trans : Transitive F) : F ⊧ (φ ➝ χ) ➝ (ψ ➝ χ) ➝ (φ ⋎ ψ ➝ χ) := fun _ => ValidOnModel.or₃ F_trans +protected lemma imply₁ : F ⊧ φ ➝ ψ ➝ φ := ValidOnModel.imply₁ -protected lemma imply₁ (F_trans : Transitive F) : F ⊧ φ ➝ ψ ➝ φ := fun hV => ValidOnModel.imply₁ hV F_trans +protected lemma imply₂ : F ⊧ (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ := ValidOnModel.imply₂ -protected lemma imply₂ (F_trans : Transitive F) (F_refl : Reflexive F) : F ⊧ (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ := fun _ => ValidOnModel.imply₂ F_trans F_refl +protected lemma mdp (hpq : F ⊧ φ ➝ ψ) (hp : F ⊧ φ) : F ⊧ ψ := ValidOnModel.mdp hpq hp -protected lemma mdp (F_refl : Reflexive F) (hpq : F ⊧ φ ➝ ψ) (hp : F ⊧ φ) : F ⊧ ψ := fun hV => ValidOnModel.mdp F_refl (hpq hV) (hp hV) +protected lemma efq : F ⊧ Axioms.EFQ φ := ValidOnModel.efq -protected lemma efq : F ⊧ Axioms.EFQ φ := fun _ => ValidOnModel.efq +protected lemma neg_equiv : F ⊧ Axioms.NegEquiv φ := ValidOnModel.neg_equiv -protected lemma neg_equiv : F ⊧ Axioms.NegEquiv φ := fun _ => ValidOnModel.neg_equiv +protected lemma lem (F_symm : Symmetric F.Rel) : F ⊧ Axioms.LEM φ := ValidOnModel.lem F_symm -protected lemma lem (F_trans : Transitive F) (F_symm : Symmetric F.Rel) : F ⊧ Axioms.LEM φ := fun hV => ValidOnModel.lem hV F_trans F_symm +protected lemma dum (F_conn : Connected F.Rel) : F ⊧ Axioms.Dummett φ ψ := ValidOnModel.dum F_conn -protected lemma dum (F_trans : Transitive F) (F_conn : Connected F.Rel) : F ⊧ Axioms.GD φ ψ := fun hV => ValidOnModel.dum hV F_trans F_conn +protected lemma wlem (F_conf : Confluent F.Rel) : F ⊧ Axioms.WeakLEM φ := ValidOnModel.wlem F_conf -protected lemma wlem (F_trans : Transitive F) (F_conf : Confluent F.Rel) : F ⊧ Axioms.WeakLEM φ := fun hV => ValidOnModel.wlem hV F_trans F_conf +protected lemma top : F ⊧ ⊤ := by + simp [ValidOnFrame.models_iff, ValidOnFrame]; + tauto; +instance : Semantics.Top (Frame) := ⟨λ _ => ValidOnFrame.top⟩ + +protected lemma bot : ¬F ⊧ ⊥ := by + simp [ValidOnFrame.models_iff, ValidOnFrame]; + use ⟨(λ _ _ => True), by tauto⟩; +instance : Semantics.Bot (Frame) := ⟨λ _ => ValidOnFrame.bot⟩ -instance : Semantics.Bot (Frame.Dep α) where - realize_bot _ := by - simp [ValidOnModel, ValidOnFrame]; - existsi (λ _ _ => True); - simp_all [Satisfies, Valuation.atomic_hereditary]; end ValidOnFrame -@[simp] def ValidOnFrameClass (𝔽 : FrameClass) (φ : Formula α) := ∀ {F : Frame}, F ∈ 𝔽 → F#α ⊧ φ +@[simp] def ValidOnFrameClass (C : FrameClass) (φ : Formula ℕ) := ∀ F, F ∈ C → F ⊧ φ namespace ValidOnFrameClass -instance semantics : Semantics (Formula α) (FrameClass.Dep α) := ⟨fun 𝔽 ↦ Kripke.ValidOnFrameClass 𝔽⟩ +variable {C : FrameClass} {φ ψ χ : Formula ℕ} + +instance semantics : Semantics (Formula ℕ) (FrameClass) := ⟨fun C ↦ Kripke.ValidOnFrameClass C⟩ -variable {𝔽 : FrameClass.Dep α} +@[simp] protected lemma models_iff : C ⊧ φ ↔ Formula.Kripke.ValidOnFrameClass C φ := iff_of_eq rfl -@[simp] protected lemma models_iff : 𝔽 ⊧ φ ↔ Formula.Kripke.ValidOnFrameClass 𝔽 φ := iff_of_eq rfl +protected lemma bot (h_nonempty : C.Nonempty) : ¬C ⊧ ⊥ := by + simp [ValidOnFrameClass.models_iff, ValidOnFrameClass]; + exact h_nonempty; end ValidOnFrameClass end Formula.Kripke - -open Formula.Kripke -open Formula.Kripke.Satisfies (formula_hereditary) - namespace Kripke -abbrev FrameClassOfTheory (T : Theory α) : FrameClass.Dep α := { F | F#α ⊧* T } -notation "𝔽(" T ")" => FrameClassOfTheory T +/-- + A set of formula that valid on frame `F`. +-/ +def Frame.theorems (F : Kripke.Frame) : Set (Formula ℕ) := { φ | F ⊧ φ } -abbrev FrameClassOfHilbert (H : Hilbert α) : FrameClass.Dep α := 𝔽((System.theory H)) -notation "𝔽(" H ")" => FrameClassOfHilbert H +def FrameClass.DefinedBy (C : FrameClass) (T : Set (Formula ℕ)) : Prop := ∀ F, F ∈ C ↔ F ⊧* T -section Soundness +section definability -variable {H : Hilbert α} - {φ : Formula α} +variable {F : Kripke.Frame} -lemma sound : H ⊢! φ → 𝔽(H) ⊧ φ := by - intro hp F hF; - simp [System.theory] at hF; - exact hF φ hp; +instance AllFrameClass.defined_by_EFQ : AllFrameClass.DefinedBy 𝗘𝗙𝗤 := by + intro F; + simp [Semantics.RealizeSet]; + apply Formula.Kripke.ValidOnFrame.efq; -instance : Sound H 𝔽(H) := ⟨sound⟩ +instance ConfluentFrameClass.defined_by_WLEM : ConfluentFrameClass.DefinedBy 𝗪𝗟𝗘𝗠 := by + intro F; + simp [Semantics.RealizeSet]; + constructor; + . rintro hCon φ V; + exact Kripke.ValidOnModel.wlem hCon; + . rintro h x y z ⟨Rxy, Rxz⟩; + let M : Kripke.Model := ⟨F, λ {v _} => y ≺ v, by simp; intro w _ _ _; trans w <;> assumption⟩; + have : ¬Kripke.Satisfies M x (∼(atom default)) := by + simp [Kripke.Satisfies]; + use y; + constructor; + . exact Rxy; + . apply F.rel_refl; + have : Kripke.Satisfies M x (∼∼(atom default)) := by + have := @h (atom default) M.Val x; + simp only [Axioms.WeakLEM, Semantics.Realize] at this; + apply or_iff_not_imp_left.mp $ Kripke.Satisfies.or_def.mp this; + assumption; + have := this Rxz; simp [Semantics.Realize, Kripke.Satisfies] at this; + obtain ⟨w, ⟨Rzw, hw⟩⟩ := this; + use w; + +instance ConnectedFrameClass.defined_by_Dummett : ConnectedFrameClass.DefinedBy 𝗗𝘂𝗺 := by + intro F; + simp [Semantics.RealizeSet]; + constructor; + . rintro hCon _ φ ψ rfl; + exact Kripke.ValidOnModel.dum hCon; + . rintro h x y z ⟨Rxy, Rxz⟩; + let M : Kripke.Model := ⟨F, ⟨λ {v a} => match a with | 0 => y ≺ v | 1 => z ≺ v | _ => True, by + intro w v Rwv a ha; + split at ha; + . exact F.rel_trans ha Rwv; + . exact F.rel_trans ha Rwv; + . tauto; + ⟩⟩; + rcases Kripke.Satisfies.or_def.mp $ @h (Axioms.Dummett (atom 0) (atom 1)) (atom 0) (atom 1) rfl M.Val x with (hi | hi); + . have := Kripke.Satisfies.imp_def.mp hi Rxy; + simp [Semantics.Realize, Kripke.Satisfies] at this; + tauto; + . have := Kripke.Satisfies.imp_def.mp hi Rxz; + simp [Semantics.Realize, Kripke.Satisfies] at this; + tauto; -lemma unprovable_bot (hc : 𝔽(H).Nonempty) : H ⊬ ⊥ := by - apply (not_imp_not.mpr (sound (α := α))); - simp [Semantics.Realize]; - obtain ⟨F, hF⟩ := hc; - use F; +section + +private lemma euclidean_of_subset_lem_frameTheorems : (𝗟𝗘𝗠 ⊆ F.theorems) → Euclidean F := by + simp [Frame.theorems]; + rintro h x y z Rxy Rxz; + let M : Kripke.Model := ⟨F, λ v _ => z ≺ v, by simp; intro w v _ _; trans w <;> assumption⟩; + suffices Kripke.Satisfies M y (atom default) by simpa [Kripke.Satisfies] using this; + apply M.Val.hereditary Rxy; + have := @h (atom default) M.Val x; + simp only [Axioms.LEM, Semantics.Realize, Kripke.Satisfies, or_iff_not_imp_right] at this; + apply this; + push_neg; + use z; constructor; - . exact hF; - . exact Semantics.Bot.realize_bot (F := Formula α) (M := Frame.Dep α) F; + . exact Rxz; + . simp [Kripke.Satisfies]; -instance (hc : 𝔽(H).Nonempty) : System.Consistent H := System.Consistent.of_unprovable $ unprovable_bot hc +private lemma subset_lem_frameTheorems_of_symmetric : Symmetric F → 𝗟𝗘𝗠 ⊆ F.theorems := by + simp [Frame.theorems]; + rintro hSym φ _ V; + apply Kripke.ValidOnModel.lem hSym; +private lemma subset_lem_frameTheorems_iff_euclidean : 𝗟𝗘𝗠 ⊆ F.theorems ↔ Euclidean F := by + constructor; + . exact euclidean_of_subset_lem_frameTheorems; + . intro hEucl; + apply subset_lem_frameTheorems_of_symmetric; + apply symm_of_refl_eucl; + . exact F.rel_refl'; + . assumption; + +instance EuclideanFrameClass.defined_by_LEM : EuclideanFrameClass.DefinedBy 𝗟𝗘𝗠 := by + intro F; + simp [Semantics.RealizeSet]; + constructor; + . intro hEucl; + simpa [Frame.theorems] using subset_lem_frameTheorems_iff_euclidean.mpr hEucl; + . intro h; + apply subset_lem_frameTheorems_iff_euclidean.mp; + simpa [Frame.theorems] using h; -lemma sound_of_characterizability [characterizability : 𝔽(H).Characteraizable 𝔽₂] : H ⊢! φ → 𝔽₂#α ⊧ φ := by - intro h F hF; - apply sound h; - apply characterizability.characterize hF; +end -instance instSoundOfCharacterizability [𝔽(H).Characteraizable 𝔽₂] : Sound H (𝔽₂#α) := ⟨sound_of_characterizability⟩ +end definability -lemma unprovable_bot_of_characterizability [characterizability : 𝔽(H).Characteraizable 𝔽₂] : H ⊬ ⊥ := by - apply unprovable_bot; - obtain ⟨F, hF⟩ := characterizability.nonempty; - use F; - apply characterizability.characterize hF; +end Kripke -instance instConsistentOfCharacterizability [FrameClass.Characteraizable.{u} 𝔽(H) 𝔽₂] : System.Consistent H := System.Consistent.of_unprovable $ unprovable_bot_of_characterizability -end Soundness +namespace Hilbert +namespace Kripke -section +open Formula.Kripke -variable {α : Type u} - -instance Int_Characteraizable : 𝔽((Hilbert.Int α)).Characteraizable ReflexiveTransitiveFrameClass where - characterize := by - simp [System.theory]; - rintro F hTrans hRefl φ hp; - induction hp using Hilbert.Deduction.rec! with - | verum => apply ValidOnFrame.verum; - | imply₁ => apply ValidOnFrame.imply₁; simpa; - | imply₂ => apply ValidOnFrame.imply₂; simpa; simpa; - | and₁ => apply ValidOnFrame.and₁; - | and₂ => apply ValidOnFrame.and₂; - | and₃ => apply ValidOnFrame.and₃; simpa; - | or₁ => apply ValidOnFrame.or₁; - | or₂ => apply ValidOnFrame.or₂; - | or₃ => apply ValidOnFrame.or₃; simpa; - | neg_equiv => apply ValidOnFrame.neg_equiv; - | mdp ihpq ihp => - apply ValidOnFrame.mdp; - repeat simpa only [ValidOnFrame.models_iff]; - | eaxm h => - obtain ⟨_, rfl⟩ := h; - apply ValidOnFrame.efq; - nonempty := by - use { World := PUnit, Rel := λ _ _ => True }; - refine ⟨by simp [Reflexive], by simp [Transitive]⟩; - - -instance Int_sound : Sound (Hilbert.Int α) (ReflexiveTransitiveFrameClass#α) := inferInstance - -instance : System.Consistent (Hilbert.Int α) := inferInstance - - -instance Cl_Characteraizable : 𝔽(Hilbert.Cl α).Characteraizable ReflexiveTransitiveSymmetricFrameClass#α where - characterize := by - simp [System.theory]; - rintro F hTrans hRefl hSymm φ hp; - induction hp using Hilbert.Deduction.rec! with - | verum => apply ValidOnFrame.verum; - | imply₁ => apply ValidOnFrame.imply₁; simpa; - | imply₂ => apply ValidOnFrame.imply₂; simpa; simpa; - | and₁ => apply ValidOnFrame.and₁; - | and₂ => apply ValidOnFrame.and₂; - | and₃ => apply ValidOnFrame.and₃; simpa; - | or₁ => apply ValidOnFrame.or₁; - | or₂ => apply ValidOnFrame.or₂; - | or₃ => apply ValidOnFrame.or₃; simpa; - | neg_equiv => apply ValidOnFrame.neg_equiv; - | mdp ihpq ihp => - apply ValidOnFrame.mdp; - repeat simpa; - | eaxm h => - rcases h with (⟨_, rfl⟩ | ⟨_, rfl⟩); - . apply ValidOnFrame.efq; - . apply ValidOnFrame.lem; simpa; simpa; - nonempty := by - use { World := PUnit, Rel := λ _ _ => True }; - refine ⟨by simp [Reflexive], by simp [Transitive], by simp [Symmetric]⟩; - -instance : Sound (Hilbert.Cl α) (ReflexiveTransitiveSymmetricFrameClass#α) := inferInstance - -instance : System.Consistent (Hilbert.Cl α) := inferInstance - - - -instance KC_Characteraizable : 𝔽(Hilbert.KC α).Characteraizable ReflexiveTransitiveConfluentFrameClass where - characterize := by - rintro F ⟨F_trans, F_refl, F_confl⟩; - simp [System.theory]; - intro φ hp; - induction hp using Hilbert.Deduction.rec! with - | verum => apply ValidOnFrame.verum; - | imply₁ => apply ValidOnFrame.imply₁; simpa; - | imply₂ => apply ValidOnFrame.imply₂; simpa; simpa; - | and₁ => apply ValidOnFrame.and₁; - | and₂ => apply ValidOnFrame.and₂; - | and₃ => apply ValidOnFrame.and₃; simpa; - | or₁ => apply ValidOnFrame.or₁; - | or₂ => apply ValidOnFrame.or₂; - | or₃ => apply ValidOnFrame.or₃; simpa; - | neg_equiv => apply ValidOnFrame.neg_equiv; - | mdp ihpq ihp => - apply ValidOnFrame.mdp; - repeat simpa; - | eaxm h => - rcases h with (⟨_, rfl⟩ | ⟨_, _, rfl⟩); - . apply ValidOnFrame.efq; - . apply ValidOnFrame.wlem; simpa; simpa; - nonempty := by - use { World := PUnit, Rel := λ _ _ => True }; - refine ⟨by simp [Reflexive], by simp [Transitive], by simp [Confluent]⟩; - -instance : Sound (Hilbert.KC α) (ReflexiveTransitiveConfluentFrameClass#α) := inferInstance - -instance : System.Consistent (Hilbert.KC α) := inferInstance - - -instance LC_Characteraizable : 𝔽((Hilbert.LC α)).Characteraizable ReflexiveTransitiveConnectedFrameClass where - characterize := by - rintro F ⟨F_trans, F_refl, F_conn⟩; - simp [System.theory]; - intro φ hp; - induction hp using Hilbert.Deduction.rec! with - | verum => apply ValidOnFrame.verum; - | imply₁ => apply ValidOnFrame.imply₁; simpa; - | imply₂ => apply ValidOnFrame.imply₂; simpa; simpa; - | and₁ => apply ValidOnFrame.and₁; - | and₂ => apply ValidOnFrame.and₂; - | and₃ => apply ValidOnFrame.and₃; simpa; - | or₁ => apply ValidOnFrame.or₁; - | or₂ => apply ValidOnFrame.or₂; - | or₃ => apply ValidOnFrame.or₃; simpa; - | neg_equiv => apply ValidOnFrame.neg_equiv; - | mdp ihpq ihp => - apply ValidOnFrame.mdp; - repeat simpa; - | eaxm h => - rcases h with (⟨_, rfl⟩ | ⟨_, _, rfl⟩); - . apply ValidOnFrame.efq; - . apply ValidOnFrame.dum; simpa; simpa; - nonempty := by - use { World := PUnit, Rel := λ _ _ => True }; - refine ⟨by simp [Reflexive], by simp [Transitive], by simp [Connected]⟩; - -instance : Sound (Hilbert.LC α) (ReflexiveTransitiveConnectedFrameClass#α) := inferInstance - -instance : System.Consistent (Hilbert.LC α) := inferInstance +variable {H : Hilbert ℕ} {φ : Formula ℕ} +variable {C : FrameClass} {T : Set (Formula ℕ)} + +lemma sound_hilbert_of_frameclass (definedBy : C.DefinedBy T) : (⟨𝗘𝗙𝗤 ∪ T⟩ : Hilbert ℕ) ⊢! φ → C ⊧ φ := by + intro hφ F hF; + induction hφ using Hilbert.Deduction.rec! with + | verum => apply ValidOnFrame.verum; + | imply₁ => apply ValidOnFrame.imply₁; + | imply₂ => apply ValidOnFrame.imply₂; + | and₁ => apply ValidOnFrame.andElim₁; + | and₂ => apply ValidOnFrame.andElim₂; + | and₃ => apply ValidOnFrame.andInst₃; + | or₁ => apply ValidOnFrame.orInst₁; + | or₂ => apply ValidOnFrame.orInst₂; + | or₃ => apply ValidOnFrame.orElim; + | neg_equiv => apply ValidOnFrame.neg_equiv; + | mdp => exact ValidOnFrame.mdp (by assumption) (by assumption); + | eaxm hi => + rcases hi with (⟨_, rfl⟩ | h); + . apply ValidOnFrame.efq; + . apply Semantics.realizeSet_iff.mp (definedBy F |>.mp hF); + assumption; + +lemma sound_of_equiv_frameclass_hilbert (definedBy : C.DefinedBy T) (heq : (⟨𝗘𝗙𝗤 ∪ T⟩ : Hilbert ℕ) =ₛ H) : H ⊢! φ → C ⊧ φ := by + intro hφ; + apply sound_hilbert_of_frameclass (T := T) (definedBy); + exact Equiv.iff.mp heq φ |>.mpr hφ; + +protected instance instSound (definedBy : C.DefinedBy T) (heq : (⟨𝗘𝗙𝗤 ∪ T⟩ : Hilbert ℕ) =ₛ H) : Sound H C := ⟨sound_of_equiv_frameclass_hilbert definedBy heq⟩ + +lemma unprovable_bot [sound : Sound H C] (hNonempty : C.Nonempty) : H ⊬ ⊥ := by + apply not_imp_not.mpr sound.sound; + simp [Semantics.Realize]; + obtain ⟨F, hF⟩ := hNonempty; + use F; + constructor; + . exact hF; + . exact Semantics.Bot.realize_bot (F := Formula ℕ) (M := Frame) F; -end +lemma consistent [Sound H C] (h_nonempty : C.Nonempty) : H.Consistent := System.Consistent.of_unprovable $ unprovable_bot h_nonempty end Kripke -section Classical +namespace Int -open LO.Kripke +instance Kripke.sound : Sound (Hilbert.Int ℕ) (AllFrameClass) := Kripke.instSound AllFrameClass.defined_by_EFQ $ by simp -namespace Formula.Kripke +instance : (Hilbert.Int ℕ).Consistent := Kripke.consistent (C := AllFrameClass) $ by + use pointFrame; + tauto; -abbrev ClassicalSatisfies (V : ClassicalValuation α) (φ : Formula α) : Prop := Satisfies (ClassicalModel V) () φ +end Int -instance : Semantics (Formula α) (ClassicalValuation α) := ⟨ClassicalSatisfies⟩ -namespace ClassicalSatisfies +namespace KC -variable {V : ClassicalValuation α} +instance Kripke.sound : Sound (Hilbert.KC ℕ) (ConfluentFrameClass) := Kripke.instSound ConfluentFrameClass.defined_by_WLEM $ by simp -@[simp] lemma atom_def : V ⊧ atom a ↔ V a := by simp only [Semantics.Realize, Satisfies] +instance : (Hilbert.KC ℕ).Consistent := Kripke.consistent (C := ConfluentFrameClass) $ by + use pointFrame; + simp [Confluent] -instance : Semantics.Tarski (ClassicalValuation α) where - realize_top := by simp [Semantics.Realize, ClassicalSatisfies, Satisfies]; - realize_bot := by simp [Semantics.Realize, ClassicalSatisfies, Satisfies]; - realize_or := by simp [Semantics.Realize, ClassicalSatisfies, Satisfies]; - realize_and := by simp [Semantics.Realize, ClassicalSatisfies, Satisfies]; - realize_imp := by simp [Semantics.Realize, Satisfies]; tauto; - realize_not := by simp [Semantics.Realize, Satisfies]; tauto; +end KC -end ClassicalSatisfies -end Formula.Kripke +namespace LC +instance Kripke.sound : Sound (Hilbert.LC ℕ) (ConnectedFrameClass) := Kripke.instSound ConnectedFrameClass.defined_by_Dummett $ by simp -namespace Kripke +instance : (Hilbert.LC ℕ).Consistent := Kripke.consistent (C := ConnectedFrameClass) $ by + use pointFrame; + simp [Connected] -open Formula.Kripke (ClassicalSatisfies) +end LC -lemma ValidOnClassicalFrame_iff : (Kripke.FrameClassOfHilbert.{u, 0} (Hilbert.Cl α)) ⊧ φ → ∀ (V : ClassicalValuation α), V ⊧ φ := by - intro h V; - refine @h (ClassicalFrame) ?_ (λ _ a => V a) (by simp [Valuation.atomic_hereditary]) (); - . apply @Cl_Characteraizable α |>.characterize; - refine ⟨ClassicalFrame.reflexive, ClassicalFrame.transitive, ClassicalFrame.symmetric⟩; -lemma notClassicalValid_of_exists_ClassicalValuation : (∃ (V : ClassicalValuation α), ¬(V ⊧ φ)) → ¬(Kripke.FrameClassOfHilbert.{u, 0} (Hilbert.Cl α)) ⊧ φ := by - contrapose; push_neg; - have := @ValidOnClassicalFrame_iff α φ; - exact this; +namespace Cl -lemma unprovable_classical_of_exists_ClassicalValuation (h : ∃ (V : ClassicalValuation α), ¬(V ⊧ φ)) : (Hilbert.Cl α) ⊬ φ := by - apply not_imp_not.mpr $ Kripke.sound.{u, 0}; - apply notClassicalValid_of_exists_ClassicalValuation; - assumption; +instance Kripke.sound : Sound (Hilbert.Cl ℕ) (EuclideanFrameClass) := Kripke.instSound EuclideanFrameClass.defined_by_LEM $ by simp -end Kripke +instance : (Hilbert.Cl ℕ).Consistent := Kripke.consistent (C := EuclideanFrameClass) $ by + use pointFrame; + simp [Euclidean] -end Classical +end Cl +end Hilbert end LO.IntProp diff --git a/Foundation/Logic/Axioms.lean b/Foundation/Logic/Axioms.lean index 5d5d82a2..7e1a6fb9 100644 --- a/Foundation/Logic/Axioms.lean +++ b/Foundation/Logic/Axioms.lean @@ -53,9 +53,9 @@ protected abbrev WeakLEM := ∼φ ⋎ ∼∼φ abbrev WeakLEM.set : Set F := { Axioms.WeakLEM φ | (φ) } notation "𝗪𝗟𝗘𝗠" => WeakLEM.set -protected abbrev GD := (φ ➝ ψ) ⋎ (ψ ➝ φ) -abbrev GD.set : Set F := { Axioms.GD φ ψ | (φ) (ψ) } -notation "𝗗𝘂𝗺" => GD.set +protected abbrev Dummett := (φ ➝ ψ) ⋎ (ψ ➝ φ) +abbrev Dummett.set : Set F := { Axioms.Dummett φ ψ | (φ) (ψ) } +notation "𝗗𝘂𝗺" => Dummett.set protected abbrev DNE := ∼∼φ ➝ φ abbrev DNE.set : Set F := { Axioms.DNE φ | (φ) } diff --git a/Foundation/Logic/HilbertStyle/Basic.lean b/Foundation/Logic/HilbertStyle/Basic.lean index 10e21ef7..213d7a12 100644 --- a/Foundation/Logic/HilbertStyle/Basic.lean +++ b/Foundation/Logic/HilbertStyle/Basic.lean @@ -155,10 +155,10 @@ def wlem [HasAxiomWeakLEM 𝓢] : 𝓢 ⊢ ∼φ ⋎ ∼∼φ := HasAxiomWeakLEM class HasAxiomDummett (𝓢 : S) where - dummett (φ ψ : F) : 𝓢 ⊢ Axioms.GD φ ψ + dummett (φ ψ : F) : 𝓢 ⊢ Axioms.Dummett φ ψ def dummett [HasAxiomDummett 𝓢] : 𝓢 ⊢ (φ ➝ ψ) ⋎ (ψ ➝ φ) := HasAxiomDummett.dummett φ ψ -@[simp] lemma dummett! [HasAxiomDummett 𝓢] : 𝓢 ⊢! Axioms.GD φ ψ := ⟨dummett⟩ +@[simp] lemma dummett! [HasAxiomDummett 𝓢] : 𝓢 ⊢! Axioms.Dummett φ ψ := ⟨dummett⟩ class HasAxiomPeirce (𝓢 : S) where diff --git a/Foundation/Logic/HilbertStyle/Supplemental.lean b/Foundation/Logic/HilbertStyle/Supplemental.lean index cb5201e2..bd316a3e 100644 --- a/Foundation/Logic/HilbertStyle/Supplemental.lean +++ b/Foundation/Logic/HilbertStyle/Supplemental.lean @@ -545,6 +545,29 @@ instance [HasAxiomEFQ 𝓢] [HasAxiomLEM 𝓢] : HasAxiomDummett 𝓢 where have d₂ : 𝓢 ⊢ ∼φ ➝ ((φ ➝ ψ) ⋎ (ψ ➝ φ)) := impTrans'' efq_imply_not₁ or₁; exact or₃''' d₁ d₂ lem; +instance [HasAxiomEFQ 𝓢] [HasAxiomDummett 𝓢] : HasAxiomWeakLEM 𝓢 where + wlem φ := by + haveI : 𝓢 ⊢ (φ ➝ ∼φ) ⋎ (∼φ ➝ φ) := dummett; + exact or₃''' (by + apply deduct'; + apply or₁'; + apply neg_equiv'.mpr; + apply deduct; + haveI d₁ : [φ, φ ➝ ∼φ] ⊢[𝓢] φ := FiniteContext.byAxm; + haveI d₂ : [φ, φ ➝ ∼φ] ⊢[𝓢] φ ➝ ∼φ := FiniteContext.byAxm; + have := neg_equiv'.mp $ d₂ ⨀ d₁; + exact this ⨀ d₁; + ) (by + apply deduct'; + apply or₂'; + apply neg_equiv'.mpr; + apply deduct; + haveI d₁ : [∼φ, ∼φ ➝ φ] ⊢[𝓢] ∼φ := FiniteContext.byAxm; + haveI d₂ : [∼φ, ∼φ ➝ φ] ⊢[𝓢] ∼φ ➝ φ := FiniteContext.byAxm; + haveI := d₂ ⨀ d₁; + exact (neg_equiv'.mp d₁) ⨀ this; + ) this; + noncomputable instance [HasAxiomDNE 𝓢] : HasAxiomPeirce 𝓢 where peirce φ ψ := by refine or₃''' imply₁ ?_ lem; diff --git a/Foundation/Logic/Kripke/Basic.lean b/Foundation/Logic/Kripke/Basic.lean index b27572c2..ab293156 100644 --- a/Foundation/Logic/Kripke/Basic.lean +++ b/Foundation/Logic/Kripke/Basic.lean @@ -216,7 +216,7 @@ namespace ClassicalFrame @[simp] lemma symmetric : Symmetric ClassicalFrame := by simp [Symmetric]; -@[simp] lemma extensive : Extensive ClassicalFrame := by simp [Extensive]; +@[simp] lemma extensive : Coreflexive ClassicalFrame := by simp [Coreflexive]; @[simp] lemma universal : Universal ClassicalFrame := by simp [Universal]; diff --git a/Foundation/Modal/Geach.lean b/Foundation/Modal/Geach.lean index a939af4a..bafab448 100644 --- a/Foundation/Modal/Geach.lean +++ b/Foundation/Modal/Geach.lean @@ -34,8 +34,8 @@ lemma euclidean_def : Euclidean R ↔ (GeachConfluent ⟨1, 1, 0, 1⟩ R) := by lemma confluent_def : Confluent R ↔ (GeachConfluent ⟨1, 1, 1, 1⟩ R) := by simp [GeachConfluent, Confluent]; -lemma extensive_def : Extensive R ↔ (GeachConfluent ⟨0, 1, 0, 0⟩ R) := by - simp [GeachConfluent, Extensive]; +lemma extensive_def : Coreflexive R ↔ (GeachConfluent ⟨0, 1, 0, 0⟩ R) := by + simp [GeachConfluent, Coreflexive]; constructor; . rintro h x y z rfl Rxz; have := h Rxz; tauto; . intro h x y Rxy; have := h rfl Rxy; tauto; diff --git a/Foundation/Modal/Maximal.lean b/Foundation/Modal/Maximal.lean index dedaa179..203e50cd 100644 --- a/Foundation/Modal/Maximal.lean +++ b/Foundation/Modal/Maximal.lean @@ -1,5 +1,5 @@ import Foundation.Modal.Hilbert -import Foundation.IntProp.Kripke.Semantics +import Foundation.IntProp.Kripke.Classical /-! # Maximality of `Hilbert.Triv α` and `𝐕𝐞𝐫` @@ -190,59 +190,57 @@ lemma verTranslated_of_GL : (Hilbert.GL α) ⊢! φ → (Hilbert.Cl α) ⊢! φ | _ => dsimp [VerTranslation]; trivial; -open IntProp.Kripke (unprovable_classical_of_exists_ClassicalValuation) +-- open IntProp.Kripke (unprovable_classical_of_exists_ClassicalValuation) -variable [Inhabited α] - -example : Hilbert.Triv α ⊬ Axioms.L (atom default : Formula α) := by +example (a : ℕ) : Hilbert.Triv ℕ ⊬ Axioms.L (atom a : Formula ℕ) := by apply iff_Triv_classical.not.mpr; - apply unprovable_classical_of_exists_ClassicalValuation; + apply IntProp.Hilbert.Cl.unprovable_of_exists_classicalValuation; simp [Axioms.L, TrivTranslation, toPropFormula, IntProp.Formula.Kripke.Satisfies]; use (λ _ => False); tauto; -lemma unprovable_AxiomL_K4 : Hilbert.K4 α ⊬ Axioms.L (atom default : Formula α) := by +lemma unprovable_AxiomL_K4 {a : ℕ} : Hilbert.K4 ℕ ⊬ Axioms.L (atom a : Formula ℕ) := by apply not_imp_not.mpr trivTranslated_of_K4; - apply unprovable_classical_of_exists_ClassicalValuation; + apply IntProp.Hilbert.Cl.unprovable_of_exists_classicalValuation; simp [Axioms.L, TrivTranslation, toPropFormula, IntProp.Formula.Kripke.Satisfies]; use (λ _ => False); tauto; -theorem K4_strictReducible_GL : (Hilbert.K4 α) <ₛ (Hilbert.GL α) := by +theorem K4_strictReducible_GL : (Hilbert.K4 ℕ) <ₛ (Hilbert.GL ℕ) := by dsimp [StrictlyWeakerThan]; constructor; . apply K4_weakerThan_GL; . simp [System.not_weakerThan_iff]; - existsi (Axioms.L (atom default)) + use (Axioms.L (atom 0)); constructor; . exact axiomL!; . exact unprovable_AxiomL_K4; -lemma unprovable_AxiomT_GL : (Hilbert.GL α) ⊬ Axioms.T (atom default : Formula α) := by +lemma unprovable_AxiomT_GL {a : ℕ} : (Hilbert.GL ℕ) ⊬ Axioms.T (atom a : Formula ℕ) := by apply not_imp_not.mpr verTranslated_of_GL; - apply unprovable_classical_of_exists_ClassicalValuation; + apply IntProp.Hilbert.Cl.unprovable_of_exists_classicalValuation; simp [Axioms.T, VerTranslation, toPropFormula, IntProp.Formula.Kripke.Satisfies]; use (λ _ => False); tauto; -instance instGLConsistencyViaUnprovableAxiomT : System.Consistent (Hilbert.GL α) := by +instance instGLConsistencyViaUnprovableAxiomT : System.Consistent (Hilbert.GL ℕ) := by apply consistent_iff_exists_unprovable.mpr; - existsi (Axioms.T (atom default)); + use (Axioms.T (atom 0)); apply unprovable_AxiomT_GL; -theorem not_S4_weakerThan_GL : ¬(Hilbert.S4 α) ≤ₛ (Hilbert.GL α) := by +theorem not_S4_weakerThan_GL : ¬(Hilbert.S4 ℕ) ≤ₛ (Hilbert.GL ℕ) := by apply System.not_weakerThan_iff.mpr; - existsi (Axioms.T (atom default)); + existsi (Axioms.T (atom 0)); constructor; . exact axiomT!; . exact unprovable_AxiomT_GL; -example : (Hilbert.Ver α) ⊬ (∼(□⊥) : Formula α) := by +example : (Hilbert.Ver ℕ) ⊬ (∼(□⊥) : Formula ℕ) := by apply iff_Ver_classical.not.mpr; - apply unprovable_classical_of_exists_ClassicalValuation; + apply IntProp.Hilbert.Cl.unprovable_of_exists_classicalValuation; dsimp [VerTranslation, toPropFormula, IntProp.Formula.Kripke.Satisfies]; use (λ _ => True); simp; diff --git a/Foundation/Modal/ModalCompanion/GMT.lean b/Foundation/Modal/ModalCompanion/GMT.lean index cd769f6c..563cbe89 100644 --- a/Foundation/Modal/ModalCompanion/GMT.lean +++ b/Foundation/Modal/ModalCompanion/GMT.lean @@ -4,31 +4,31 @@ import Foundation.Modal.ModalCompanion.Basic namespace LO.Modal -open IntProp +open LO.IntProp open LO.Kripke open Modal.Kripke -variable {α : Type u} [DecidableEq α] [Inhabited α] [Encodable α] +variable {iH : IntProp.Hilbert ℕ} {mH : Modal.Hilbert ℕ} +variable {φ ψ χ : IntProp.Formula ℕ} -variable {iH : IntProp.Hilbert α} {mH : Modal.Hilbert α} -variable {φ ψ χ : IntProp.Formula α} - -lemma provable_S4_of_provable_efq : ((Hilbert.S4 α) ⊢! φᵍ) → ((Hilbert.Int α) ⊢! φ) := by +lemma provable_S4_of_provable_efq : ((Hilbert.S4 ℕ) ⊢! φᵍ) → ((Hilbert.Int ℕ) ⊢! φ) := by contrapose; intro h; - replace h := (not_imp_not.mpr $ IntProp.Kripke.Int_complete.complete) h; + replace h := (not_imp_not.mpr $ Hilbert.Int.Kripke.complete.complete) h; simp [IntProp.Formula.Kripke.ValidOnFrame, IntProp.Formula.Kripke.ValidOnModel] at h; - obtain ⟨F, F_refl, F_trans, V, V_hered, w, hp⟩ := h; + obtain ⟨F, V, w, hp⟩ := h; - have h₁ : ∀ ψ x, IntProp.Formula.Kripke.Satisfies ⟨F, V⟩ x ψ ↔ (Modal.Formula.Kripke.Satisfies ⟨F, V⟩ x (ψᵍ)) := by + have h₁ : ∀ ψ x, IntProp.Formula.Kripke.Satisfies ⟨F, V⟩ x ψ ↔ (Modal.Formula.Kripke.Satisfies ⟨⟨F.World, F.Rel⟩, V⟩ x (ψᵍ)) := by intro ψ x; induction ψ using IntProp.Formula.rec' generalizing x with | hatom a => simp [GoedelTranslation]; constructor; - . intro _ _ h; exact V_hered h (by assumption); - . intro h; exact h x (F_refl x); + . intro _ _ h; + exact V.hereditary h $ by assumption; + . intro h; + exact h x (F.rel_refl' x); | hor φ ψ ihp ihq => simp only [GoedelTranslation]; constructor; @@ -43,14 +43,18 @@ lemma provable_S4_of_provable_efq : ((Hilbert.S4 α) ⊢! φᵍ) → ((Hilbert.I . right; exact ihq x |>.mpr hq; | _ => simp_all [IntProp.Formula.Kripke.Satisfies, Modal.Formula.Kripke.Satisfies]; - have : ¬(Modal.Formula.Kripke.Satisfies ⟨F, V⟩ w (φᵍ)) := (h₁ φ w).not.mp hp; + have : ¬(Modal.Formula.Kripke.Satisfies ⟨⟨F.World, F.Rel⟩, V⟩ w (φᵍ)) := (h₁ φ w).not.mp hp; apply not_imp_not.mpr $ S4_sound_aux; simp [Formula.Kripke.ValidOnFrame, Formula.Kripke.ValidOnModel]; - use F; - exact ⟨⟨F_refl, F_trans⟩, by use V, w⟩; - -theorem provable_efq_iff_provable_S4 : (Hilbert.Int α) ⊢! φ ↔ (Hilbert.S4 α) ⊢! φᵍ := ⟨provable_efq_of_provable_S4, provable_S4_of_provable_efq⟩ -instance : ModalCompanion (Hilbert.Int α) (Hilbert.S4 α) := ⟨provable_efq_iff_provable_S4⟩ + use ⟨F.World, F.Rel⟩; + constructor; + . constructor; + . exact F.rel_refl'; + . exact F.rel_trans'; + . use V, w; + +theorem provable_efq_iff_provable_S4 : (Hilbert.Int ℕ) ⊢! φ ↔ (Hilbert.S4 ℕ) ⊢! φᵍ := ⟨provable_efq_of_provable_S4, provable_S4_of_provable_efq⟩ +instance : ModalCompanion (Hilbert.Int ℕ) (Hilbert.S4 ℕ) := ⟨provable_efq_iff_provable_S4⟩ end LO.Modal diff --git a/Foundation/Vorspiel/BinaryRelations.lean b/Foundation/Vorspiel/BinaryRelations.lean index ef1b78a4..e73bbebc 100644 --- a/Foundation/Vorspiel/BinaryRelations.lean +++ b/Foundation/Vorspiel/BinaryRelations.lean @@ -21,7 +21,9 @@ def Functional := ∀ ⦃x y z⦄, x ≺ y ∧ x ≺ z → y = z def RightConvergent := ∀ ⦃x y z⦄, x ≺ y ∧ x ≺ z → y ≺ z ∨ z ≺ y ∨ y = z -def Extensive := ∀ ⦃x y⦄, x ≺ y → x = y +def Coreflexive := ∀ ⦃x y⦄, x ≺ y → x = y + +def Equality := ∀ ⦃x y⦄, x ≺ y ↔ x = y def Antisymmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x → x = y @@ -94,11 +96,29 @@ lemma Finite.converseWellFounded_of_trans_irrefl' end ConverseWellFounded -lemma extensive_of_reflex_antisymm_eucl (hRefl : Reflexive rel) (hAntisymm : Antisymmetric rel) (hEucl : Euclidean rel) : Extensive rel := by - intro x y rxy; - have rxx := hRefl x; - exact hAntisymm rxy (hEucl rxx rxy); +lemma corefl_of_refl_assym_eucl (hRefl : Reflexive rel) (hAntisymm : Antisymmetric rel) (hEucl : Euclidean rel) : Coreflexive rel := by + intro x y Rxy; + have Ryx := hEucl (hRefl x) Rxy; + exact hAntisymm Rxy Ryx; + +lemma equality_of_refl_corefl (hRefl : Reflexive rel) (hCorefl : Coreflexive rel) : Equality rel := by + intro x y; + constructor; + . apply hCorefl; + . rintro rfl; apply hRefl; + +lemma equality_of_refl_assym_eucl (hRefl : Reflexive rel) (hAntisymm : Antisymmetric rel) (hEucl : Euclidean rel) : Equality rel := by + apply equality_of_refl_corefl; + . assumption; + . exact corefl_of_refl_assym_eucl hRefl hAntisymm hEucl; + +lemma refl_of_equality (h : Equality rel) : Reflexive rel := by + intro x; + exact h.mpr rfl; +lemma corefl_of_equality (h : Equality rel) : Coreflexive rel := by + intro x y Rxy; + apply h.mp Rxy; lemma irreflexive_of_assymetric (hAssym : Assymetric rel) : Irreflexive rel := by intro x Rxx; @@ -112,6 +132,7 @@ lemma refl_of_universal (h : Universal rel) : Reflexive rel := by lemma eucl_of_universal (h : Universal rel) : Euclidean rel := by rintro x y z _ _; exact @h z y; + @[simp] lemma WellFounded.trivial_wellfounded : WellFounded (α := α) (λ _ _ => False) := by constructor; intro _;