theorem
LO.Modal.Standard.Kripke.iff_boxdot_reflexive_closure
{α : Type u_2}
{p : LO.Modal.Standard.Formula α}
{F : LO.Kripke.Frame}
{V : LO.Kripke.Valuation F α}
{x : { Frame := F, Valuation := V }.World}
:
LO.Modal.Standard.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x (pᵇ) ↔ LO.Modal.Standard.Formula.Kripke.Satisfies { Frame := F^=, Valuation := V } x p
theorem
LO.Modal.Standard.Kripke.iff_frame_boxdot_reflexive_closure
{α : Type u_2}
{p : LO.Modal.Standard.Formula α}
{F : LO.Kripke.Frame}
:
theorem
LO.Modal.Standard.Kripke.iff_reflexivize_irreflexivize
{α : Type u_2}
{p : LO.Modal.Standard.Formula α}
{F : LO.Kripke.Frame}
(F_Refl : Reflexive F.Rel)
{x : F.World}
{V : LO.Kripke.Valuation F α}
:
LO.Modal.Standard.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p ↔ LO.Modal.Standard.Formula.Kripke.Satisfies { Frame := F^≠^=, Valuation := V } x p
theorem
LO.Modal.Standard.boxdotTranslatedGL_of_Grz
{α : Type u}
[DecidableEq α]
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Grz_of_boxdotTranslatedGL
{α : Type u}
[Inhabited α]
[DecidableEq α]
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.iff_Grz_boxdotTranslatedGL
{α : Type u}
[Inhabited α]
[DecidableEq α]
{p : LO.Modal.Standard.Formula α}
:
Equations
- LO.Modal.Standard.instBoxdotPropertyGrzGL = { bdp := ⋯ }