gotrevor-Foundation/Foundation/Modal/Kripke/AxiomPoint3.lean at master · FormalizedFormalLogic/gotrevor-Foundation · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
module

public import Foundation.Modal.Kripke.AxiomWeakPoint3

@[expose] public section

namespace LO.Modal

namespace Kripke

variable {F : Kripke.Frame}

namespace Frame

variable {F : Frame}

abbrev IsPiecewiseStronglyConnected (F : Frame) := _root_.IsPiecewiseStronglyConnected F.Rel

instance [F.IsPiecewiseStronglyConnected] : F.IsPiecewiseConnected := inferInstance

lemma ps_connected [F.IsPiecewiseStronglyConnected] : ∀ {x y z : F.World}, x ≺ y → x ≺ z → y ≺ z ∨ z ≺ y := by
  apply IsPiecewiseStronglyConnected.ps_connected

end Frame


instance : whitepoint.IsPiecewiseStronglyConnected where
  ps_connected := by tauto;


section definability

open Formula (atom)
open Formula.Kripke

lemma validate_axiomPoint3_of_isPiecewiseStronglyConnected [F.IsPiecewiseStronglyConnected] : F ⊧ (Axioms.Point3 (.atom 0) (.atom 1)) := by
  rintro V x;
  apply Satisfies.or_def.mpr;
  suffices
    (∀ y, x ≺ y → (∀ z, y ≺ z → V 0 z) → V 1 y) ∨
    (∀ y, x ≺ y → (∀ z, y ≺ z → V 1 z) → V 0 y)
    by simpa [Semantics.Models, Satisfies];
  by_contra hC;
  push Not at hC;
  obtain ⟨⟨y, Rxy, hp, hnq⟩, ⟨z, Rxz, hq, hnp⟩⟩ := hC;
  rcases IsPiecewiseStronglyConnected.ps_connected Rxy Rxz with (Ryz | Rzy);
  . have := hp z Ryz; contradiction;
  . have := hq y Rzy; contradiction;

lemma isPiecewiseStronglyConnected_of_validate_axiomPoint3 (h : F ⊧ (Axioms.Point3 (.atom 0) (.atom 1))) : F.IsPiecewiseStronglyConnected where
  ps_connected := by
    dsimp [PiecewiseStronglyConnected];
    revert h;
    contrapose!;
    rintro ⟨x, y, z, Rxy, Rxz, nRyz, nRzy⟩;
    apply ValidOnFrame.not_of_exists_valuation_world;
    use (λ a w => match a with | 0 => y ≺ w | 1 => z ≺ w | _ => False), x;
    suffices ∃ y', x ≺ y' ∧ (∀ z', y' ≺ z' → y ≺ z') ∧ ¬z ≺ y' ∧ (∃ z', x ≺ z' ∧ (∀ y, z' ≺ y → z ≺ y) ∧ ¬y ≺ z') by
      simpa [Semantics.Models, Satisfies];
    refine ⟨y, Rxy, by tauto, nRzy, z, Rxz, by tauto, nRyz⟩;

end definability


section canonicality

variable {S} [Entailment S (Formula ℕ)]
variable {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢]

open Formula.Kripke
open Entailment
open MaximalConsistentTableau
open canonicalModel

instance [Entailment.HasAxiomPoint3 𝓢] : (canonicalFrame 𝓢).IsPiecewiseStronglyConnected where
  ps_connected := by
    rintro x y z Rxy Rxz;
    by_contra hC;
    push Not at hC;
    rcases hC with ⟨nRyz, nRzy⟩;
    obtain ⟨φ, hφy, hφz⟩ := Set.not_subset.mp nRyz;
    obtain ⟨ψ, hψz, hψy⟩ := Set.not_subset.mp nRzy;
    apply x.neither (φ := □(□φ 🡒 ψ) ⋎ □(□ψ 🡒 φ));
    constructor;
    . exact iff_provable_mem₁.mp axiomPoint3! x;
    . apply iff_mem₂_or.mpr;
      constructor;
      . apply iff_mem₂_box.mpr;
        use y;
        constructor;
        . exact Rxy;
        . apply iff_mem₂_imp.mpr;
          constructor;
          . exact hφy;
          . exact iff_not_mem₁_mem₂.mp hψy;
      . apply iff_mem₂_box.mpr;
        use z;
        constructor;
        . exact Rxz;
        . apply iff_mem₂_imp.mpr;
          constructor;
          . exact hψz;
          . exact iff_not_mem₁_mem₂.mp hφz;

end canonicality

open Formula.Kripke

end Kripke

end LO.Modal
end