@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveSymmetricFiniteFrameClass : LO.Modal.Kripke.FiniteFrameClass

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveFiniteFrameClass : LO.Modal.Kripke.FiniteFrameClass

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveSymmetricFiniteFrameClass : LO.Modal.Kripke.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 : LO.Modal.Kripke.Model) (T : LO.Modal.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 : LO.Modal.Kripke.Model) (T : LO.Modal.Theory ℕ) [T.SubformulaClosed] : Equivalence (LO.Modal.Kripke.filterEquiv M T)

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

Equations

• ⋯ = ⋯

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

• def_world : FM.World = LO.Modal.Kripke.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) => ∀ (φ : LO.Modal.Formula ℕ), □φ ∈ T → x ⊧ □φ → y ⊧ φ) ⋯ (cast ⋯ Qx) (cast ⋯ Qy)
• def_valuation : ∀ (Qx : FM.World) (a : ℕ) (ha : autoParam (LO.Modal.Formula.atom a ∈ T) _auto✝), 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 : LO.Modal.Kripke.Model} {T : LO.Modal.Theory ℕ} [T.SubformulaClosed] {FM : LO.Modal.Kripke.Model} (h_filter : LO.Modal.Kripke.FilterOf FM M T) (hRefl : Reflexive M.Rel) : Reflexive FM.Rel

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

@[reducible, inline]

abbrev LO.Modal.Kripke.standardFilterationValuation (M : LO.Modal.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.World) => M.Val x a) ⋯ Qx

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.coarsestFilterationModel (M : LO.Modal.Kripke.Model) (T : LO.Modal.Theory ℕ) [T.SubformulaClosed] : LO.Modal.Kripke.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 : LO.Modal.Kripke.Model} {T : LO.Modal.Theory ℕ} [T.SubformulaClosed] : LO.Modal.Kripke.FilterOf (LO.Modal.Kripke.coarsestFilterationModel M T) M T

Equations

• ⋯ = ⋯

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.finestFilterationModel (M : LO.Modal.Kripke.Model) (T : LO.Modal.Theory ℕ) [T.SubformulaClosed] : LO.Modal.Kripke.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 : LO.Modal.Kripke.Model} {T : LO.Modal.Theory ℕ} [T.SubformulaClosed] : LO.Modal.Kripke.FilterOf (LO.Modal.Kripke.finestFilterationModel M T) M T

Equations

• ⋯ = ⋯

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

@[reducible, inline]

abbrev LO.Modal.Kripke.finestFilterationTransitiveClosureModel (M : LO.Modal.Kripke.Model) (T : LO.Modal.Theory ℕ) [T.SubformulaClosed] : LO.Modal.Kripke.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 : LO.Modal.Kripke.Model} {T : LO.Modal.Theory ℕ} [T.SubformulaClosed] (M_trans : Transitive M.Rel) : LO.Modal.Kripke.FilterOf (LO.Modal.Kripke.finestFilterationTransitiveClosureModel M T) M T

Equations

• ⋯ = ⋯

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

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

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

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

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

Equations

• LO.Modal.Hilbert.K.Kripke.finite_complete = ⋯

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

Equations

• LO.Modal.Hilbert.K.Kripke.ffp = ⋯

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

Equations

• LO.Modal.Hilbert.KTB.Kripke.finite_complete = ⋯

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

Equations

• LO.Modal.Hilbert.KTB.Kripke.ffp = ⋯

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

Equations

• LO.Modal.Hilbert.S4.Kripke.finite_complete = ⋯

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

Equations

• LO.Modal.Hilbert.S4.Kripke.ffp = ⋯

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

Equations

• LO.Modal.Hilbert.KT4B.Kripke.finite_complete = ⋯

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

Equations

• LO.Modal.Hilbert.KT4B.Kripke.ffp = ⋯