def LO.Modal.Neighborhood.filterEquiv (M : Model) (T : FormulaSet ℕ) [T.IsSubformulaClosed] (x y : M.World) : Prop

Equations

• LO.Modal.Neighborhood.filterEquiv M T x y = ∀ φ ∈ T, x ⊧ φ ↔ y ⊧ φ

theorem LO.Modal.Neighborhood.filterEquiv.equivalence (M : Model) (T : FormulaSet ℕ) [T.IsSubformulaClosed] : Equivalence (filterEquiv M T)

def LO.Modal.Neighborhood.FilterEqvSetoid (M : Model) (T : FormulaSet ℕ) [T.IsSubformulaClosed] : Setoid M.World

Equations

• LO.Modal.Neighborhood.FilterEqvSetoid M T = { r := LO.Modal.Neighborhood.filterEquiv M T, iseqv := ⋯ }

@[reducible, inline]

abbrev LO.Modal.Neighborhood.FilterEqvQuotient (M : Model) (T : FormulaSet ℕ) [T.IsSubformulaClosed] : Type

Equations

• LO.Modal.Neighborhood.FilterEqvQuotient M T = Quotient (LO.Modal.Neighborhood.FilterEqvSetoid M T)

theorem LO.Modal.Neighborhood.FilterEqvQuotient.iff_eq {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {x y : M.World} : ⟦x⟧ = ⟦y⟧ ↔ ∀ φ ∈ T, x ⊧ φ ↔ y ⊧ φ

theorem LO.Modal.Neighborhood.FilterEqvQuotient.finite {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] (T_finite : Set.Finite T) : Finite (FilterEqvQuotient M T)

instance LO.Modal.Neighborhood.FilterEqvQuotient.instNonempty {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] : Nonempty (FilterEqvQuotient M T)

def LO.Modal.Neighborhood.toFilterEquivSet {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] (X : Set M.World) : Set (FilterEqvQuotient M T)

Equations

• LO.Modal.Neighborhood.toFilterEquivSet X = {x : LO.Modal.Neighborhood.FilterEqvQuotient M T | ∃ x_1 ∈ X, ⟦x_1⟧ = x}

theorem LO.Modal.Neighborhood.toFilterEquivSet.mem_of_mem {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {X : Set M.World} {x : M.World} (hx : x ∈ X) : ⟦x⟧ ∈ toFilterEquivSet X

theorem LO.Modal.Neighborhood.toFilterEquivSet.iff_mem_truthset {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {x : M.World} {φ : Formula ℕ} (hφ : φ ∈ T) : x ∈ M.truthset φ ↔ ⟦x⟧ ∈ toFilterEquivSet (M.truthset φ)

@[simp]

theorem LO.Modal.Neighborhood.toFilterEquivSet.empty {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] : toFilterEquivSet ∅ = ∅

theorem LO.Modal.Neighborhood.toFilterEquivSet.union {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {X Y : Set M.World} : toFilterEquivSet (X ∪ Y) = toFilterEquivSet X ∪ toFilterEquivSet Y

theorem LO.Modal.Neighborhood.toFilterEquivSet.of_inter {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {X Y : Set M.World} : toFilterEquivSet (X ∩ Y) ⊆ toFilterEquivSet X ∩ toFilterEquivSet Y

theorem LO.Modal.Neighborhood.toFilterEquivSet.compl_truthset {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {φ : Formula ℕ} (hφ : φ ∈ T) : toFilterEquivSet (M.truthset φ)ᶜ = (toFilterEquivSet (M.truthset φ))ᶜ

theorem LO.Modal.Neighborhood.toFilterEquivSet.subset_original_truthset_of_subset {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {φ ψ : Formula ℕ} (hψ : ψ ∈ T) (h : toFilterEquivSet (M.truthset φ) ⊆ toFilterEquivSet (M.truthset ψ)) : M.truthset φ ⊆ M.truthset ψ

theorem LO.Modal.Neighborhood.toFilterEquivSet.eq_original_truthset_of_eq {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {φ ψ : Formula ℕ} (hφ : φ ∈ T) (hψ : ψ ∈ T) (h : toFilterEquivSet (M.truthset φ) = toFilterEquivSet (M.truthset ψ)) : M.truthset φ = M.truthset ψ

@[simp]

theorem LO.Modal.Neighborhood.toFilterEquivSet.eq_univ {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] : toFilterEquivSet Set.univ = Set.univ

@[simp]

theorem LO.Modal.Neighborhood.toFilterEquivSet.contains_unit {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] [M.ContainsUnit] : toFilterEquivSet (M.truthset (□⊤)) = Set.univ

theorem LO.Modal.Neighborhood.toFilterEquivSet.trans_truthset {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {φ : Formula ℕ} [M.IsTransitive] : toFilterEquivSet (M.truthset (□φ)) ⊆ toFilterEquivSet (M.truthset (□□φ))

theorem LO.Modal.Neighborhood.toFilterEquivSet.refl_truthset {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {φ : Formula ℕ} [M.IsReflexive] : toFilterEquivSet (M.truthset (□φ)) ⊆ toFilterEquivSet (M.truthset φ)

theorem LO.Modal.Neighborhood.toFilterEquivSet.mono'_truthset {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {φ ψ : Formula ℕ} [M.IsMonotonic] (hψ : ψ ∈ T) (h : toFilterEquivSet (M.truthset φ) ⊆ toFilterEquivSet (M.truthset ψ)) : toFilterEquivSet (M.truthset (□φ)) ⊆ toFilterEquivSet (M.truthset (□ψ))

structure LO.Modal.Neighborhood.Filtration (M : Model) (T : FormulaSet ℕ) [T.IsSubformulaClosed] : Type

• B : Set (FilterEqvQuotient M T) → Set (FilterEqvQuotient M T)
• B_def (φ : Formula ℕ) : □φ ∈ T → self.B (toFilterEquivSet (M.truthset φ)) = toFilterEquivSet (M.box (M.truthset φ))
• V : ℕ → Set (FilterEqvQuotient M T)
• V_def (a : ℕ) : self.V a = toFilterEquivSet (M.truthset (Formula.atom a))

def LO.Modal.Neighborhood.Filtration.toModel {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] (Fi : Filtration M T) : Model

Equations

• Fi.toModel = { toFrame := LO.Modal.Neighborhood.Frame.mk_ℬ (LO.Modal.Neighborhood.FilterEqvQuotient M T) Fi.B, Val := Fi.V }

@[simp]

theorem LO.Modal.Neighborhood.Filtration.toModel_def {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {Fi : Filtration M T} {X : Set Fi.toModel.World} : Fi.toModel.box X = Fi.B X

theorem LO.Modal.Neighborhood.Filtration.filtration {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] (Fi : Filtration M T) (φ : Formula ℕ) (hφ : φ ∈ T) : Fi.toModel.truthset φ = toFilterEquivSet (M.truthset φ)

theorem LO.Modal.Neighborhood.Filtration.filtration_satisfies {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] (Fi : Filtration M T) (φ : Formula ℕ) (hφ : φ ∈ T) {x : M.World} : Formula.Neighborhood.Satisfies Fi.toModel ⟦x⟧ φ ↔ x ⊧ φ

theorem LO.Modal.Neighborhood.Filtration.truthlemma {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] (Fi : Filtration M T) {φ ψ : Formula ℕ} (hφ : φ ∈ T) (hψ : ψ ∈ T) : Fi.toModel.truthset φ = Fi.toModel.truthset ψ ↔ toFilterEquivSet (M.truthset φ) = toFilterEquivSet (M.truthset ψ)

theorem LO.Modal.Neighborhood.Filtration.iff_mem_toModel_box_mem_B {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {Y : Set (FilterEqvQuotient M T)} {W : Quot ⇑(FilterEqvSetoid M T)} {Fi : Filtration M T} : W ∈ Fi.toModel.box Y ↔ W ∈ Fi.B Y

theorem LO.Modal.Neighborhood.Filtration.box_in_out {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {φ : Formula ℕ} {Fi : Filtration M T} (hφ : □φ ∈ T) : Fi.B (toFilterEquivSet (M.truthset φ)) = toFilterEquivSet (M.truthset (□φ))

theorem LO.Modal.Neighborhood.Filtration.mem_box_in_out {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {φ : Formula ℕ} {Fi : Filtration M T} {X : FilterEqvQuotient M T} (hψ : □φ ∈ T) : X ∈ Fi.B (toFilterEquivSet (M.truthset φ)) ↔ X ∈ toFilterEquivSet (M.truthset (□φ))

theorem LO.Modal.Neighborhood.Filtration.transitive_lemma {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {φ ψ : Formula ℕ} (hφ : φ ∈ T) (hψ : □ψ ∈ T) (Fi : Filtration M T) (h : toFilterEquivSet (M.truthset φ) = Fi.B (toFilterEquivSet (M.truthset ψ))) : toFilterEquivSet (M.truthset (□φ)) = toFilterEquivSet (M.truthset (□□ψ))

def LO.Modal.Neighborhood.minimalFiltration (M : Model) (T : FormulaSet ℕ) [T.IsSubformulaClosed] : Filtration M T

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Modal.Neighborhood.minimalFiltration.iff_mem_B {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {X : Set (FilterEqvQuotient M T)} {W : FilterEqvQuotient M T} : W ∈ (minimalFiltration M T).B X ↔ ∃ (φ : Formula ℕ), □φ ∈ T ∧ X = toFilterEquivSet (M.truthset φ) ∧ W ∈ toFilterEquivSet (M.truthset (□φ))

def LO.Modal.Neighborhood.transitiveFiltration (M : Model) [M.IsTransitive] (T : FormulaSet ℕ) [T.IsSubformulaClosed] : Filtration M T

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Modal.Neighborhood.transitiveFiltration.iff_mem_B {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] [M.IsTransitive] {X : Set (FilterEqvQuotient M T)} {W : FilterEqvQuotient M T} : W ∈ (transitiveFiltration M T).B X ↔ (∃ (φ : Formula ℕ), □φ ∈ T ∧ X = toFilterEquivSet (M.truthset φ) ∧ W ∈ toFilterEquivSet (M.truthset (□φ))) ∨ ∃ (φ : Formula ℕ), □φ ∈ T ∧ X = toFilterEquivSet (M.truthset (□φ)) ∧ W ∈ toFilterEquivSet (M.truthset (□φ))

instance LO.Modal.Neighborhood.transitiveFiltration.isTransitive {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] [M.IsTransitive] : (transitiveFiltration M T).toModel.IsTransitive

instance LO.Modal.Neighborhood.transitiveFiltration.isReflexive {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] [M.IsTransitive] [M.IsReflexive] : (transitiveFiltration M T).toModel.IsReflexive

instance LO.Modal.Neighborhood.transitiveFiltration.containsUnit {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] [M.IsTransitive] [M.ContainsUnit] (hT : □⊤ ∈ T) : (transitiveFiltration M T).toModel.ContainsUnit

def LO.Modal.Neighborhood.supplementedTransitiveFiltration (M : Model) [M.IsMonotonic] [M.IsTransitive] (T : FormulaSet ℕ) [T.IsSubformulaClosed] : Filtration M T

Equations

• One or more equations did not get rendered due to their size.

instance LO.Modal.Neighborhood.supplementedTransitiveFiltration.isMonotonic {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] [M.IsMonotonic] [M.IsTransitive] : (supplementedTransitiveFiltration M T).toModel.IsMonotonic

instance LO.Modal.Neighborhood.supplementedTransitiveFiltration.isTransitive {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] [M.IsMonotonic] [M.IsTransitive] : (supplementedTransitiveFiltration M T).toModel.IsTransitive

instance LO.Modal.Neighborhood.supplementedTransitiveFiltration.isReflexive {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] [M.IsMonotonic] [M.IsTransitive] [M.IsReflexive] : (supplementedTransitiveFiltration M T).toModel.IsReflexive

instance LO.Modal.Neighborhood.supplementedTransitiveFiltration.containsUnit {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] [M.IsMonotonic] [M.IsTransitive] [M.ContainsUnit] (hT : □⊤ ∈ T) : (supplementedTransitiveFiltration M T).toModel.ContainsUnit

def LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration (M : Model) [M.IsMonotonic] [M.IsTransitive] [M.IsRegular] (T : FormulaSet ℕ) [T.IsSubformulaClosed] (hT : Set.Finite T) : Filtration M T

Equations

• One or more equations did not get rendered due to their size.

instance LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration.isRegular {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {T_finite : Set.Finite T} [M.IsMonotonic] [M.IsTransitive] [M.IsRegular] : (quasiFilteringTransitiveFiltration M T T_finite).toModel.IsRegular

instance LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration.isMonotonic {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {T_finite : Set.Finite T} [M.IsMonotonic] [M.IsTransitive] [M.IsRegular] : (quasiFilteringTransitiveFiltration M T T_finite).toModel.IsMonotonic

instance LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration.isTransitive {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {T_finite : Set.Finite T} [M.IsMonotonic] [M.IsTransitive] [M.IsRegular] : (quasiFilteringTransitiveFiltration M T T_finite).toModel.IsTransitive

instance LO.Modal.Neighborhood.quasiFilteringTransitiveFiltration.containsUnit {M : Model} {T : FormulaSet ℕ} [T.IsSubformulaClosed] {T_finite : Set.Finite T} [M.IsMonotonic] [M.IsTransitive] [M.IsRegular] [M.ContainsUnit] (hT : □⊤ ∈ T) : (quasiFilteringTransitiveFiltration M T T_finite).toModel.ContainsUnit