int

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;
 

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,17 +211,22 @@ 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₂⟩;
     | _ => apply dni'!; simp;
 
 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

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,

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