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

@@ -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}
 

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
 

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
 
 

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

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