def LO.Modal.Kripke.filterEquiv {α : Type u} (M : LO.Kripke.Model α) (T : LO.Modal.Theory α) [T.SubformulaClosed] (x : M.World) (y : M.World) : Prop

Equations

• LO.Modal.Kripke.filterEquiv M T x y = ∀ (p : LO.Modal.Formula α), autoParam (p ∈ T) _auto✝ → (x ⊧ p ↔ y ⊧ p)

theorem LO.Modal.Kripke.filterEquiv.equivalence {α : Type u} (M : LO.Kripke.Model α) (T : LO.Modal.Theory α) [T.SubformulaClosed] : Equivalence (LO.Modal.Kripke.filterEquiv M T)

def LO.Modal.Kripke.FilterEqvSetoid {α : Type u} (M : LO.Kripke.Model α) (T : LO.Modal.Theory α) [T.SubformulaClosed] : Setoid M.World

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.FilterEqvQuotient {α : Type u} (M : LO.Kripke.Model α) (T : LO.Modal.Theory α) [T.SubformulaClosed] : Type u_1

Equations

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

theorem LO.Modal.Kripke.FilterEqvQuotient.finite {α : Type u} (M : LO.Kripke.Model α) (T : LO.Modal.Theory α) [T.SubformulaClosed] (T_finite : Set.Finite T) : Finite (LO.Modal.Kripke.FilterEqvQuotient M T)

instance LO.Modal.Kripke.instNonemptyFilterEqvQuotient {α : Type u} (M : LO.Kripke.Model α) (T : LO.Modal.Theory α) [T.SubformulaClosed] : Nonempty (LO.Modal.Kripke.FilterEqvQuotient M T)

Equations

• ⋯ = ⋯

class LO.Modal.Kripke.FilterOf {α : Type u} (FM : LO.Kripke.Model α) (M : LO.Kripke.Model α) (T : LO.Modal.Theory α) [T.SubformulaClosed] : Type

• def_world : FM.World = LO.Modal.Kripke.FilterEqvQuotient M T
• def_rel₁ : ∀ {x y : M.Frame.World}, x ≺ y → cast ⋯ ⟦x⟧ ≺ cast ⋯ ⟦y⟧
• def_box : ∀ {Qx Qy : FM.World}, Qx ≺ Qy → Quotient.lift₂ (fun (x y : M.World) => ∀ (p : LO.Modal.Formula α), □p ∈ T → x ⊧ □p → y ⊧ p) ⋯ (cast ⋯ Qx) (cast ⋯ Qy)
• def_valuation : ∀ (Qx : FM.Frame.World) (a : α) (ha : autoParam (LO.Modal.Formula.atom a ∈ T) _auto✝), FM.Valuation Qx a ↔ Quotient.lift (fun (x : M.Frame.World) => M.Valuation x a) ⋯ (cast ⋯ Qx)

@[simp]

theorem LO.Modal.Kripke.FilterOf.def_world {α : Type u} {FM : LO.Kripke.Model α} {M : LO.Kripke.Model α} {T : LO.Modal.Theory α} [T.SubformulaClosed] [self : LO.Modal.Kripke.FilterOf FM M T] : FM.World = LO.Modal.Kripke.FilterEqvQuotient M T

theorem LO.Modal.Kripke.FilterOf.def_rel₁ {α : Type u} {FM : LO.Kripke.Model α} {M : LO.Kripke.Model α} {T : LO.Modal.Theory α} [T.SubformulaClosed] [self : LO.Modal.Kripke.FilterOf FM M T] {x : M.Frame.World} {y : M.Frame.World} : x ≺ y → cast ⋯ ⟦x⟧ ≺ cast ⋯ ⟦y⟧

theorem LO.Modal.Kripke.FilterOf.def_box {α : Type u} {FM : LO.Kripke.Model α} {M : LO.Kripke.Model α} {T : LO.Modal.Theory α} [T.SubformulaClosed] [self : LO.Modal.Kripke.FilterOf FM M T] {Qx : FM.World} {Qy : FM.World} : Qx ≺ Qy → Quotient.lift₂ (fun (x y : M.World) => ∀ (p : LO.Modal.Formula α), □p ∈ T → x ⊧ □p → y ⊧ p) ⋯ (cast ⋯ Qx) (cast ⋯ Qy)

theorem LO.Modal.Kripke.FilterOf.def_valuation {α : Type u} {FM : LO.Kripke.Model α} {M : LO.Kripke.Model α} {T : LO.Modal.Theory α} [T.SubformulaClosed] [self : LO.Modal.Kripke.FilterOf FM M T] (Qx : FM.Frame.World) (a : α) (ha : autoParam (LO.Modal.Formula.atom a ∈ T) _auto✝) : FM.Valuation Qx a ↔ Quotient.lift (fun (x : M.Frame.World) => M.Valuation x a) ⋯ (cast ⋯ Qx)

@[reducible, inline]

abbrev LO.Modal.Kripke.StandardFilterationValuation {α : Type u} (M : LO.Kripke.Model α) (T : LO.Modal.Theory α) [T.SubformulaClosed] (Qx : LO.Modal.Kripke.FilterEqvQuotient M T) (a : α) : Prop

Equations

• LO.Modal.Kripke.StandardFilterationValuation M T Qx a = ∀ (ha : LO.Modal.Formula.atom a ∈ T), Quotient.lift (fun (x : M.Frame.World) => M.Valuation x a) ⋯ Qx

@[reducible, inline]

abbrev LO.Modal.Kripke.FinestFilterationFrame {α : Type u} (M : LO.Kripke.Model α) (T : LO.Modal.Theory α) [T.SubformulaClosed] : LO.Kripke.Frame

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.FinestFilterationModel {α : Type u} (M : LO.Kripke.Model α) (T : LO.Modal.Theory α) [T.SubformulaClosed] : LO.Kripke.Model α

Equations

• LO.Modal.Kripke.FinestFilterationModel M T = { Frame := LO.Modal.Kripke.FinestFilterationFrame M T, Valuation := LO.Modal.Kripke.StandardFilterationValuation M T }

instance LO.Modal.Kripke.FinestFilterationModel.filterOf {α : Type u} {M : LO.Kripke.Model α} {T : LO.Modal.Theory α} [T.SubformulaClosed] : LO.Modal.Kripke.FilterOf (LO.Modal.Kripke.FinestFilterationModel M T) M T

Equations

• LO.Modal.Kripke.FinestFilterationModel.filterOf = { def_world := ⋯, def_rel₁ := ⋯, def_box := ⋯, def_valuation := ⋯ }

@[reducible, inline]

abbrev LO.Modal.Kripke.CoarsestFilterationFrame {α : Type u} (M : LO.Kripke.Model α) (T : LO.Modal.Theory α) [T.SubformulaClosed] : LO.Kripke.Frame

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.CoarsestFilterationModel {α : Type u} (M : LO.Kripke.Model α) (T : LO.Modal.Theory α) [T.SubformulaClosed] : LO.Kripke.Model α

Equations

• LO.Modal.Kripke.CoarsestFilterationModel M T = { Frame := LO.Modal.Kripke.CoarsestFilterationFrame M T, Valuation := LO.Modal.Kripke.StandardFilterationValuation M T }

instance LO.Modal.Kripke.CoarsestFilterationModel.filterOf {α : Type u} {M : LO.Kripke.Model α} {T : LO.Modal.Theory α} [T.SubformulaClosed] : LO.Modal.Kripke.FilterOf (LO.Modal.Kripke.CoarsestFilterationModel M T) M T

Equations

• LO.Modal.Kripke.CoarsestFilterationModel.filterOf = { def_world := ⋯, def_rel₁ := ⋯, def_box := ⋯, def_valuation := ⋯ }

theorem LO.Modal.Kripke.reflexive_filteration_model {α : Type u} {M : LO.Kripke.Model α} {T : LO.Modal.Theory α} [T.SubformulaClosed] {FM : LO.Kripke.Model α} (h_filter : LO.Modal.Kripke.FilterOf FM M T) (hRefl : Reflexive M.Frame.Rel) : Reflexive FM.Frame.Rel

theorem LO.Modal.Kripke.serial_filteration_model {α : Type u} {M : LO.Kripke.Model α} {T : LO.Modal.Theory α} [T.SubformulaClosed] {FM : LO.Kripke.Model α} (h_filter : LO.Modal.Kripke.FilterOf FM M T) (hSerial : Serial M.Frame.Rel) : Serial FM.Frame.Rel

theorem LO.Modal.Kripke.symmetric_finest_filteration_model {α : Type u} {M : LO.Kripke.Model α} {T : LO.Modal.Theory α} [T.SubformulaClosed] (hSymm : Symmetric M.Frame.Rel) : Symmetric (LO.Modal.Kripke.FinestFilterationModel M T).Frame.Rel

theorem LO.Modal.Kripke.filteration {α : Type u} {M : LO.Kripke.Model α} {T : LO.Modal.Theory α} [T.SubformulaClosed] (FM : LO.Kripke.Model α) (filterOf : LO.Modal.Kripke.FilterOf FM M T) {x : M.World} {p : LO.Modal.Formula α} (hs : autoParam (p ∈ T) _auto✝) : x ⊧ p ↔ cast ⋯ ⟦x⟧ ⊧ p

instance LO.Modal.Kripke.K_finite_complete {α : Type u} [DecidableEq α] : LO.Complete 𝐊 LO.Kripke.AllFrameClassꟳ#α

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.instFiniteFramePropertyKAllFrameClass {α : Type u} [DecidableEq α] : LO.Modal.Kripke.FiniteFrameProperty 𝐊 LO.Kripke.AllFrameClass

Equations

• LO.Modal.Kripke.instFiniteFramePropertyKAllFrameClass = LO.Modal.Kripke.FiniteFrameProperty.mk

instance LO.Modal.Kripke.KTB_finite_complete {α : Type u} [DecidableEq α] [Inhabited α] : LO.Complete 𝐊𝐓𝐁 LO.Kripke.ReflexiveSymmetricFrameClassꟳ#α

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.instFiniteFramePropertyKTBReflexiveSymmetricFrameClass {α : Type u} [DecidableEq α] [Inhabited α] : LO.Modal.Kripke.FiniteFrameProperty 𝐊𝐓𝐁 LO.Kripke.ReflexiveSymmetricFrameClass

Equations

• LO.Modal.Kripke.instFiniteFramePropertyKTBReflexiveSymmetricFrameClass = LO.Modal.Kripke.FiniteFrameProperty.mk

@[reducible, inline]

abbrev LO.Modal.Kripke.FinestFilterationTransitiveClosureModel {α : Type u} (M : LO.Kripke.Model α) (T : LO.Modal.Theory α) [T.SubformulaClosed] : LO.Kripke.Model α

Equations

• LO.Modal.Kripke.FinestFilterationTransitiveClosureModel M T = { Frame := LO.Modal.Kripke.FinestFilterationFrame M T^+, Valuation := LO.Modal.Kripke.StandardFilterationValuation M T }

instance LO.Modal.Kripke.FinestFilterationTransitiveClosureModel.filterOf {α : Type u} {M : LO.Kripke.Model α} (M_trans : Transitive M.Frame.Rel) {T : LO.Modal.Theory α} [T.SubformulaClosed] : LO.Modal.Kripke.FilterOf (LO.Modal.Kripke.FinestFilterationTransitiveClosureModel M T) M T

Equations

• LO.Modal.Kripke.FinestFilterationTransitiveClosureModel.filterOf M_trans = { def_world := ⋯, def_rel₁ := ⋯, def_box := ⋯, def_valuation := ⋯ }

theorem LO.Modal.Kripke.FinestFilterationTransitiveClosureModel.rel_transitive {α : Type u} {M : LO.Kripke.Model α} {T : LO.Modal.Theory α} [T.SubformulaClosed] : Transitive (LO.Modal.Kripke.FinestFilterationTransitiveClosureModel M T).Frame.Rel

theorem LO.Modal.Kripke.FinestFilterationTransitiveClosureModel.rel_symmetric {α : Type u} {M : LO.Kripke.Model α} {T : LO.Modal.Theory α} [T.SubformulaClosed] (M_symm : Symmetric M.Frame.Rel) : Symmetric (LO.Modal.Kripke.FinestFilterationTransitiveClosureModel M T).Frame.Rel

theorem LO.Modal.Kripke.FinestFilterationTransitiveClosureModel.rel_reflexive {α : Type u} {M : LO.Kripke.Model α} (M_trans : Transitive M.Frame.Rel) {T : LO.Modal.Theory α} [T.SubformulaClosed] (M_refl : Reflexive M.Frame.Rel) : Reflexive (LO.Modal.Kripke.FinestFilterationTransitiveClosureModel M T).Frame.Rel

instance LO.Modal.Kripke.S4_finite_complete {α : Type u} [DecidableEq α] [Inhabited α] : LO.Complete 𝐒𝟒 LO.Kripke.PreorderFrameClassꟳ#α

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.instFiniteFramePropertyS4PreorderFrameClass {α : Type u} [DecidableEq α] [Inhabited α] : LO.Modal.Kripke.FiniteFrameProperty 𝐒𝟒 LO.Kripke.PreorderFrameClass

Equations

• LO.Modal.Kripke.instFiniteFramePropertyS4PreorderFrameClass = LO.Modal.Kripke.FiniteFrameProperty.mk

instance LO.Modal.Kripke.KT4B_finite_complete {α : Type u} [DecidableEq α] [Inhabited α] : LO.Complete 𝐊𝐓𝟒𝐁 LO.Kripke.EquivalenceFrameClassꟳ#α

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.instFiniteFramePropertyKT4BEquivalenceFrameClass {α : Type u} [DecidableEq α] [Inhabited α] : LO.Modal.Kripke.FiniteFrameProperty 𝐊𝐓𝟒𝐁 LO.Kripke.EquivalenceFrameClass

Equations

• LO.Modal.Kripke.instFiniteFramePropertyKT4BEquivalenceFrameClass = LO.Modal.Kripke.FiniteFrameProperty.mk