Documentation

Logic.Modal.Standard.Kripke.S5

source
theorem LO.Modal.Standard.Kripke.Frame.PointGenerated.rel_universal {F : LO.Modal.Standard.Kripke.Frame} {r : F.World} (F_refl : Reflexive F.Rel) (F_eucl : Euclidean F.Rel) :
Universal (F↾r).Rel
source
@[reducible, inline]
abbrev LO.Modal.Standard.Kripke.UniversalFrameClass :
LO.Modal.Standard.Kripke.FrameClass
Equations
Instances For
    source
    theorem LO.Modal.Standard.Kripke.iff_Universal_ReflexiveEuclidean_validOnFrameClass :
    ∀ {α : Type u_1} {p : LO.Modal.Standard.Formula α}, LO.Modal.Standard.Kripke.UniversalFrameClass.alt ⊧ p ↔ LO.Modal.Standard.Kripke.ReflexiveEuclideanFrameClass.alt ⊧ p
    source
    instance LO.Modal.Standard.Kripke.S5_complete_universal {α : Type u} [Inhabited α] [DecidableEq α] :
    LO.Complete 𝐒𝟓 LO.Modal.Standard.Kripke.UniversalFrameClass.alt
    Equations
    • ⋯ = ⋯