add(Modal/Kripke): Rewriting to only Model based semantics

Foundation/Modal/Hilbert/Normal2/Basic.lean

@@ -0,0 +1,84 @@
+module
+
+public import Foundation.Modal.Entailment.GL
+public import Foundation.Modal.Entailment.Grz
+public import Foundation.Modal.Entailment.K4Hen
+public import Foundation.Modal.Entailment.K4Henkin
+public import Foundation.Modal.Entailment.S5Grz
+public import Foundation.Modal.Hilbert.Axiom
+public import Foundation.Modal.Logic.Basic
+public import Foundation.Modal.Logic.Basic
+public import Foundation.Propositional.Entailment.Cl.Łukasiewicz
+
+@[expose] public section
+
+namespace LO.Modal
+
+open LO.Entailment LO.Modal.Entailment
+
+inductive Hilbert.Normal {α} (Ax : Set (Formula α)) : Logic α
+| axm {φ}       : φ ∈ Ax → Normal Ax φ
+| mdp {φ ψ}     : Normal Ax (φ ➝ ψ) → Normal Ax φ → Normal Ax ψ
+| nec {φ}       : Normal Ax φ → Normal Ax (□φ)
+| implyK φ ψ    : Normal Ax $ Axioms.ImplyK φ ψ
+| implyS φ ψ χ  : Normal Ax $ Axioms.ImplyS φ ψ χ
+| ec φ ψ        : Normal Ax $ Axioms.ElimContra φ ψ
+
+namespace Hilbert.Normal
+
+variable {Ax Ax₁ Ax₂ : Axiom α}
+
+instance : Entailment.Łukasiewicz (Hilbert.Normal Ax) where
+  implyK {_ _} := by constructor; apply Hilbert.Normal.implyK;
+  implyS {_ _ _} := by constructor; apply Hilbert.Normal.implyS;
+  elimContra {_ _} := by constructor; apply Hilbert.Normal.ec;
+  mdp h₁ h₂ := by
+    constructor;
+    apply Hilbert.Normal.mdp;
+    . exact h₁.1;
+    . exact h₂.1;
+
+instance : Entailment.Necessitation (Hilbert.Normal Ax) where
+  nec h := by constructor; apply Hilbert.Normal.nec; exact h.1;
+
+lemma axm' {φ} : φ ∈ Ax → Hilbert.Normal Ax ⊢ φ := fun h ↦ ⟨⟨axm h⟩⟩
+
+protected lemma rec!
+  {motive   : (φ : Formula α) → (Normal Ax ⊢ φ) → Sort}
+  (axm      : ∀ {φ : Formula α}, (h : φ ∈ Ax) → motive φ (axm' h))
+  (mdp      : ∀ {φ ψ : Formula α}, {hφψ : (Normal Ax) ⊢ φ ➝ ψ} → {hφ : (Normal Ax) ⊢ φ} → motive (φ ➝ ψ) hφψ → motive φ hφ → motive ψ (hφψ ⨀ hφ))
+  (nec      : ∀ {φ}, {hφψ : (Normal Ax) ⊢ φ} → motive (φ) hφψ → motive (□φ) (nec! hφψ))
+  (implyK   : ∀ {φ ψ}, motive (Axioms.ImplyK φ ψ) $ by simp)
+  (implyS   : ∀ {φ ψ χ}, motive (Axioms.ImplyS φ ψ χ) $ by simp)
+  (ec       : ∀ {φ ψ}, motive (Axioms.ElimContra φ ψ) $ by simp)
+  : ∀ {φ}, (d : Normal Ax ⊢ φ) → motive φ d := by
+  rintro φ d;
+  replace d := Logic.iff_provable.mp d;
+  induction d with
+  | axm h => apply axm h;
+  | mdp hφψ hφ ihφψ ihφ =>
+    apply mdp;
+    . exact ihφψ (Logic.iff_provable.mpr hφψ);
+    . exact ihφ (Logic.iff_provable.mpr hφ);
+  | nec hφ ihφ => apply nec; exact ihφ (Logic.iff_provable.mpr hφ);
+  | implyK φ ψ => apply implyK;
+  | implyS φ ψ χ => apply implyS;
+  | ec φ ψ => apply ec;
+
+open Axiom
+
+
+end Hilbert.Normal
+
+
+section
+
+open Hilbert.Normal
+
+protected abbrev K (α) : Logic α := Hilbert.Normal { Axioms.K φ ψ | (φ : Formula α) (ψ : Formula α) }
+
+end
+
+end LO.Modal
+
+end

Foundation/Modal/Kripke2/Basic.lean

@@ -0,0 +1,218 @@
+module
+
+public import Foundation.Modal.Logic.Basic
+public import Foundation.Vorspiel.Rel.Basic
+public import Foundation.Logic.ForcingRelation
+
+@[expose] public section
+
+variable {κ α : Type*} [Nonempty κ]
+
+namespace LO.Modal
+
+open Entailment
+
+structure KripkeModel (κ : Type*) [Nonempty κ] (α : Type*) where
+  rel : Rel κ κ
+  val : α → κ → Prop
+
+namespace KripkeModel
+
+abbrev world (_ : KripkeModel κ α) := κ
+
+variable {M : KripkeModel κ α} {x y z : M.world} {a : α} {φ ψ χ : Formula α} {n m : ℕ}
+
+
+abbrev rel' : Rel M.world M.world := M.rel
+infix:45 " ≺ " => rel'
+
+abbrev invRel (x y : M.world) := M.rel y x
+infix:45 " ≻ " => invRel
+
+abbrev relItr (n : ℕ) : Rel M.world M.world := M.rel.Iterate n
+notation x:45 " ≺^[" n:0 "] " y:46 => relItr n x y
+
+-- instance : CoeSort (KripkeModel κ α) (Type*) := ⟨λ M => M.world⟩
+instance : CoeFun (KripkeModel κ α) (λ _ => α → κ → Prop) := ⟨fun M => M.val⟩
+
+abbrev replaceVal (M : KripkeModel κ α) (V : α → M.world → Prop) : KripkeModel κ α where
+  rel := M.rel
+  val := V
+
+@[simp]
+lemma replaceVal_comp {V₁ V₂ : α → M.world → Prop}
+  : (M.replaceVal V₁ |>.replaceVal V₂) = M.replaceVal V₂ := by tauto;
+
+section Forces
+
+@[grind]
+def Forces (M : KripkeModel κ α) (x : M.world) : Formula α → Prop
+  | .atom a  => M a x
+  | ⊥  => False
+  | φ ➝ ψ => (M.Forces x φ) ➝ (M.Forces x ψ)
+  | □φ   => ∀ y, x ≺ y → (M.Forces y φ)
+
+instance : ForcingRelation M.world (Formula α) where
+  Forces := Forces M
+
+@[grind =] lemma forces_atom : x ⊩ (.atom a) ↔ M a x := by tauto
+@[simp, grind .] lemma forces_falsum : x ⊮ ⊥ := by tauto;
+@[simp, grind .] lemma forces_verum : x ⊩ ⊤ := by tauto;
+@[grind =] lemma forces_imp : x ⊩ (φ ➝ ψ) ↔ (x ⊩ φ) ➝ (x ⊩ ψ) := by tauto;
+@[grind =] lemma forces_neg : x ⊩ ∼φ ↔ x ⊮ φ := by tauto;
+@[grind =] lemma forces_and : x ⊩ (φ ⋏ ψ) ↔ (x ⊩ φ) ∧ (x ⊩ ψ) := by grind;
+@[grind =] lemma forces_or : x ⊩ (φ ⋎ ψ) ↔ (x ⊩ φ) ∨ (x ⊩ ψ) := by grind;
+@[grind =] lemma forces_iff : x ⊩ (φ ⭤ ψ) ↔ ((x ⊩ φ) ↔ (x ⊩ ψ)) := by grind [LogicalConnective.iff];
+@[grind =] lemma forces_box : x ⊩ □φ ↔ ∀ y, x ≺ y → (y ⊩ φ) := by tauto;
+
+@[grind =] lemma iff_forces_dn : x ⊩ ∼∼φ ↔ x ⊩ φ := by simp [forces_neg, forces_neg.not];
+
+@[grind =]
+lemma forces_dia : x ⊩ ◇φ ↔ ∃ y, x ≺ y ∧ (y ⊩ φ) := calc
+  _ ↔ x ⊩ ∼□(∼φ) := by rw [DiaByBox.dia_by_box]
+  _ ↔ x ⊮ □(∼φ)  := by grind;
+  _ ↔ ¬x ⊩ □(∼φ) := by grind;
+  _ ↔ ¬(∀ y, x ≺ y → y ⊩ ∼φ) := by grind;
+  _ ↔ ∃ y, x ≺ y ∧ y ⊮ ∼φ := by grind;
+  _ ↔ ∃ y, x ≺ y ∧ y ⊩ (∼∼φ) := by simp [forces_neg];
+  _ ↔ _ := by simp [iff_forces_dn];
+
+instance : ForcingRelation.BasicSemantics M.world where
+  verum {_} := forces_verum
+  falsum {_} := forces_falsum
+  and {_ _ _} := forces_and
+  or {_ _ _} := forces_or
+
+
+@[grind =]
+lemma forces_boxItr : x ⊩ □^[n]φ ↔ ∀ y, x ≺^[n] y → y ⊩ φ := by
+  induction n generalizing x <;> grind [Rel.Iterate.iff_zero, Rel.Iterate.iff_succ];
+
+@[grind =]
+lemma forces_diaItr : x ⊩ ◇^[n]φ ↔ ∃ y, x ≺^[n] y ∧ (y ⊩ φ) := by
+  induction n generalizing x <;> grind [Rel.Iterate.iff_zero, Rel.Iterate.iff_succ];
+
+
+@[grind =]
+lemma forces_lconj {l : List _} : x ⊩ l.conj ↔ ∀ φ ∈ l, x ⊩ φ := by
+  induction l <;>
+  grind [List.conj_cons, List.conj_nil];
+
+@[grind =]
+lemma forces_lconj₂ {l : List _} : x ⊩ ⋀l ↔ ∀ φ ∈ l, x ⊩ φ := by
+  induction l using List.induction_with_singleton <;>
+  grind [List.conj₂_nil, List.conj₂_cons_nonempty, List.conj₂_singleton]
+
+@[grind =]
+lemma forces_lconj' {l : List β} {ι : β → Formula α} : x ⊩ l.conj' ι ↔ ∀ i ∈ l, x ⊩ (ι i) := by
+  grind [List.conj'];
+
+@[grind =]
+lemma forces_fconj {s : Finset _} : x ⊩ s.conj ↔ ∀ φ ∈ s, x ⊩ φ := by
+  apply Iff.trans forces_lconj₂;
+  simp;
+
+@[grind =]
+lemma forces_fconj' {s : Finset β} {ι : β → Formula α} : x ⊩ s.conj' ι ↔ ∀ i ∈ s, x ⊩ (ι i) := by
+  apply Iff.trans forces_lconj';
+  simp;
+
+
+@[grind =]
+lemma forces_ldisj {l : List _} : x ⊩ l.disj ↔ ∃ φ ∈ l, x ⊩ φ := by
+  induction l <;>
+  grind [List.disj_cons, List.disj_nil];
+
+@[grind =]
+lemma forces_ldisj₂ {l : List _} : x ⊩ ⋁l ↔ ∃ φ ∈ l, x ⊩ φ := by
+  induction l using List.induction_with_singleton <;>
+  grind [List.disj₂_nil, List.disj₂_cons_nonempty, List.disj₂_singleton]
+
+@[grind =]
+lemma forces_ldisj' {l : List β} {ι : β → Formula α} : x ⊩ l.disj' ι ↔ ∃ i ∈ l, x ⊩ (ι i) := by
+  grind [List.disj']
+
+@[grind =]
+lemma forces_fdisj {s : Finset _} : x ⊩ s.disj ↔ ∃ φ ∈ s, x ⊩ φ := by
+  apply Iff.trans forces_ldisj₂;
+  simp;
+
+@[grind =]
+lemma forces_fdisj' {s : Finset β} {ι : β → Formula α} : x ⊩ s.disj' ι ↔ ∃ i ∈ s, x ⊩ (ι i) := by
+  apply Iff.trans forces_ldisj';
+  simp;
+
+
+/-
+lemma iff_forces_diaItr_dual : (x ⊩ ◇^[n]φ) ↔ (x ⊩ ∼□^[n](∼φ)) := calc
+  _ ↔ ∃ y, x ≺^[n] y ∧ (y ⊩ φ) := forces_diaItr
+  _ ↔ ¬(∀ y, x ≺^[n] y → ¬y ⊩ φ) := by push_neg; rfl;
+  _ ↔ _ := by sorry;
+-/
+
+lemma iff_dia_dual : (x ⊩ ◇φ) ↔ (x ⊩ ∼□(∼φ)) := by
+  grind [Rel.Iterate.iff_zero, Rel.Iterate.iff_succ];
+
+
+abbrev replaceSubstVal (M : KripkeModel κ α) (s : Substitution α) : KripkeModel κ α
+  := M.replaceVal (λ a x => x ⊩ (s a))
+
+lemma iff_forces_replaceSubstVal (s : Substitution α) :
+  (M.replaceSubstVal s).Forces x φ ↔ x ⊩ (φ⟦s⟧) := by
+  induction φ generalizing x <;> . dsimp [Forces]; grind;
+
+end Forces
+
+
+section Models
+
+def Models (M : KripkeModel κ α) (φ) := M.world ∀⊩ φ
+infix:45 " ⊧ " => Models
+
+abbrev NotModels (M : KripkeModel κ α) (φ) := ¬M ⊧ φ
+infix:45 " ⊭ " => NotModels
+
+@[simp, grind .]
+lemma models_verum : M ⊧ ⊤ := ForcingRelation.AllForces.verum
+
+@[simp, grind .]
+lemma models_falsum : M ⊭ ⊥ := by simp [NotModels, Models]
+
+@[grind =]
+lemma models_and : M ⊧ (φ ⋏ ψ) ↔ M ⊧ φ ∧ M ⊧ ψ := ForcingRelation.AllForces.and
+
+@[grind =]
+lemma iff_notModels_exists_world_notForces : M ⊭ φ ↔ ∃ x : M.world, x ⊮ φ := by
+  simp [NotModels, Models];
+alias ⟨exists_world_notForces_of_notModels, notModels_of_exists_world_notForces⟩ := iff_notModels_exists_world_notForces
+
+@[grind <=]
+lemma models_mdp (hpq : M ⊧ φ ➝ ψ) (hp : M ⊧ φ) : M ⊧ ψ := fun x ↦ hpq x (hp x)
+
+@[grind <=]
+lemma models_nec (hp : M ⊧ φ) : M ⊧ □φ := fun _ y _ ↦ hp y
+
+@[grind <=]
+lemma models_multinec (hp : M ⊧ φ) : M ⊧ □^[n]φ := by induction n <;> grind;
+
+lemma models_implyK : M ⊧ (Axioms.ImplyK φ ψ) := by intro x; grind;
+lemma models_implyS : M ⊧ (Axioms.ImplyS φ ψ χ) := by intro x; grind;
+lemma models_elimContra : M ⊧ (Axioms.ElimContra φ ψ) := by intro x; grind;
+lemma models_axiomK : M ⊧ (Axioms.K φ ψ) := by tauto;
+
+attribute [simp, grind .]
+  models_implyK
+  models_implyS
+  models_elimContra
+  models_axiomK
+
+end Models
+
+
+def logic (M : KripkeModel κ α) : Logic α := { φ | M ⊧ φ }
+
+end KripkeModel
+
+
+
+end LO.Modal

Foundation/Modal/Kripke2/Completeness.lean

@@ -0,0 +1,88 @@
+module
+
+public import Foundation.Modal.Tableau
+public import Foundation.Modal.Kripke2.Basic
+
+@[expose] public section
+
+namespace LO.Modal
+
+open Entailment
+open Formula
+open MaximalConsistentTableau
+open KripkeModel
+
+variable [DecidableEq α] [Encodable α]
+variable {S} [Entailment S (Formula α)]
+variable {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢]
+variable {φ ψ : Formula α}
+
+@[grind]
+def canonicalKripkeModel (𝓢 : S) [Entailment.Consistent 𝓢] [Entailment.K 𝓢] : KripkeModel (MaximalConsistentTableau 𝓢) α where
+  rel t₁ t₂ := □⁻¹'t₁.1.1 ⊆ t₂.1.1
+  val a t := (atom a) ∈ t.1.1
+
+attribute [grind .]
+  MaximalConsistentTableau.not_mem₁_falsum
+  MaximalConsistentTableau.mem₂_falsum
+attribute [grind =] MaximalConsistentTableau.iff_mem₁_imp
+attribute [grind =] MaximalConsistentTableau.iff_not_mem₁_mem₂
+attribute [grind =]
+  MaximalConsistentTableau.iff_mem₁_box
+  MaximalConsistentTableau.iff_mem₂_box
+
+namespace canonicalKripkeModel
+
+variable {t : (canonicalKripkeModel 𝓢).world}
+
+lemma truthlemma : (φ ∈ t.1.1 ↔ t ⊩ φ) ∧ (φ ∈ t.1.2 ↔ t ⊮ φ) := by
+  induction φ generalizing t with
+  | hatom | hfalsum | himp => grind;
+  | hbox φ ihφ =>
+    constructor;
+    . constructor;
+      . intro h t' Rtt';
+        apply ihφ.1.1;
+        grind;
+      . intro h;
+        apply iff_mem₁_box.mpr;
+        intro t' Rtt';
+        apply ihφ.1.2;
+        exact h t' Rtt';
+    . constructor;
+      . intro h;
+        apply forces_box.not.mpr;
+        push_neg;
+        obtain ⟨t', Rtt', ht'⟩ := iff_mem₂_box.mp h;
+        use t';
+        grind;
+      . intro h;
+        apply iff_mem₂_box.mpr;
+        replace h := forces_box.not.mp h;
+        grind;
+
+@[grind =] lemma truthlemma₁ : φ ∈ t.1.1 ↔ t ⊩ φ := truthlemma.1
+@[grind =] lemma truthlemma₂ : φ ∈ t.1.2 ↔ t ⊮ φ := truthlemma.2
+
+@[grind =]
+lemma iff_valid_provable : (canonicalKripkeModel 𝓢) ⊧ φ ↔ 𝓢 ⊢ φ := by
+  constructor;
+  . contrapose!;
+    intro h;
+    have : Tableau.Consistent 𝓢 (∅, {φ}) := by
+      apply Tableau.iff_consistent_empty_singleton₂.mpr;
+      exact h;
+    obtain ⟨t, ht⟩ := lindenbaum this;
+    apply notModels_of_exists_world_notForces;
+    use t;
+    apply truthlemma₂.mp;
+    apply ht.2;
+    tauto_set;
+  . intro h t;
+    exact truthlemma₁.mp $ MaximalConsistentTableau.iff_provable_mem₁.mp h t;
+
+end canonicalKripkeModel
+
+end LO.Modal
+
+end