|
| 1 | +module |
| 2 | + |
| 3 | +public import Foundation.Modal.Neighborhood.Completeness |
| 4 | + |
| 5 | +@[expose] public section |
| 6 | + |
| 7 | +namespace LO.Modal.Neighborhood |
| 8 | + |
| 9 | +open Formula.Neighborhood |
| 10 | + |
| 11 | +variable {F : Frame} |
| 12 | + |
| 13 | +class Frame.IsRegular (F : Frame) : Prop where |
| 14 | + regular : ∀ X Y, (F.box X) ∩ (F.box Y) ⊆ F.box (X ∩ Y) |
| 15 | + |
| 16 | +lemma Frame.regular [Frame.IsRegular F] {X Y : Set F} : (F.box X) ∩ (F.box Y) ⊆ F.box (X ∩ Y) := by apply IsRegular.regular |
| 17 | + |
| 18 | +open Classical in |
| 19 | +lemma Frame.regular_finset_iUnion [F.IsRegular] (s : Finset (Set F)) (hs : s.Nonempty) : (⋂ i ∈ s, F.box i) ⊆ F.box (⋂ i ∈ s, i) := by |
| 20 | + induction s using Finset.induction_on with |
| 21 | + | empty => simp_all; |
| 22 | + | insert i s hi ih => |
| 23 | + wlog hs : s.Nonempty; |
| 24 | + . simp_all; |
| 25 | + replace ih := ih hs; |
| 26 | + apply Set.Subset.trans ?_ (show i ∩ ⋂ j ∈ s, j = ⋂ j ∈ insert i s, j by simp ▸ F.regular (X := i) (Y := ⋂ j ∈ s, j)); |
| 27 | + suffices (F.box i) ∩ (⋂ j ∈ s, F.box j) ⊆ F.box (⋂ j ∈ s, j) by simpa; |
| 28 | + grind; |
| 29 | + |
| 30 | +open Classical in |
| 31 | +lemma Frame.regular_finite_iUnion [F.IsRegular] {ι} [h : Fintype ι] [Nonempty ι] {X : ι → Set F} : (⋂ i : ι, F.box (X i)) ⊆ F.box (⋂ i : ι, X i) := by |
| 32 | + simpa using Frame.regular_finset_iUnion (Finset.univ.image X) (by simp); |
| 33 | + |
| 34 | +instance : Frame.simple_blackhole.IsRegular := ⟨by |
| 35 | + intro X Y e; |
| 36 | + simp_all; |
| 37 | +⟩ |
| 38 | + |
| 39 | +@[simp] |
| 40 | +lemma valid_axiomC_of_isRegular [F.IsRegular] : F ⊧ Axioms.C (.atom 0) (.atom 1) := by |
| 41 | + intro V x; |
| 42 | + simp only [ |
| 43 | + Satisfies, Model.truthset.eq_imp, Model.truthset.eq_and, Model.truthset.eq_box, |
| 44 | + Model.truthset.eq_atom, Set.mem_union, Set.mem_compl_iff, Set.mem_inter_iff, Set.mem_setOf_eq |
| 45 | + ]; |
| 46 | + apply not_or_of_imp; |
| 47 | + rintro ⟨h₁, h₂⟩; |
| 48 | + apply F.regular; |
| 49 | + constructor; |
| 50 | + . apply h₁; |
| 51 | + . apply h₂; |
| 52 | + |
| 53 | +lemma isRegular_of_valid_axiomC (h : F ⊧ Axioms.C (.atom 0) (.atom 1)) : F.IsRegular := by |
| 54 | + constructor; |
| 55 | + rintro X Y w ⟨hwX, hwY⟩; |
| 56 | + have := @h (λ a => match a with | 0 => X | 1 => Y | _ => ∅) w; |
| 57 | + simp [Satisfies] at this; |
| 58 | + grind; |
| 59 | + |
| 60 | +section |
| 61 | + |
| 62 | +variable [Entailment S (Formula ℕ)] |
| 63 | +variable {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.E 𝓢] |
| 64 | + |
| 65 | +open Entailment |
| 66 | +open MaximalConsistentSet |
| 67 | + |
| 68 | +instance [Entailment.HasAxiomC 𝓢] : (basicCanonicity 𝓢).toModel.IsRegular := by |
| 69 | + constructor; |
| 70 | + rintro X Y A ⟨hX, hY⟩; |
| 71 | + obtain ⟨φ, rfl, hφ⟩ := basicCanonicity.iff_mem_box_exists_fml.mp hX; |
| 72 | + obtain ⟨ψ, rfl, hψ⟩ := basicCanonicity.iff_mem_box_exists_fml.mp hY; |
| 73 | + suffices A ∈ proofset 𝓢 (□(φ ⋏ ψ)) by |
| 74 | + rwa [(show proofset 𝓢 φ ∩ proofset 𝓢 ψ = proofset 𝓢 (φ ⋏ ψ) by grind), Canonicity.box_proofset]; |
| 75 | + apply proofset.imp_subset |>.mp (show 𝓢 ⊢ □φ ⋏ □ψ 🡒 □(φ ⋏ ψ) by simp); |
| 76 | + rw [proofset.eq_and] |
| 77 | + tauto; |
| 78 | + |
| 79 | +end |
| 80 | + |
| 81 | +end LO.Modal.Neighborhood |
| 82 | +end |
0 commit comments