diff --git a/Foundation/IntProp/ConsistentTableau.lean b/Foundation/IntProp/ConsistentTableau.lean index 0f7a3ddf..64260c63 100644 --- a/Foundation/IntProp/ConsistentTableau.lean +++ b/Foundation/IntProp/ConsistentTableau.lean @@ -183,7 +183,7 @@ end Saturated variable [Λ.IncludeEFQ] -lemma self_consistent [h : System.Consistent Λ] : Tableau.Consistent Λ (Ax(Λ), ∅) := by +lemma self_consistent [h : System.Consistent Λ] : Tableau.Consistent Λ (Λ.axioms, ∅) := by intro Γ Δ hΓ hΔ; replace hΔ : Δ = [] := List.nil_iff.mpr hΔ; obtain ⟨ψ, hq⟩ := h.exists_unprovable; @@ -193,7 +193,8 @@ lemma self_consistent [h : System.Consistent Λ] : Tableau.Consistent Λ (Ax(Λ) simp at hC; exact imp_trans''! hC efq! ⨀ (by apply iff_provable_list_conj.mpr; - exact λ _ hp => ⟨Deduction.eaxm $ hΓ _ hp⟩; + intro φ hφ; + exact Hilbert.Deduction.eaxm! $ hΓ _ hφ; ); contradiction; diff --git a/Foundation/IntProp/Deduction.lean b/Foundation/IntProp/Deduction.lean index 7fbf858c..e1a75c8c 100644 --- a/Foundation/IntProp/Deduction.lean +++ b/Foundation/IntProp/Deduction.lean @@ -7,24 +7,29 @@ namespace LO.IntProp variable {α : Type u} structure Hilbert (α) where - axiomSet : Theory α -notation "Ax(" Λ ")" => Hilbert.axiomSet Λ + axioms : Theory α namespace Hilbert +variable {Λ : Hilbert α} + + +section + class IncludeEFQ (Λ : Hilbert α) where - include_EFQ : 𝗘𝗙𝗤 ⊆ Ax(Λ) := by simp + include_EFQ : 𝗘𝗙𝗤 ⊆ Λ.axioms := by simp class IncludeLEM (Λ : Hilbert α) where - include_LEM : 𝗟𝗘𝗠 ⊆ Ax(Λ) := by simp + include_LEM : 𝗟𝗘𝗠 ⊆ Λ.axioms := by simp class IncludeDNE (Λ : Hilbert α) where - include_DNE : 𝗗𝗡𝗘 ⊆ Ax(Λ) := by simp + include_DNE : 𝗗𝗡𝗘 ⊆ Λ.axioms := by simp + +end -end Hilbert inductive Deduction (Λ : Hilbert α) : Formula α → Type _ - | eaxm {φ} : φ ∈ Ax(Λ) → Deduction Λ φ + | eaxm {φ} : φ ∈ Λ.axioms → Deduction Λ φ | mdp {φ ψ} : Deduction Λ (φ ➝ ψ) → Deduction Λ φ → Deduction Λ ψ | verum : Deduction Λ $ ⊤ | imply₁ φ ψ : Deduction Λ $ φ ➝ ψ ➝ φ @@ -42,7 +47,7 @@ instance : System (Formula α) (Hilbert α) := ⟨Deduction⟩ open Deduction open Hilbert -variable {Λ : Hilbert α} +section instance : System.Minimal Λ where mdp := mdp @@ -72,61 +77,68 @@ instance [Λ.IncludeDNE] : System.Classical Λ where instance [DecidableEq α] [Λ.IncludeEFQ] [Λ.IncludeLEM] : System.Classical Λ where -lemma Deduction.eaxm! {Λ : Hilbert α} {φ : Formula α} (h : φ ∈ Ax(Λ)) : Λ ⊢! φ := ⟨eaxm h⟩ - +end -namespace Hilbert abbrev theorems (Λ : Hilbert α) : Set (Formula α) := System.theory Λ + +section systems + +variable (α) + protected abbrev Minimal : Hilbert α := ⟨∅⟩ -protected abbrev Intuitionistic : Hilbert α := ⟨𝗘𝗙𝗤⟩ -notation "𝐈𝐧𝐭" => Hilbert.Intuitionistic -instance : IncludeEFQ (α := α) 𝐈𝐧𝐭 where -instance : System.Intuitionistic (𝐈𝐧𝐭 : Hilbert α) where +protected abbrev Int : Hilbert α := ⟨𝗘𝗙𝗤⟩ +instance : IncludeEFQ (Hilbert.Int α) where +instance : System.Intuitionistic (Hilbert.Int α) where -protected abbrev Classical : Hilbert α := ⟨𝗘𝗙𝗤 ∪ 𝗟𝗘𝗠⟩ -notation "𝐂𝐥" => Hilbert.Classical -instance : IncludeLEM (α := α) 𝐂𝐥 where -instance : IncludeEFQ (α := α) 𝐂𝐥 where +protected abbrev Cl : Hilbert α := ⟨𝗘𝗙𝗤 ∪ 𝗟𝗘𝗠⟩ +instance : IncludeLEM (α := α) (Hilbert.Cl α) where +instance : IncludeEFQ (α := α) (Hilbert.Cl α) where --- `𝐊𝐂` from chagrov & zakharyaschev (1997) +/-- + `KC` from Chagrov & Zakharyaschev (1997) +-/ protected abbrev KC : Hilbert α := ⟨𝗘𝗙𝗤 ∪ 𝗪𝗟𝗘𝗠⟩ -notation "𝐊𝐂" => Hilbert.KC -instance : IncludeEFQ (α := α) 𝐊𝐂 where -instance : System.HasAxiomWeakLEM (𝐊𝐂 : Hilbert α) where +instance : IncludeEFQ (α := α) (Hilbert.KC α) where +instance : System.HasAxiomWeakLEM (Hilbert.KC α) where wlem φ := by apply eaxm; aesop; --- `𝐋𝐂` from chagrov & zakharyaschev (1997) +/-- + `LC` from Chagrov & Zakharyaschev (1997) +-/ protected abbrev LC : Hilbert α := ⟨𝗘𝗙𝗤 ∪ 𝗗𝘂𝗺⟩ -notation "𝐋𝐂" => Hilbert.LC -instance : IncludeEFQ (α := α) 𝐋𝐂 where -instance : System.HasAxiomDummett (𝐋𝐂 : Hilbert α) where +instance : IncludeEFQ (α := α) (Hilbert.LC α) where +instance : System.HasAxiomDummett (Hilbert.LC α) where dummett φ ψ := by apply eaxm; aesop; -/- MEMO: - Term `WeakMinimal` and `WeakClassical` are from Ariola (2007) - Minimal <ₛ WeakMinimal <ₛ WeakClassical <ₛ Classical --/ +-- MEMO: Minimal <ₛ WeakMinimal <ₛ WeakClassical <ₛ Classical +/-- + `WeakMinimal` from Ariola (2007) +-/ protected abbrev WeakMinimal : Hilbert α := ⟨𝗟𝗘𝗠⟩ + +/-- + `WeakClassical` from Ariola (2007) +-/ protected abbrev WeakClassical : Hilbert α := ⟨𝗣𝗲⟩ +end systems -end Hilbert namespace Deduction -variable {Λ : Hilbert α} - open System +lemma eaxm! {Λ : Hilbert α} {φ : Formula α} (h : φ ∈ Λ.axioms) : Λ ⊢! φ := ⟨eaxm h⟩ + noncomputable def rec! {α : Type u} {Λ : Hilbert α} {motive : (a : Formula α) → Λ ⊢! a → Sort u_1} - (eaxm : ∀ {φ}, (a : φ ∈ Ax(Λ)) → motive φ ⟨eaxm a⟩) + (eaxm : ∀ {φ}, (a : φ ∈ Λ.axioms) → motive φ ⟨eaxm a⟩) (mdp : ∀ {φ ψ}, {hpq : Λ ⊢! (φ ➝ ψ)} → {hp : Λ ⊢! φ} → motive (φ ➝ ψ) hpq → motive φ hp → motive ψ (hpq ⨀ hp)) (verum : motive ⊤ verum!) (imply₁ : ∀ {φ ψ}, motive (φ ➝ ψ ➝ φ) imply₁!) @@ -150,9 +162,9 @@ end Deduction open System -variable {Λ₁ Λ₂ : Hilbert α} +section -lemma weaker_than_of_subset_axiomset' (hMaxm : ∀ {φ : Formula α}, φ ∈ Ax(Λ₁) → Λ₂ ⊢! φ) +lemma weaker_than_of_subset_axiomset' {Λ₁ Λ₂ : Hilbert α} (hMaxm : ∀ {φ : Formula α}, φ ∈ Λ₁.axioms → Λ₂ ⊢! φ) : Λ₁ ≤ₛ Λ₂ := by apply System.weakerThan_iff.mpr; intro φ h; @@ -161,30 +173,30 @@ lemma weaker_than_of_subset_axiomset' (hMaxm : ∀ {φ : Formula α}, φ ∈ Ax( | mdp ihpq ihp => exact ihpq ⨀ ihp; | _ => simp; -lemma weaker_than_of_subset_axiomset (hSubset : Ax(Λ₁) ⊆ Ax(Λ₂) := by aesop) : Λ₁ ≤ₛ Λ₂ := by +lemma weaker_than_of_subset_axiomset {Λ₁ Λ₂ : Hilbert α} (hSubset : Λ₁.axioms ⊆ Λ₂.axioms := by aesop) : Λ₁ ≤ₛ Λ₂ := by apply weaker_than_of_subset_axiomset'; intro φ hp; apply eaxm! $ hSubset hp; -lemma Int_weaker_than_Cl : (𝐈𝐧𝐭 : Hilbert α) ≤ₛ 𝐂𝐥 := weaker_than_of_subset_axiomset +lemma Int_weaker_than_Cl : (Hilbert.Int α) ≤ₛ (Hilbert.Cl α) := weaker_than_of_subset_axiomset -lemma Int_weaker_than_KC : (𝐈𝐧𝐭 : Hilbert α) ≤ₛ 𝐊𝐂 := weaker_than_of_subset_axiomset +lemma Int_weaker_than_KC : (Hilbert.Int α) ≤ₛ (Hilbert.KC α) := weaker_than_of_subset_axiomset -lemma Int_weaker_than_LC : (𝐈𝐧𝐭 : Hilbert α) ≤ₛ 𝐋𝐂 := weaker_than_of_subset_axiomset +lemma Int_weaker_than_LC : (Hilbert.Int α) ≤ₛ (Hilbert.LC α) := weaker_than_of_subset_axiomset -lemma KC_weaker_than_Cl : (𝐊𝐂 : Hilbert α) ≤ₛ 𝐂𝐥 := by - apply weaker_than_of_subset_axiomset'; - intro φ hp; - rcases hp with (⟨_, rfl⟩ | ⟨_, rfl⟩) <;> simp; +lemma KC_weaker_than_Cl : (Hilbert.KC α) ≤ₛ (Hilbert.Cl α) := weaker_than_of_subset_axiomset' $ by + rintro φ (⟨_, rfl⟩ | ⟨_, rfl⟩) <;> simp; -lemma LC_weaker_than_Cl [DecidableEq α] : (𝐋𝐂 : Hilbert α) ≤ₛ 𝐂𝐥 := by +lemma LC_weaker_than_Cl [DecidableEq α] : (Hilbert.LC α) ≤ₛ (Hilbert.Cl α) := by apply weaker_than_of_subset_axiomset'; - intro φ hp; - rcases hp with (⟨_, rfl⟩ | ⟨_, _, rfl⟩) <;> simp; + rintro φ (⟨_, rfl⟩ | ⟨_, _, rfl⟩) <;> simp; + +end -variable {φ : Formula α} -theorem iff_provable_dn_efq_dne_provable [DecidableEq α] : 𝐈𝐧𝐭 ⊢! ∼∼φ ↔ 𝐂𝐥 ⊢! φ := by +section Glivenko + +theorem iff_provable_dn_efq_dne_provable [DecidableEq α] : (Hilbert.Int α) ⊢! ∼∼φ ↔ (Hilbert.Cl α) ⊢! φ := by constructor; . intro d; exact dne'! $ Int_weaker_than_Cl d; . intro d; @@ -199,7 +211,7 @@ theorem iff_provable_dn_efq_dne_provable [DecidableEq α] : 𝐈𝐧𝐭 ⊢! subst hq; apply neg_equiv'!.mpr; apply FiniteContext.deduct'!; - have : [∼(ψ ⋎ ∼ψ)] ⊢[𝐈𝐧𝐭]! ∼ψ ⋏ ∼∼ψ := demorgan₃'! $ FiniteContext.id!; + have : [∼(ψ ⋎ ∼ψ)] ⊢[Hilbert.Int α]! ∼ψ ⋏ ∼∼ψ := demorgan₃'! $ FiniteContext.id!; exact neg_mdp! (and₂'! this) (and₁'! this); | @mdp φ ψ h₁ h₂ ih₁ ih₂ => exact (dn_distribute_imply'! $ ih₁ ⟨h₁⟩) ⨀ ih₂ ⟨h₂⟩; @@ -207,9 +219,14 @@ theorem iff_provable_dn_efq_dne_provable [DecidableEq α] : 𝐈𝐧𝐭 ⊢! alias glivenko := iff_provable_dn_efq_dne_provable -theorem iff_provable_neg_efq_provable_neg_efq [DecidableEq α] : 𝐈𝐧𝐭 ⊢! ∼φ ↔ 𝐂𝐥 ⊢! ∼φ := by +theorem iff_provable_neg_efq_provable_neg_efq [DecidableEq α] : (Hilbert.Int α) ⊢! ∼φ ↔ (Hilbert.Cl α) ⊢! ∼φ := by constructor; . intro d; exact glivenko.mp $ dni'! d; . intro d; exact tne'! $ glivenko.mpr d; +end Glivenko + + +end Hilbert + end LO.IntProp diff --git a/Foundation/IntProp/Kripke/Completeness.lean b/Foundation/IntProp/Kripke/Completeness.lean index f34f5d70..99953ab5 100644 --- a/Foundation/IntProp/Kripke/Completeness.lean +++ b/Foundation/IntProp/Kripke/Completeness.lean @@ -13,7 +13,6 @@ open Kripke namespace Kripke --- variable [Inhabited α] [DecidableEq α] [Encodable α] [Λ.IncludeEFQ] variable {α : Type u} {Λ : Hilbert α} @@ -316,20 +315,20 @@ lemma complete (H : CanonicalFrame Λ ∈ 𝔽) {φ : Formula α} : 𝔽#α ⊧ instance instComplete (H : CanonicalFrame Λ ∈ 𝔽) : Complete Λ (𝔽#α) := ⟨complete H⟩ -instance Int_complete : Complete 𝐈𝐧𝐭 (Kripke.ReflexiveTransitiveFrameClass.{u}#α) := instComplete $ by +instance Int_complete : Complete (Hilbert.Int α) (Kripke.ReflexiveTransitiveFrameClass.{u}#α) := instComplete $ by refine ⟨ CanonicalFrame.reflexive, CanonicalFrame.transitive, ⟩ -instance LC_complete : Complete 𝐋𝐂 (Kripke.ReflexiveTransitiveConnectedFrameClass.{u}#α) := instComplete $ by +instance LC_complete : Complete (Hilbert.LC α) (Kripke.ReflexiveTransitiveConnectedFrameClass.{u}#α) := instComplete $ by refine ⟨ CanonicalFrame.reflexive, CanonicalFrame.transitive, CanonicalFrame.connected ⟩; -instance KC_complete : Complete 𝐊𝐂 (Kripke.ReflexiveTransitiveConfluentFrameClass.{u}#α) := instComplete $ by +instance KC_complete : Complete (Hilbert.KC α) (Kripke.ReflexiveTransitiveConfluentFrameClass.{u}#α) := instComplete $ by refine ⟨ CanonicalFrame.reflexive, CanonicalFrame.transitive, diff --git a/Foundation/IntProp/Kripke/DP.lean b/Foundation/IntProp/Kripke/DP.lean index 0490b760..5fa284d1 100644 --- a/Foundation/IntProp/Kripke/DP.lean +++ b/Foundation/IntProp/Kripke/DP.lean @@ -110,7 +110,7 @@ lemma satisfies_right_on_IntDPCounterexampleModel : exact ihq.mpr $ h (by simpa) $ ihp.mp hp; | _ => simp_all [IntDPCounterexampleModel, Satisfies.iff_models, Satisfies]; -theorem disjunctive_int [Inhabited α] [DecidableEq α] [Encodable α] : 𝐈𝐧𝐭 ⊢! φ ⋎ ψ → 𝐈𝐧𝐭 ⊢! φ ∨ 𝐈𝐧𝐭 ⊢! ψ := by +theorem disjunctive_int [Inhabited α] [DecidableEq α] [Encodable α] : (Hilbert.Int α) ⊢! φ ⋎ ψ → (Hilbert.Int α) ⊢! φ ∨ (Hilbert.Int α) ⊢! ψ := by contrapose; intro hC; push_neg at hC; have ⟨hnp, hnq⟩ := hC; @@ -140,7 +140,7 @@ theorem disjunctive_int [Inhabited α] [DecidableEq α] [Encodable α] : 𝐈 (w := Sum.inl ()) (w' := Sum.inr $ Sum.inr wq) (by aesop)) $ satisfies_right_on_IntDPCounterexampleModel |>.not.mp hq; -instance [DecidableEq α] [Inhabited α] [Encodable α] : Disjunctive (𝐈𝐧𝐭 : Hilbert α) := ⟨disjunctive_int⟩ +instance [DecidableEq α] [Inhabited α] [Encodable α] : Disjunctive (Hilbert.Int α) := ⟨disjunctive_int⟩ end Kripke diff --git a/Foundation/IntProp/Kripke/LEM.lean b/Foundation/IntProp/Kripke/LEM.lean index 04d5189d..f75fd787 100644 --- a/Foundation/IntProp/Kripke/LEM.lean +++ b/Foundation/IntProp/Kripke/LEM.lean @@ -7,12 +7,12 @@ import Foundation.IntProp.Kripke.Semantics - `noLEM`: LEM is not always valid in intuitionistic logic. -/ -namespace LO.IntProp.Kripke +namespace LO.IntProp open System - open Formula Formula.Kripke + variable {α : Type u} abbrev NoLEMFrame : Kripke.Frame where @@ -24,32 +24,38 @@ abbrev NoLEMFrame : Kripke.Frame where | .inl _, .inr _ => True | _, _ => False -lemma NoLEMFrame.transitive : Transitive NoLEMFrame.Rel := by simp [Transitive]; +namespace NoLEMFrame + +lemma is_transitive : Transitive NoLEMFrame.Rel := by simp [Transitive]; + +lemma is_reflexive : Reflexive NoLEMFrame.Rel := by simp [Reflexive]; -lemma NoLEMFrame.reflexive : Reflexive NoLEMFrame.Rel := by simp [Reflexive]; +lemma is_confluent : Confluent NoLEMFrame.Rel := by simp [Confluent]; -lemma NoLEMFrame.confluent : Confluent NoLEMFrame.Rel := by simp [Confluent]; +lemma is_connected : Connected NoLEMFrame.Rel := by simp [Connected]; -lemma NoLEMFrame.connected : Connected NoLEMFrame.Rel := by simp [Connected]; +end NoLEMFrame -lemma noLEM_on_frameclass [Inhabited α] : ∃ (φ : Formula α), ¬((Kripke.FrameClassOfHilbert.{u, 0} 𝐈𝐧𝐭) ⊧ φ ⋎ ∼φ) := by + +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.reflexive, NoLEMFrame.transitive⟩; + exact ⟨NoLEMFrame.is_reflexive, NoLEMFrame.is_transitive⟩; . simp [ValidOnFrame]; use (λ w _ => match w with | .inr _ => True | .inl _ => False); constructor; . simp; . simp [ValidOnModel, Satisfies]; + /-- Law of Excluded Middle is not always provable in intuitionistic logic. -/ -theorem noLEM [Inhabited α] : ∃ (φ : Formula α), 𝐈𝐧𝐭 ⊬ φ ⋎ ∼φ := by - obtain ⟨φ, hp⟩ := noLEM_on_frameclass (α := α); +theorem Hilbert.Int.noLEM [Inhabited α] : ∃ (φ : Formula α), (Hilbert.Int α) ⊬ φ ⋎ ∼φ := by + obtain ⟨φ, hp⟩ := Kripke.noLEM_on_frameclass (α := α); use φ; by_contra hC; have := @Kripke.sound _ _ _ hC; @@ -58,47 +64,46 @@ theorem noLEM [Inhabited α] : ∃ (φ : Formula α), 𝐈𝐧𝐭 ⊬ φ ⋎ /-- Intuitionistic logic is proper weaker than classical logic. -/ -theorem Int_strictly_weaker_than_Cl [DecidableEq α] [Inhabited α] : (𝐈𝐧𝐭 : Hilbert α) <ₛ 𝐂𝐥 := by +theorem Hilbert.Int_strictly_weaker_than_Cl [DecidableEq α] [Inhabited α] : (Hilbert.Int α) <ₛ (Hilbert.Cl α) := by constructor; - . exact Int_weaker_than_Cl; + . exact Hilbert.Int_weaker_than_Cl; . apply weakerThan_iff.not.mpr; push_neg; - obtain ⟨φ, hp⟩ := noLEM (α := α); + obtain ⟨φ, hp⟩ := Hilbert.Int.noLEM (α := α); use (φ ⋎ ∼φ); constructor; . exact lem!; . assumption; - section -lemma noLEM_on_frameclass_KC [DecidableEq α] [Inhabited α] : ∃ (φ : Formula α), ¬((Kripke.FrameClassOfHilbert.{u, 0} 𝐊𝐂) ⊧ φ ⋎ ∼φ) := by +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 KC_Characteraizable.characterize; - exact ⟨NoLEMFrame.reflexive, NoLEMFrame.transitive, NoLEMFrame.confluent⟩; + . 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); constructor; . simp; . simp [ValidOnModel, Satisfies]; -lemma noLEM_KC [DecidableEq α] [Inhabited α] : ∃ (φ : Formula α), 𝐊𝐂 ⊬ φ ⋎ ∼φ := by - obtain ⟨φ, hp⟩ := noLEM_on_frameclass_KC (α := α); +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; contradiction; -theorem KC_strictly_weaker_than_Cl [DecidableEq α] [Inhabited α] : (𝐊𝐂 : Hilbert α) <ₛ 𝐂𝐥 := by +theorem Hilbert.KC_strictly_weaker_than_Cl [DecidableEq α] [Inhabited α] : (Hilbert.KC α) <ₛ (Hilbert.Cl α) := by constructor; - . exact KC_weaker_than_Cl; + . exact Hilbert.KC_weaker_than_Cl; . apply weakerThan_iff.not.mpr; push_neg; - obtain ⟨φ, hp⟩ := noLEM_KC (α := α); + obtain ⟨φ, hp⟩ := Hilbert.KC.noLEM (α := α); use (φ ⋎ ∼φ); constructor; . exact lem!; @@ -109,32 +114,32 @@ end section -lemma noLEM_on_frameclass_LC [Inhabited α] : ∃ (φ : Formula α), ¬((Kripke.FrameClassOfHilbert.{u, 0} 𝐋𝐂) ⊧ φ ⋎ ∼φ) := by +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.reflexive, NoLEMFrame.transitive, NoLEMFrame.connected⟩; + 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 noLEM_LC [Inhabited α] : ∃ (φ : Formula α), 𝐋𝐂 ⊬ φ ⋎ ∼φ := by - obtain ⟨φ, hp⟩ := noLEM_on_frameclass_LC (α := α); +lemma Hilbert.LC.noLEM [Inhabited α] : ∃ (φ : Formula α), (Hilbert.LC α) ⊬ φ ⋎ ∼φ := by + obtain ⟨φ, hp⟩ := Kripke.noLEM_on_frameclass_LC (α := α); use φ; by_contra hC; have := @Kripke.sound _ _ _ hC; contradiction; -theorem LC_strictly_weaker_than_Cl [DecidableEq α] [Inhabited α] : (𝐋𝐂 : Hilbert α) <ₛ 𝐂𝐥 := by +theorem Hilbert.LC_strictly_weaker_than_Cl [DecidableEq α] [Inhabited α] : (Hilbert.LC α) <ₛ (Hilbert.Cl α) := by constructor; - . exact LC_weaker_than_Cl; + . exact Hilbert.LC_weaker_than_Cl; . apply weakerThan_iff.not.mpr; push_neg; - obtain ⟨φ, hp⟩ := noLEM_LC (α := α); + obtain ⟨φ, hp⟩ := Hilbert.LC.noLEM (α := α); use (φ ⋎ ∼φ); constructor; . exact lem!; @@ -142,5 +147,4 @@ theorem LC_strictly_weaker_than_Cl [DecidableEq α] [Inhabited α] : (𝐋𝐂 : end - -end LO.IntProp.Kripke +end LO.IntProp diff --git a/Foundation/IntProp/Kripke/Semantics.lean b/Foundation/IntProp/Kripke/Semantics.lean index ae5bb33f..bea7a606 100644 --- a/Foundation/IntProp/Kripke/Semantics.lean +++ b/Foundation/IntProp/Kripke/Semantics.lean @@ -309,11 +309,11 @@ section variable {α : Type u} -instance Int_Characteraizable : 𝔽((𝐈𝐧𝐭 : Hilbert α)).Characteraizable ReflexiveTransitiveFrameClass where +instance Int_Characteraizable : 𝔽((Hilbert.Int α)).Characteraizable ReflexiveTransitiveFrameClass where characterize := by simp [System.theory]; rintro F hTrans hRefl φ hp; - induction hp using Deduction.rec! with + induction hp using Hilbert.Deduction.rec! with | verum => apply ValidOnFrame.verum; | imply₁ => apply ValidOnFrame.imply₁; simpa; | imply₂ => apply ValidOnFrame.imply₂; simpa; simpa; @@ -335,16 +335,16 @@ instance Int_Characteraizable : 𝔽((𝐈𝐧𝐭 : Hilbert α)).Characteraizab refine ⟨by simp [Reflexive], by simp [Transitive]⟩; -instance Int_sound : Sound 𝐈𝐧𝐭 (ReflexiveTransitiveFrameClass#α) := inferInstance +instance Int_sound : Sound (Hilbert.Int α) (ReflexiveTransitiveFrameClass#α) := inferInstance -instance : System.Consistent (𝐈𝐧𝐭 : Hilbert α) := inferInstance +instance : System.Consistent (Hilbert.Int α) := inferInstance -instance Cl_Characteraizable : 𝔽((𝐂𝐥 : Hilbert α)).Characteraizable ReflexiveTransitiveSymmetricFrameClass#α where +instance Cl_Characteraizable : 𝔽(Hilbert.Cl α).Characteraizable ReflexiveTransitiveSymmetricFrameClass#α where characterize := by simp [System.theory]; rintro F hTrans hRefl hSymm φ hp; - induction hp using Deduction.rec! with + induction hp using Hilbert.Deduction.rec! with | verum => apply ValidOnFrame.verum; | imply₁ => apply ValidOnFrame.imply₁; simpa; | imply₂ => apply ValidOnFrame.imply₂; simpa; simpa; @@ -366,18 +366,18 @@ instance Cl_Characteraizable : 𝔽((𝐂𝐥 : Hilbert α)).Characteraizable Re use { World := PUnit, Rel := λ _ _ => True }; refine ⟨by simp [Reflexive], by simp [Transitive], by simp [Symmetric]⟩; -instance : Sound 𝐂𝐥 (ReflexiveTransitiveSymmetricFrameClass#α) := inferInstance +instance : Sound (Hilbert.Cl α) (ReflexiveTransitiveSymmetricFrameClass#α) := inferInstance -instance : System.Consistent (𝐂𝐥 : Hilbert α) := inferInstance +instance : System.Consistent (Hilbert.Cl α) := inferInstance -instance KC_Characteraizable : 𝔽((𝐊𝐂 : Hilbert α)).Characteraizable ReflexiveTransitiveConfluentFrameClass where +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 Deduction.rec! with + induction hp using Hilbert.Deduction.rec! with | verum => apply ValidOnFrame.verum; | imply₁ => apply ValidOnFrame.imply₁; simpa; | imply₂ => apply ValidOnFrame.imply₂; simpa; simpa; @@ -399,17 +399,17 @@ instance KC_Characteraizable : 𝔽((𝐊𝐂 : Hilbert α)).Characteraizable Re use { World := PUnit, Rel := λ _ _ => True }; refine ⟨by simp [Reflexive], by simp [Transitive], by simp [Confluent]⟩; -instance : Sound 𝐊𝐂 (ReflexiveTransitiveConfluentFrameClass#α) := inferInstance +instance : Sound (Hilbert.KC α) (ReflexiveTransitiveConfluentFrameClass#α) := inferInstance -instance : System.Consistent (𝐊𝐂 : Hilbert α) := inferInstance +instance : System.Consistent (Hilbert.KC α) := inferInstance -instance LC_Characteraizable : 𝔽((𝐋𝐂 : Hilbert α)).Characteraizable ReflexiveTransitiveConnectedFrameClass where +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 Deduction.rec! with + induction hp using Hilbert.Deduction.rec! with | verum => apply ValidOnFrame.verum; | imply₁ => apply ValidOnFrame.imply₁; simpa; | imply₂ => apply ValidOnFrame.imply₂; simpa; simpa; @@ -431,9 +431,9 @@ instance LC_Characteraizable : 𝔽((𝐋𝐂 : Hilbert α)).Characteraizable Re use { World := PUnit, Rel := λ _ _ => True }; refine ⟨by simp [Reflexive], by simp [Transitive], by simp [Connected]⟩; -instance : Sound 𝐋𝐂 (ReflexiveTransitiveConnectedFrameClass#α) := inferInstance +instance : Sound (Hilbert.LC α) (ReflexiveTransitiveConnectedFrameClass#α) := inferInstance -instance : System.Consistent (𝐋𝐂 : Hilbert α) := inferInstance +instance : System.Consistent (Hilbert.LC α) := inferInstance end @@ -473,18 +473,18 @@ namespace Kripke open Formula.Kripke (ClassicalSatisfies) -lemma ValidOnClassicalFrame_iff : (Kripke.FrameClassOfHilbert.{u, 0} 𝐂𝐥) ⊧ φ → ∀ (V : ClassicalValuation α), V ⊧ φ := by +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} 𝐂𝐥) ⊧ φ := by +lemma notClassicalValid_of_exists_ClassicalValuation : (∃ (V : ClassicalValuation α), ¬(V ⊧ φ)) → ¬(Kripke.FrameClassOfHilbert.{u, 0} (Hilbert.Cl α)) ⊧ φ := by contrapose; push_neg; have := @ValidOnClassicalFrame_iff α φ; exact this; -lemma unprovable_classical_of_exists_ClassicalValuation (h : ∃ (V : ClassicalValuation α), ¬(V ⊧ φ)) : 𝐂𝐥 ⊬ φ := by +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; diff --git a/Foundation/Modal/Maximal.lean b/Foundation/Modal/Maximal.lean index 8b60071e..31618427 100644 --- a/Foundation/Modal/Maximal.lean +++ b/Foundation/Modal/Maximal.lean @@ -124,7 +124,7 @@ lemma deducible_iff_verTranslation : (Hilbert.Ver α) ⊢! φ ⭤ φⱽ := by | himp _ _ ih₁ ih₂ => exact imp_replace_iff! ih₁ ih₂; | _ => apply iff_id! -lemma of_classical {mΛ : Modal.Hilbert α} {φ : IntProp.Formula α} : (𝐂𝐥 ⊢! φ) → (mΛ ⊢! φᴹ) := by +lemma of_classical {mΛ : Modal.Hilbert α} {φ : IntProp.Formula α} : ((Hilbert.Cl α) ⊢! φ) → (mΛ ⊢! φᴹ) := by intro h; induction h.some with | eaxm ih => @@ -137,7 +137,7 @@ lemma of_classical {mΛ : Modal.Hilbert α} {φ : IntProp.Formula α} : (𝐂 exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩); | _ => dsimp [IntProp.Formula.toModalFormula]; trivial; -lemma iff_Triv_classical : Hilbert.Triv α ⊢! φ ↔ 𝐂𝐥 ⊢! φᵀᴾ := by +lemma iff_Triv_classical : Hilbert.Triv α ⊢! φ ↔ (Hilbert.Cl α) ⊢! φᵀᴾ := by constructor; . intro h; induction h using Deduction.inducition_with_necOnly! with @@ -154,7 +154,7 @@ lemma iff_Triv_classical : Hilbert.Triv α ⊢! φ ↔ 𝐂𝐥 ⊢! φᵀᴾ := have d₂ : Hilbert.Triv α ⊢! φᵀ := by simpa only [TrivTranslation.back] using of_classical h; exact d₁ ⨀ d₂; -lemma iff_Ver_classical : (Hilbert.Ver α) ⊢! φ ↔ 𝐂𝐥 ⊢! φⱽᴾ := by +lemma iff_Ver_classical : (Hilbert.Ver α) ⊢! φ ↔ (Hilbert.Cl α) ⊢! φⱽᴾ := by constructor; . intro h; induction h using Deduction.inducition_with_necOnly! with @@ -171,13 +171,13 @@ lemma iff_Ver_classical : (Hilbert.Ver α) ⊢! φ ↔ 𝐂𝐥 ⊢! φⱽᴾ := have d₂ : (Hilbert.Ver α) ⊢! φⱽ := by simpa using of_classical h; exact d₁ ⨀ d₂; -lemma trivTranslated_of_K4 : (Hilbert.K4 α) ⊢! φ → 𝐂𝐥 ⊢! φᵀᴾ := by +lemma trivTranslated_of_K4 : (Hilbert.K4 α) ⊢! φ → (Hilbert.Cl α) ⊢! φᵀᴾ := by intro h; apply iff_Triv_classical.mp; exact System.weakerThan_iff.mp Hilbert.K4_weakerThan_Triv h; -lemma verTranslated_of_GL : (Hilbert.GL α) ⊢! φ → 𝐂𝐥 ⊢! φⱽᴾ := by +lemma verTranslated_of_GL : (Hilbert.GL α) ⊢! φ → (Hilbert.Cl α) ⊢! φⱽᴾ := by intro h; induction h using Deduction.inducition_with_necOnly! with | hMaxm a => diff --git a/Foundation/Modal/ModalCompanion/Basic.lean b/Foundation/Modal/ModalCompanion/Basic.lean index 26003025..a63bc963 100644 --- a/Foundation/Modal/ModalCompanion/Basic.lean +++ b/Foundation/Modal/ModalCompanion/Basic.lean @@ -73,7 +73,7 @@ private lemma provable_efq_of_provable_S4.case_neg_equiv [System.K4 mΛ] : mΛ instance [System.S4 mΛ] : System.K4 mΛ where open provable_efq_of_provable_S4 in -lemma provable_efq_of_provable_S4 [DecidableEq α] (h : 𝐈𝐧𝐭 ⊢! φ) : (Hilbert.S4 α) ⊢! φᵍ := by +lemma provable_efq_of_provable_S4 [DecidableEq α] (h : (Hilbert.Int α) ⊢! φ) : (Hilbert.S4 α) ⊢! φᵍ := by induction h.some with | eaxm ih => simp_all only [Set.mem_setOf_eq]; diff --git a/Foundation/Modal/ModalCompanion/GMT.lean b/Foundation/Modal/ModalCompanion/GMT.lean index 00a5f4b4..e49ee1aa 100644 --- a/Foundation/Modal/ModalCompanion/GMT.lean +++ b/Foundation/Modal/ModalCompanion/GMT.lean @@ -4,6 +4,7 @@ import Foundation.Modal.ModalCompanion.Basic namespace LO.Modal +open IntProp open LO.Kripke open Modal.Kripke @@ -12,7 +13,7 @@ variable {α : Type u} [DecidableEq α] [Inhabited α] [Encodable α] variable {iΛ : IntProp.Hilbert α} {mΛ : Modal.Hilbert α} variable {φ ψ χ : IntProp.Formula α} -lemma provable_S4_of_provable_efq : ((Hilbert.S4 α) ⊢! φᵍ) → (𝐈𝐧𝐭 ⊢! φ) := by +lemma provable_S4_of_provable_efq : ((Hilbert.S4 α) ⊢! φᵍ) → ((Hilbert.Int α) ⊢! φ) := by contrapose; intro h; @@ -49,7 +50,7 @@ lemma provable_S4_of_provable_efq : ((Hilbert.S4 α) ⊢! φᵍ) → (𝐈𝐧 use F; exact ⟨⟨F_refl, F_trans⟩, by use V, w⟩; -theorem provable_efq_iff_provable_S4 : 𝐈𝐧𝐭 ⊢! φ ↔ (Hilbert.S4 α) ⊢! φᵍ := ⟨provable_efq_of_provable_S4, provable_S4_of_provable_efq⟩ -instance : ModalCompanion (α := α) 𝐈𝐧𝐭 (Hilbert.S4 α) := ⟨provable_efq_iff_provable_S4⟩ +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