@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveSymmetricFiniteFrameClass : FiniteFrameClass

Equations

• LO.Modal.Kripke.ReflexiveSymmetricFiniteFrameClass = {F : LO.Modal.Kripke.FiniteFrame | Reflexive F.Rel ∧ Symmetric F.Rel}

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveFiniteFrameClass : FiniteFrameClass

Equations

• LO.Modal.Kripke.ReflexiveTransitiveFiniteFrameClass = {F : LO.Modal.Kripke.FiniteFrame | Reflexive F.Rel ∧ Transitive F.Rel}

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveSymmetricFiniteFrameClass : FiniteFrameClass

Equations

• LO.Modal.Kripke.ReflexiveTransitiveSymmetricFiniteFrameClass = {F : LO.Modal.Kripke.FiniteFrame | Reflexive F.Rel ∧ Transitive F.Rel ∧ Symmetric F.Rel}

def LO.Modal.Kripke.filterEquiv (M : Model) (T : Theory ℕ) [T.SubformulaClosed] (x y : M.World) : Prop

Equations

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

theorem LO.Modal.Kripke.filterEquiv.equivalence (M : Model) (T : Theory ℕ) [T.SubformulaClosed] : Equivalence (filterEquiv M T)

def LO.Modal.Kripke.FilterEqvSetoid (M : Model) (T : 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 (M : Model) (T : Theory ℕ) [T.SubformulaClosed] : Type

Equations

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

theorem LO.Modal.Kripke.FilterEqvQuotient.finite (M : Model) (T : Theory ℕ) [T.SubformulaClosed] (T_finite : Set.Finite T) : Finite (FilterEqvQuotient M T)

instance LO.Modal.Kripke.instNonemptyFilterEqvQuotient (M : Model) (T : Theory ℕ) [T.SubformulaClosed] : Nonempty (FilterEqvQuotient M T)

class LO.Modal.Kripke.FilterOf (FM M : Model) (T : Theory ℕ) [T.SubformulaClosed] : Prop

• def_world : FM.World = FilterEqvQuotient M T
• def_rel₁ {x y : M.World} : x ≺ y → cast ⋯ ⟦x⟧ ≺ cast ⋯ ⟦y⟧
• def_box {Qx Qy : FM.World} : Qx ≺ Qy → Quotient.lift₂ (fun (x y : M.World) => ∀ (φ : Formula ℕ), □φ ∈ T → x ⊧ □φ → y ⊧ φ) ⋯ (cast ⋯ Qx) (cast ⋯ Qy)
• def_valuation (Qx : FM.World) (a : ℕ) (ha : Formula.atom a ∈ T := by trivial) : FM.Val Qx a ↔ Quotient.lift (fun (x : M.World) => M.Val x a) ⋯ (cast ⋯ Qx)

theorem LO.Modal.Kripke.reflexive_filterOf_of_reflexive {M : Model} {T : Theory ℕ} [T.SubformulaClosed] {FM : Model} (h_filter : FilterOf FM M T) (hRefl : Reflexive M.Rel) : Reflexive FM.Rel

theorem LO.Modal.Kripke.serial_filterOf_of_serial {M : Model} {T : Theory ℕ} [T.SubformulaClosed] {FM : Model} (h_filter : FilterOf FM M T) (hSerial : Serial M.Rel) : Serial FM.Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.standardFilterationValuation (M : Model) (T : Theory ℕ) [T.SubformulaClosed] (Qx : 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.World) => M.Val x a) ⋯ Qx

@[reducible, inline]

abbrev LO.Modal.Kripke.coarsestFilterationFrame (M : Model) (T : Theory ℕ) [T.SubformulaClosed] : Frame

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.coarsestFilterationModel (M : Model) (T : Theory ℕ) [T.SubformulaClosed] : Model

Equations

• LO.Modal.Kripke.coarsestFilterationModel M T = { toFrame := LO.Modal.Kripke.coarsestFilterationFrame M T, Val := LO.Modal.Kripke.standardFilterationValuation M T }

instance LO.Modal.Kripke.coarsestFilterationModel.filterOf {M : Model} {T : Theory ℕ} [T.SubformulaClosed] : FilterOf (coarsestFilterationModel M T) M T

@[reducible, inline]

abbrev LO.Modal.Kripke.finestFilterationFrame (M : Model) (T : Theory ℕ) [T.SubformulaClosed] : Frame

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.finestFilterationModel (M : Model) (T : Theory ℕ) [T.SubformulaClosed] : Model

Equations

• LO.Modal.Kripke.finestFilterationModel M T = { toFrame := LO.Modal.Kripke.finestFilterationFrame M T, Val := LO.Modal.Kripke.standardFilterationValuation M T }

instance LO.Modal.Kripke.finestFilterationModel.filterOf {M : Model} {T : Theory ℕ} [T.SubformulaClosed] : FilterOf (finestFilterationModel M T) M T

theorem LO.Modal.Kripke.finestFilterationModel.symmetric_of_symmetric {M : Model} {T : Theory ℕ} [T.SubformulaClosed] (hSymm : Symmetric M.Rel) : Symmetric (finestFilterationModel M T).Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.finestFilterationTransitiveClosureModel (M : Model) (T : Theory ℕ) [T.SubformulaClosed] : Model

Equations

• LO.Modal.Kripke.finestFilterationTransitiveClosureModel M T = { toFrame := LO.Modal.Kripke.finestFilterationFrame M T^+, Val := LO.Modal.Kripke.standardFilterationValuation M T }

instance LO.Modal.Kripke.finestFilterationTransitiveClosureModel.filterOf {M : Model} {T : Theory ℕ} [T.SubformulaClosed] (M_trans : Transitive M.Rel) : FilterOf (finestFilterationTransitiveClosureModel M T) M T

theorem LO.Modal.Kripke.finestFilterationTransitiveClosureModel.transitive {M : Model} {T : Theory ℕ} [T.SubformulaClosed] : Transitive (finestFilterationTransitiveClosureModel M T).Rel

theorem LO.Modal.Kripke.finestFilterationTransitiveClosureModel.symmetric_of_symmetric {M : Model} {T : Theory ℕ} [T.SubformulaClosed] (M_symm : Symmetric M.Rel) : Symmetric (finestFilterationTransitiveClosureModel M T).Rel

theorem LO.Modal.Kripke.finestFilterationTransitiveClosureModel.reflexive_of_transitive_reflexive {M : Model} {T : Theory ℕ} [T.SubformulaClosed] (M_trans : Transitive M.Rel) (M_refl : Reflexive M.Rel) : Reflexive (finestFilterationTransitiveClosureModel M T).Rel

theorem LO.Modal.Kripke.filteration {M : Model} {T : Theory ℕ} [T.SubformulaClosed] (FM : Model) (filterOf : FilterOf FM M T) {x : M.World} {φ : Formula ℕ} (hs : φ ∈ T) : x ⊧ φ ↔ cast ⋯ ⟦x⟧ ⊧ φ

instance LO.Modal.Hilbert.K.Kripke.finite_complete : Complete (Hilbert.K ℕ) Kripke.AllFiniteFrameClass

instance LO.Modal.Hilbert.K.Kripke.ffp : Kripke.FiniteFrameProperty (Hilbert.K ℕ) Kripke.AllFiniteFrameClass

instance LO.Modal.Hilbert.KTB.Kripke.finite_complete : Complete (Hilbert.KTB ℕ) Kripke.ReflexiveSymmetricFiniteFrameClass

instance LO.Modal.Hilbert.KTB.Kripke.ffp : Kripke.FiniteFrameProperty (Hilbert.KTB ℕ) Kripke.ReflexiveSymmetricFiniteFrameClass

instance LO.Modal.Hilbert.S4.Kripke.finite_complete : Complete (Hilbert.S4 ℕ) Kripke.ReflexiveTransitiveFiniteFrameClass

instance LO.Modal.Hilbert.S4.Kripke.ffp : Kripke.FiniteFrameProperty (Hilbert.S4 ℕ) Kripke.ReflexiveTransitiveFiniteFrameClass

instance LO.Modal.Hilbert.KT4B.Kripke.finite_complete : Complete (Hilbert.KT4B ℕ) Kripke.ReflexiveTransitiveSymmetricFiniteFrameClass

instance LO.Modal.Hilbert.KT4B.Kripke.ffp : Kripke.FiniteFrameProperty (Hilbert.KT4B ℕ) Kripke.ReflexiveTransitiveSymmetricFiniteFrameClass