feat(Modal): Strong completeness of Geach logics (iehality#34)

* Geach axiom definability * framedefinability * wip * fix * fix * fix * wip * fix morphism * completeness lemmata wip * `multiframe_box` wip * `defAxiomGeach` * wip * refactor deduction & aesop automation * refactor * fix * feat(Deduction): prove `finset_conj_iff!` * `finset_dt!` * change definition of box for sets * lemma * finished! * Fix by review * refactor naming * fix --------- Co-authored-by: palalansouki <palalansouki@gmail.com>
FormalMathematicsLab · Apr 13, 2024 · 9ef771e · 9ef771e
1 parent 4eabf3f
commit 9ef771e
Show file tree

Hide file tree

Showing 20 changed files with 2,225 additions and 912 deletions.
diff --git a/Logic/Logic/Deduction.lean b/Logic/Logic/Deduction.lean
diff --git a/Logic/Logic/Init.lean b/Logic/Logic/Init.lean
@@ -0,0 +1,3 @@
+import Aesop
+
+declare_aesop_rule_sets [Deduction]
diff --git a/Logic/Logic/LogicSymbol.lean b/Logic/Logic/LogicSymbol.lean
@@ -211,8 +211,6 @@ attribute [simp] DeMorgan.verum DeMorgan.falsum DeMorgan.and DeMorgan.or DeMorga
 class NegDefinition (F : Type*) [LogicalConnective F] where
   neg {p : F} : ~p = p ⟶ ⊥
 
-attribute [simp] NegDefinition.neg
-
 namespace LogicalConnective
 
 section
@@ -416,6 +414,9 @@ def conj : List α → α
 lemma map_conj [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (l : List α) : f l.conj ↔ ∀ a ∈ l, f a := by
   induction l <;> simp[*]
 
+lemma map_conj_append [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (l₁ l₂ : List α) : f (l₁ ++ l₂).conj ↔ f (l₁.conj ⋏ l₂.conj) := by
+  induction l₁ <;> induction l₂ <;> aesop;
+
 def disj : List α → α
   | []      => ⊥
   | a :: as => a ⋎ as.disj
@@ -427,6 +428,9 @@ def disj : List α → α
 lemma map_disj [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (l : List α) : f l.disj ↔ ∃ a ∈ l, f a := by
   induction l <;> simp[*]
 
+lemma map_disj_append [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (l₁ l₂ : List α) : f (l₁ ++ l₂).disj ↔ f (l₁.disj ⋎ l₂.disj) := by
+  induction l₁ <;> induction l₂ <;> aesop;
+
 end
 
 end List
@@ -435,18 +439,40 @@ namespace Finset
 
 section
 
-variable [LogicalConnective α]
+variable [LogicalConnective α] [DecidableEq α]
 
 noncomputable def conj (s : Finset α) : α := s.toList.conj
 
 lemma map_conj [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (s : Finset α) : f s.conj ↔ ∀ a ∈ s, f a := by
   simpa using List.map_conj f s.toList
 
+lemma map_conj_union [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (s₁ s₂ : Finset α) : f (s₁ ∪ s₂).conj ↔ f (s₁.conj ⋏ s₂.conj) := by
+  simp [map_conj];
+  constructor;
+  . intro h;
+    constructor;
+    . intro a ha;
+      exact h a (Or.inl ha);
+    . intro a ha;
+      exact h a (Or.inr ha);
+  . intro ⟨h₁, h₂⟩ a ha;
+    cases ha <;> simp_all;
+
 noncomputable def disj (s : Finset α) : α := s.toList.disj
 
 lemma map_disj [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (s : Finset α) : f s.disj ↔ ∃ a ∈ s, f a := by
   simpa using List.map_disj f s.toList
 
+lemma map_disj_union [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (s₁ s₂ : Finset α) : f (s₁ ∪ s₂).disj ↔ f (s₁.disj ⋎ s₂.disj) := by
+  simp [map_disj];
+  constructor;
+  . rintro ⟨a, h₁ | h₂, hb⟩;
+    . left; use a;
+    . right; use a;
+  . rintro (⟨a₁, h₁⟩ | ⟨a₂, h₂⟩);
+    . use a₁; simp_all;
+    . use a₂; simp_all;
+
 end
 
 end Finset
diff --git a/Logic/Modal/Normal/Axioms.lean b/Logic/Modal/Normal/Axioms.lean
@@ -40,31 +40,33 @@ section Axioms
 variable {F : Type u} [ModalLogicSymbol F] (p q : F)
 
 /-- a.k.a. Distribution Axiom -/
-def AxiomK := □(p ⟶ q) ⟶ □p ⟶ □q
+abbrev AxiomK := □(p ⟶ q) ⟶ □p ⟶ □q
 
-def AxiomT := □p ⟶ p
+abbrev AxiomT := □p ⟶ p
 
-def AxiomB := p ⟶ □◇p
+abbrev AxiomB := p ⟶ □◇p
 
-def AxiomD := □p ⟶ ◇p
+abbrev AxiomD := □p ⟶ ◇p
 
-def Axiom4 := □p ⟶ □□p
+abbrev Axiom4 := □p ⟶ □□p
 
-def Axiom5 := ◇p ⟶ □◇p
+abbrev Axiom5 := ◇p ⟶ □◇p
 
-def AxiomDot2 := ◇□p ⟶ □◇p
+abbrev AxiomDot2 := ◇□p ⟶ □◇p
 
-def AxiomDot3 := □(□p ⟶ □q) ⋎ □(□q ⟶ □p)
+abbrev AxiomC4 := □□p ⟶ □p
 
-def AxiomGrz := □(□(p ⟶ □p) ⟶ p) ⟶ p
+abbrev AxiomCD := ◇p ⟶ □p
 
-def AxiomM := (□◇p ⟶ ◇□p)
+abbrev AxiomTc := p ⟶ □p
 
-def AxiomCD := ◇p ⟶ □p
+abbrev AxiomDot3 := □(□p ⟶ □q) ⋎ □(□q ⟶ □p)
 
-def AxiomC4 := □□p ⟶ □p
+abbrev AxiomGrz := □(□(p ⟶ □p) ⟶ p) ⟶ p
 
-def AxiomL := □(□p ⟶ p) ⟶ □p
+abbrev AxiomM := (□◇p ⟶ ◇□p)
+
+abbrev AxiomL := □(□p ⟶ p) ⟶ □p
 
 end Axioms
 
@@ -185,7 +187,6 @@ namespace LogicS4
 
 end LogicS4
 
-
 def LogicS4Dot2 : AxiomSet α := 𝐒𝟒 ∪ .𝟐
 notation "𝐒𝟒.𝟐" => LogicS4Dot2