Gentzen axF and axiomK wip

Author: SnO2WMaN

ModalTableau/Gentzen/Basic.lean

@@ -17,6 +17,11 @@ namespace SequentPart
 
 def isFreshLabel (x : Label) (Γ : SequentPart) : Prop := (x ∉ Γ.fmls.map LabelledFormula.label) ∧ (∀ y, (x, y) ∉ Γ.rels) ∧ (∀ y, (y, x) ∉ Γ.rels)
 
+/-
+instance : Decidable (isFreshLabel Γ x) := by
+  simp [isFreshLabel];
+-/
+
 variable {x : Label} {Γ : SequentPart}
 
 lemma not_include_labelledFml_of_isFreshLabel (h : Γ.isFreshLabel x) : ∀ φ, (x ∶ φ) ∉ Γ.fmls := by have := h.1; aesop;
@@ -50,24 +55,26 @@ end Sequent
 
 
 inductive Derivation : Sequent → Type _
-| initA {Γ Δ : SequentPart} {x} {a} : Derivation (⟨insert (x ∶ atom a) Γ.fmls, Γ.rels⟩ ⟹ ⟨insert (x ∶ atom a) Δ.fmls, Δ.rels⟩)
-| bot {Γ Δ : SequentPart} {x} : Derivation (⟨insert (x ∶ ⊥) Γ.fmls, Γ.rels⟩ ⟹ Δ)
+| axA {Γ Δ : SequentPart} {x} {a} : Derivation (⟨(x ∶ atom a) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ ⟨(x ∶ atom a) ::ₘ Δ.fmls, Δ.rels⟩)
+| axBot {Γ Δ : SequentPart} {x} : Derivation (⟨(x ∶ ⊥) ::ₘ  Γ.fmls, Γ.rels⟩ ⟹ Δ)
 | impL {Γ Δ : SequentPart} {x} {φ ψ} :
-    Derivation (Γ ⟹ ⟨insert (x ∶ φ) Δ.fmls, Δ.rels⟩) →
-    Derivation (⟨insert (x ∶ ψ) Γ.fmls, Γ.rels⟩ ⟹ Δ) →
-    Derivation (⟨insert (x ∶ φ ➝ ψ) Γ.fmls, Γ.rels⟩ ⟹ Δ)
+    Derivation (Γ ⟹ ⟨(x ∶ φ) ::ₘ Δ.fmls, Δ.rels⟩) →
+    Derivation (⟨(x ∶ ψ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ) →
+    Derivation (⟨(x ∶ φ ➝ ψ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ)
 | impR {Γ Δ : SequentPart} {x} {φ ψ} :
-    Derivation (⟨insert (x ∶ φ) Γ.fmls, Γ.rels⟩ ⟹ ⟨insert (x ∶ ψ) Δ.fmls, Δ.rels⟩) →
-    Derivation (Γ ⟹ ⟨insert (x ∶ φ ➝ ψ) Δ.fmls, Δ.rels⟩)
+    Derivation (⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ ⟨(x ∶ ψ) ::ₘ Δ.fmls, Δ.rels⟩) →
+    Derivation (Γ ⟹ ⟨(x ∶ φ ➝ ψ) ::ₘ Δ.fmls, Δ.rels⟩)
 | boxL {Γ Δ : SequentPart} {x y} {φ} :
-    Derivation (⟨insert (x ∶ □φ) $ insert (y ∶ φ) Γ.fmls, insert (x, y) Γ.rels⟩ ⟹ Δ) →
-    Derivation (⟨insert (x ∶ □φ) Γ.fmls, insert (x, y) Γ.rels⟩ ⟹ Δ)
+    Derivation (⟨(x ∶ □φ) ::ₘ (y ∶ φ) ::ₘ Γ.fmls, (x, y) ::ₘ Γ.rels⟩ ⟹ Δ) →
+    Derivation (⟨(x ∶ □φ) ::ₘ Γ.fmls, (x, y) ::ₘ Γ.rels⟩ ⟹ Δ)
 | boxR {Γ Δ : SequentPart} {x y} {φ} :
     x ≠ y → Γ.isFreshLabel y → Δ.isFreshLabel y →
-    Derivation (⟨Γ.fmls, insert (x, y) Γ.rels⟩ ⟹ ⟨insert (y ∶ φ) Δ.fmls, Δ.rels⟩) →
-    Derivation (Γ ⟹ ⟨insert (x ∶ □φ) Δ.fmls, Δ.rels⟩)
+    Derivation (⟨Γ.fmls, (x, y) ::ₘ Γ.rels⟩ ⟹ ⟨(y ∶ φ) ::ₘ Δ.fmls, Δ.rels⟩) →
+    Derivation (Γ ⟹ ⟨(x ∶ □φ) ::ₘ Δ.fmls, Δ.rels⟩)
 prefix:70 "⊢ᵍ " => Derivation
 
+export Derivation (axA axBot impL impR boxL boxR)
+
 abbrev Derivable (S : Sequent) : Prop := Nonempty (⊢ᵍ S)
 prefix:70 "⊢ᵍ! " => Derivable
 
@@ -77,10 +84,10 @@ section
 theorem soundness {S : Sequent} : ⊢ᵍ S → ∀ (M : Kripke.Model), ∀ (f : Assignment M), S.Satisfies M f := by
   intro d;
   induction d with
-  | initA =>
+  | axA =>
     rintro M f ⟨hΓ, hX⟩;
     simp_all;
-  | bot =>
+  | axBot =>
     rintro M f ⟨hΓ, hX⟩;
     simp at hΓ;
   | @impL Γ Δ x φ ψ d₁ d₂ ih₁ ih₂ =>
@@ -197,12 +204,42 @@ theorem soundness {S : Sequent} : ⊢ᵍ S → ∀ (M : Kripke.Model), ∀ (f :
       have : ¬(f a) ≺ (f b) := hΔ₁ a b h₁;
       contradiction;
 
-theorem soundness_fml : ⊢ᵍ! ⟨⟨{}, {}⟩, ⟨{default ∶ φ}, {}⟩⟩ → ∀ (M : Kripke.Model), ∀ (f : Assignment M), f default ⊧ φ := by
+theorem soundness_fml : ⊢ᵍ! ⟨⟨∅, ∅⟩, ⟨{0 ∶ φ}, ∅⟩⟩ → ∀ (M : Kripke.Model), ∀ (f : Assignment M), f 0 ⊧ φ := by
   rintro ⟨d⟩ M f;
   simpa [Sequent.Satisfies] using soundness d M f
 
 end
 
+def axF {Γ Δ : SequentPart} {x} {φ} : ⊢ᵍ (⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ ⟨(x ∶ φ) ::ₘ Δ.fmls, Δ.rels⟩) := by
+  induction φ using Formula.rec' generalizing Γ Δ x with
+  | hatom a => exact axA
+  | hfalsum => exact axBot
+  | himp φ ψ ihφ ihψ =>
+    apply impR;
+    simpa [Multiset.cons_swap] using impL ihφ ihψ;
+  | hbox φ ih =>
+    letI y := x + 1;
+    apply boxR (y := y) (by simp [y]) (by sorry) (by sorry);
+    apply boxL;
+    simpa [Multiset.cons_swap] using ih (Γ := ⟨(x ∶ □φ) ::ₘ Γ.fmls, _ ::ₘ Γ.rels⟩);
+
+def axiomK : ⊢ᵍ ⟨⟨∅, ∅⟩, ⟨{0 ∶ □(φ ➝ ψ) ➝ □φ ➝ □ψ}, ∅⟩⟩ := by
+  apply impR (Δ := ⟨_, _⟩);
+  apply impR;
+  apply boxR (y := 1) (by simp) (by simp [SequentPart.isFreshLabel]) (by simp [SequentPart.isFreshLabel]);
+  suffices ⊢ᵍ (⟨(0 ∶ □φ) ::ₘ {0 ∶ □(φ ➝ ψ)}, {(0, 1)}⟩ ⟹ ⟨{1 ∶ ψ}, ∅⟩) by simpa;
+  apply boxL (Γ := ⟨_, _⟩);
+  suffices ⊢ᵍ (⟨(0 ∶ □(φ ➝ ψ)) ::ₘ (1 ∶ φ) ::ₘ {(0 ∶ □φ)}, {(0, 1)}⟩ ⟹ ⟨{1 ∶ ψ}, ∅⟩) by
+    have e : (0 ∶ □(φ ➝ ψ)) ::ₘ (1 ∶ φ) ::ₘ {0 ∶ □φ} = (0 ∶ □φ) ::ₘ (1 ∶ φ) ::ₘ {0 ∶ □(φ ➝ ψ)} := by sorry;
+    simpa [e];
+  apply boxL (x := 0) (φ := φ ➝ ψ) (Γ := ⟨{1 ∶ φ, 0 ∶ □φ}, _⟩);
+  suffices ⊢ᵍ (⟨(1 ∶ φ ➝ ψ) ::ₘ {1 ∶ φ, 0 ∶ □φ, 0 ∶ □(φ ➝ ψ)}, {(0, 1)}⟩ ⟹ ⟨{1 ∶ ψ}, ∅⟩) by
+    have e : (0 ∶ □(φ ➝ ψ)) ::ₘ (1 ∶ φ ➝ ψ) ::ₘ (1 ∶ φ) ::ₘ {0 ∶ □φ} = (1 ∶ φ ➝ ψ) ::ₘ {1 ∶ φ, 0 ∶ □φ, 0 ∶ □(φ ➝ ψ)} := by sorry;
+    simpa [e];
+  apply impL (Γ := ⟨_, _⟩);
+  . simpa using axF (Γ := ⟨_, _⟩) (Δ := ⟨_, _⟩);
+  . simpa using axF (Γ := ⟨_, _⟩) (Δ := ⟨_, _⟩);
+
 end Gentzen