Skip to content

Commit b8b4aee

Browse files
SnO2WMaNSnO2WMaN
committed
add(Propositional/Kripke): Rewriting model-based semantics
1 parent 0246417 commit b8b4aee

5 files changed

Lines changed: 453 additions & 0 deletions

File tree

‎Foundation/Propositional/Kripke3/Axiom/Dummett.lean‎

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
module
2+
3+
public import Foundation.Propositional.Kripke3.Basic
4+
public import Foundation.Vorspiel.Rel.Connected
5+
6+
@[expose] public section
7+
8+
namespace LO.Propositional
9+
10+
variable {κ α : Type*} [Nonempty κ]
11+
12+
namespace KripkeModel
13+
14+
variable {M : KripkeModel κ α} [M.Intuitionistic] {φ ψ χ : Formula α}
15+
16+
lemma validates_axiomDummett [IsPiecewiseStronglyConnected M.rel] : M ⊧ (Axioms.Dummett φ ψ) := by
17+
have : PiecewiseStronglyConnected M.rel := IsPiecewiseStronglyConnected.ps_connected;
18+
contrapose! this;
19+
obtain ⟨x, h⟩ := exists_world_notForces_of_notValidates this;
20+
replace h := forces_or.not.mp h;
21+
push_neg at h;
22+
rcases h with ⟨h₁, h₂⟩;
23+
24+
replace h₁ := forces_imp.not.mp h₁;
25+
push_neg at h₁;
26+
obtain ⟨y, Rxy, hyφ, hyψ⟩ := h₁;
27+
28+
replace h₂ := forces_imp.not.mp h₂;
29+
push_neg at h₂;
30+
obtain ⟨z, Rxz, hzψ, hzφ⟩ := h₂;
31+
32+
dsimp [PiecewiseStronglyConnected]
33+
push_neg;
34+
use x, y, z;
35+
refine ⟨Rxy, Rxz, ?_⟩;
36+
. set_option push_neg.use_distrib true in by_contra! hC;
37+
rcases hC with (Ryz | Rzy);
38+
. apply hzφ $ M.formula_persistency hyφ Ryz;
39+
. apply hyψ $ M.formula_persistency hzψ Rzy;
40+
41+
variable [DecidableEq α]
42+
lemma isPiecewiseStronglyConvergent_of_validates_axiomDummett
43+
(a b : α) (hab : a ≠ b := by trivial)
44+
[Std.Refl K]
45+
(h : ∀ V, letI M : KripkeModel κ α := ⟨K, V⟩; M ⊧ (Axioms.Dummett #a #b))
46+
: IsPiecewiseStronglyConvergent K := by
47+
constructor;
48+
rintro x y z Rxy Rxz;
49+
have := (h $ (λ {p v} => if p = a then K y v else if p = b then K z v else True)) x;
50+
rw [forces_or] at this;
51+
rcases this with (hi | hi);
52+
. simp only [forces_imp, forces_atom, ↓reduceIte, hab.symm] at hi;
53+
use y;
54+
constructor;
55+
. apply Std.Refl.refl;
56+
. apply hi;
57+
. assumption;
58+
. apply Std.Refl.refl;
59+
. use z;
60+
simp only [forces_imp, forces_atom, hab.symm, ↓reduceIte] at hi;
61+
constructor;
62+
. apply hi z Rxz;
63+
exact Std.Refl.refl z;
64+
. apply Std.Refl.refl;
65+
66+
end KripkeModel
67+
68+
end LO.Propositional
69+
end

‎Foundation/Propositional/Kripke3/Axiom/LEM.lean‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
module
2+
3+
public import Foundation.Propositional.Kripke3.Basic
4+
public import Foundation.Vorspiel.Rel.Euclidean
5+
6+
@[expose] public section
7+
8+
namespace LO.Propositional
9+
10+
variable {κ α : Type*} [Nonempty κ]
11+
12+
namespace KripkeModel
13+
14+
variable {M : KripkeModel κ α} [M.Intuitionistic] {φ ψ χ : Formula α}
15+
16+
lemma validates_axiomLEM_of_isSymmetric [Std.Symm M.rel] : M ⊧ (Axioms.LEM φ) := by
17+
have : Symmetric M.rel := Std.Symm.symm;
18+
contrapose! this;
19+
obtain ⟨x, h⟩ := exists_world_notForces_of_notValidates this;
20+
21+
replace h := forces_or.not.mp h;
22+
push_neg at h;
23+
rcases h with ⟨h₁, h₂⟩;
24+
25+
replace h₂ := forces_neg.not.mp h₂;
26+
push_neg at h₂;
27+
obtain ⟨y, Rxy, hy⟩ := h₂;
28+
29+
dsimp [Symmetric]
30+
push_neg;
31+
use x, y;
32+
constructor;
33+
. assumption;
34+
. contrapose! h₁;
35+
apply M.formula_persistency hy h₁;
36+
37+
lemma validates_axiomLEM_of_isRightEuclidean [IsRightEuclidean M.rel] : M ⊧ (Axioms.LEM φ) := validates_axiomLEM_of_isSymmetric
38+
39+
lemma isRightEuclidean_of_validates_axiomLEM [Std.Refl K] [IsTrans _ K]
40+
(h : ∀ V, letI M : KripkeModel κ α := ⟨K, V⟩; M ⊧ (Axioms.LEM #a))
41+
: IsRightEuclidean K := by
42+
constructor;
43+
rintro x y z Rxy Rxz;
44+
have := h (λ {p v} => K y v) x;
45+
rcases this with (hi | hi);
46+
. apply IsTrans.trans y x z hi Rxz;
47+
. exfalso;
48+
apply forces_neg.mp hi y Rxy;
49+
apply Std.Refl.refl;
50+
51+
end KripkeModel
52+
53+
end LO.Propositional
54+
end

‎Foundation/Propositional/Kripke3/Axiom/Tra.lean‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
module
2+
3+
public import Foundation.Propositional.Kripke3.Basic
4+
5+
@[expose] public section
6+
7+
namespace LO.Propositional
8+
9+
variable {κ α : Type*} [Nonempty κ]
10+
11+
namespace KripkeModel
12+
13+
variable {M : KripkeModel κ α} [IsTrans _ M.rel]
14+
{φ ψ χ : Formula α}
15+
16+
@[simp, grind .]
17+
lemma validates_axiomTra₁ : M ⊧ Axioms.Tra1 φ ψ χ :=
18+
fun _ y _ hyφψ z Ryz _ w Rzw hzφ =>
19+
hyφψ w (IsTrans.trans y z w Ryz Rzw) hzφ
20+
21+
@[simp, grind .]
22+
lemma validates_axiomTra₂ : M ⊧ Axioms.Tra2 φ ψ χ :=
23+
fun _ y _ hyφψ z Ryz hzψχ w Rzw hwφ =>
24+
hzψχ w Rzw $ hyφψ w (IsTrans.trans y z w Ryz Rzw) hwφ
25+
26+
end KripkeModel
27+
28+
end LO.Propositional
29+
30+
end

‎Foundation/Propositional/Kripke3/Axiom/WLEM.lean‎

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
module
2+
3+
public import Foundation.Propositional.Kripke3.Basic
4+
public import Foundation.Vorspiel.Rel.Convergent
5+
6+
@[expose] public section
7+
8+
namespace LO.Propositional
9+
10+
variable {κ α : Type*} [Nonempty κ]
11+
12+
namespace KripkeModel
13+
14+
variable {M : KripkeModel κ α} [M.Intuitionistic] {φ ψ χ : Formula α}
15+
16+
lemma validates_axiomWLEM [IsPiecewiseStronglyConvergent M.rel] : M ⊧ (Axioms.WLEM φ) := by
17+
have : PiecewiseStronglyConvergent M.rel := IsPiecewiseStronglyConvergent.ps_convergent;
18+
contrapose! this;
19+
obtain ⟨x, h⟩ := exists_world_notForces_of_notValidates this;
20+
21+
replace h := forces_or.not.mp h;
22+
push_neg at h;
23+
rcases h with ⟨h₁, h₂⟩;
24+
25+
replace h₁ := forces_neg.not.mp h₁;
26+
push_neg at h₁;
27+
obtain ⟨y, Rxy, hy⟩ := h₁;
28+
29+
replace h₂ := forces_neg.not.mp h₂;
30+
push_neg at h₂;
31+
obtain ⟨z, Rxz, hz⟩ := h₂;
32+
33+
dsimp [PiecewiseStronglyConvergent]
34+
push_neg;
35+
use x, y, z;
36+
refine ⟨Rxy, Rxz, ?_⟩;
37+
. intro u Ryu;
38+
by_contra Rzu;
39+
exact hz u Rzu $ M.formula_persistency hy Ryu;
40+
41+
lemma isPiecewiseStronglyConvergent_of_validates_axiomWLEM [Std.Refl K]
42+
(h : ∀ V, letI M : KripkeModel κ α := ⟨K, V⟩; M ⊧ (Axioms.WLEM #a))
43+
: IsPiecewiseStronglyConvergent K := by
44+
constructor;
45+
rintro x y z Rxy Rxz;
46+
have := (h $ (λ {p v} => K y v)) x;
47+
rw [forces_or] at this;
48+
rcases this with (hi | hi);
49+
. exfalso;
50+
simp only [forces_neg, ForcingRelation.NotForces, forces_atom] at hi;
51+
apply hi y Rxy $ Std.Refl.refl y;
52+
. simp only [forces_neg, ForcingRelation.NotForces, forces_atom] at hi;
53+
push_neg at hi;
54+
obtain ⟨w, Rzw, Ryw⟩ := hi z Rxz;
55+
use w;
56+
57+
end KripkeModel
58+
59+
end LO.Propositional
60+
end

0 commit comments

Comments
 (0)