add(Propositional/Kripke): Rewriting model-based semantics

Foundation.lean

@@ -494,6 +494,18 @@ public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl_Tra1
 public import Foundation.Propositional.Kripke2.Hilbert.F_Ser
 public import Foundation.Propositional.Kripke2.Hilbert.F_Sym
 public import Foundation.Propositional.Kripke2.Hilbert.F_Tra1
+public import Foundation.Propositional.Kripke3.Axiom.Dummett
+public import Foundation.Propositional.Kripke3.Axiom.KreiselPutnam
+public import Foundation.Propositional.Kripke3.Axiom.LEM
+public import Foundation.Propositional.Kripke3.Axiom.Tra
+public import Foundation.Propositional.Kripke3.Axiom.WLEM
+public import Foundation.Propositional.Kripke3.Basic
+public import Foundation.Propositional.Kripke3.Logic.Cl
+public import Foundation.Propositional.Kripke3.Logic.Int.Completeness
+public import Foundation.Propositional.Kripke3.Logic.Int.DP
+public import Foundation.Propositional.Kripke3.Logic.KC
+public import Foundation.Propositional.Kripke3.Logic.KreiselPutnam
+public import Foundation.Propositional.Kripke3.Logic.LC
 public import Foundation.Propositional.Logic.Basic
 public import Foundation.Propositional.Logic.Letterless_Int_Cl
 public import Foundation.Propositional.Logic.PostComplete

Foundation/Propositional/Entailment/Corsi/VF.lean

@@ -124,7 +124,6 @@ lemma ruleC_fconj' {Γ : Finset ι} (Φ : ι → F) (h : ∀ i ∈ Γ, 𝓢 ⊢
   simpa;
 
 
-
 lemma mem_lconj₂ {Γ : List F} (h : φ ∈ Γ) : 𝓢 ⊢ ⋀Γ 🡒 φ := by
   induction Γ using List.induction_with_singleton with
   | hcons ψ Δ he ih =>
@@ -191,6 +190,10 @@ lemma mem_ldisj₂ {Γ : List F} (h : ψ ∈ Γ) : 𝓢 ⊢ ψ 🡒 Γ.disj₂ :
       exact orIntroR;
   | _ => simp_all;
 
+lemma mem_fdisj {Γ : Finset F} (h : ψ ∈ Γ) : 𝓢 ⊢ ψ 🡒 Γ.disj := by
+  apply mem_ldisj₂;
+  simpa using h;
+
 lemma mem_fdisj' {Γ : Finset ι} (Φ : ι → F) (hΦ : ∃ i ∈ Γ, Φ i = ψ) : 𝓢 ⊢ ψ 🡒 ⩖ i ∈ Γ, Φ i := by
   apply mem_ldisj₂;
   simpa;
@@ -212,6 +215,26 @@ lemma ruleD_fdisj' {Γ : Finset ι} (Φ : ι → F) (h : ∀ i ∈ Γ, 𝓢 ⊢
   simpa;
 
 
+lemma CLDisj₂Disj₂_of_provable {Γ : List F} (h : ∀ γ ∈ Γ, 𝓢 ⊢ γ 🡒 δ) : 𝓢 ⊢ Γ.disj₂ 🡒 δ := by
+  induction Γ using List.induction_with_singleton with
+  | hnil => simp only [List.disj₂_nil, Entailment.efq!];
+  | hsingle φ => apply h; simp;
+  | hcons ψ Δ he ih =>
+    simp only [List.disj₂_cons_nonempty he];
+    simp only [List.mem_cons, forall_eq_or_imp] at h;
+    apply ruleD;
+    . apply h.1;
+    . apply ih h.2;
+
+lemma CLDisj₂Disj₂_of_subset {Γ Δ : List F} (h : ∀ φ, φ ∈ Γ → φ ∈ Δ) : 𝓢 ⊢ Γ.disj₂ 🡒 Δ.disj₂ := by
+  apply CLDisj₂Disj₂_of_provable;
+  intro γ hγ;
+  apply mem_ldisj₂ $ h _ hγ;
+
+lemma CFDisjFDisj_of_subset {Γ Δ : Finset F} (h : Γ ⊆ Δ) : 𝓢 ⊢ Γ.disj 🡒 Δ.disj := by
+  apply CLDisj₂Disj₂_of_subset;
+  simpa;
+
 
 variable [Entailment.Disjunctive 𝓢] [Entailment.Consistent 𝓢]
 

Foundation/Propositional/Kripke/AxiomDummett.lean

@@ -102,5 +102,7 @@ end canonicality
 
 end Kripke
 
+
+
 end LO.Propositional
 end

Foundation/Propositional/Kripke3/Axiom/Dummett.lean

@@ -0,0 +1,96 @@
+module
+
+public import Foundation.Propositional.Kripke3.Basic
+public import Foundation.Vorspiel.Rel.Connected
+public import Foundation.Propositional.Kripke3.Logic.Int.Completeness
+
+@[expose] public section
+
+namespace LO.Propositional
+
+variable {κ α : Type*} [Nonempty κ]
+
+namespace KripkeModel
+
+variable {M : KripkeModel κ α} [M.Intuitionistic] {φ ψ χ : Formula α}
+
+lemma validates_axiomDummett [IsPiecewiseStronglyConnected M.rel] : M ⊧ (Axioms.Dummett φ ψ) := by
+  have : PiecewiseStronglyConnected M.rel := IsPiecewiseStronglyConnected.ps_connected;
+  contrapose! this;
+  obtain ⟨x, h⟩ := exists_world_notForces_of_notValidates this;
+  replace h := forces_or.not.mp h;
+  push_neg at h;
+  rcases h with ⟨h₁, h₂⟩;
+
+  replace h₁ := forces_imp.not.mp h₁;
+  push_neg at h₁;
+  obtain ⟨y, Rxy, hyφ, hyψ⟩ := h₁;
+
+  replace h₂ := forces_imp.not.mp h₂;
+  push_neg at h₂;
+  obtain ⟨z, Rxz, hzψ, hzφ⟩ := h₂;
+
+  dsimp [PiecewiseStronglyConnected]
+  push_neg;
+  use x, y, z;
+  refine ⟨Rxy, Rxz, ?_⟩;
+  . set_option push_neg.use_distrib true in by_contra! hC;
+    rcases hC with (Ryz | Rzy);
+    . apply hzφ $ M.formula_persistency hyφ Ryz;
+    . apply hyψ $ M.formula_persistency hzψ Rzy;
+
+variable [DecidableEq α]
+lemma isPiecewiseStronglyConvergent_of_validates_axiomDummett
+  (a b : α) (hab : a ≠ b := by trivial)
+  [Std.Refl K]
+  (h : ∀ V, letI M : KripkeModel κ α := ⟨K, V⟩; M ⊧ (Axioms.Dummett #a #b))
+  : IsPiecewiseStronglyConvergent K := by
+  constructor;
+  rintro x y z Rxy Rxz;
+  have := (h $ (λ {p v} => if p = a then K y v else if p = b then K z v else True)) x;
+  rw [forces_or] at this;
+  rcases this with (hi | hi);
+  . simp only [forces_imp, forces_atom, ↓reduceIte, hab.symm] at hi;
+    use y;
+    constructor;
+    . apply Std.Refl.refl;
+    . apply hi;
+      . assumption;
+      . apply Std.Refl.refl;
+  . use z;
+    simp only [forces_imp, forces_atom, hab.symm, ↓reduceIte] at hi;
+    constructor;
+    . apply hi z Rxz;
+      exact Std.Refl.refl z;
+    . apply Std.Refl.refl;
+
+end KripkeModel
+
+
+
+section
+
+variable {S} [Entailment S (Formula ℕ)]
+variable {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢]
+
+open Formula.Kripke
+open LO.Entailment
+     LO.Entailment.FiniteContext
+open canonicalKripkeModel
+open SaturatedConsistentTableau
+open Classical
+
+instance [Entailment.HasAxiomDummett 𝓢] : IsPiecewiseStronglyConnected (canonicalKripkeModel 𝓢).rel := by
+  constructor;
+  rintro x y z Rxy Rxz;
+  by_contra!;
+  obtain ⟨φ, hφy, hφz⟩ := Set.not_subset.mp this.1;
+  obtain ⟨ψ, hψz, hψy⟩ := Set.not_subset.mp this.2;
+  rcases (show φ 🡒 ψ ∈ x.1.1 ∨ ψ 🡒 φ ∈ x.1.1 by exact iff_mem₁_or.mp $ mem₁_of_provable dummett!) with (hφψx | hψφx);
+  . exact hψy $ mdp₁_mem hφy (Rxy hφψx);
+  . exact hφz $ mdp₁_mem hψz (Rxz hψφx);
+
+end
+
+end LO.Propositional
+end