class LO.Modal.Kripke.Frame.IsS4Point4 (F : Frame) extends IsRefl F.World F.Rel, IsTrans F.World F.Rel, F.SatisfiesSobocinskiCondition : Prop

• refl (a : F.World) : F.Rel a a
• trans (a b c : F.World) : F.Rel a b → F.Rel b c → F.Rel a c
• sobocinski ⦃x y z : F.World⦄ : x ≠ y → x ≺ y → x ≺ z → z ≺ y

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.S4Point4 : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.S4Point4 = {F : LO.Modal.Kripke.Frame | F.IsS4Point4}

instance LO.Modal.Kripke.instIsS4Point3OfIsS4Point4 {F : Frame} [F.IsS4Point4] : F.IsS4Point3

instance LO.Modal.Modal.S4Point4.Kripke.instSoundLogicNatFormulaFrameClassS4Point4S4Point4 : Sound Modal.S4Point4 Kripke.FrameClass.S4Point4

instance LO.Modal.Modal.S4Point4.Kripke.instConsistentFormulaNatLogicS4Point4 : Entailment.Consistent Modal.S4Point4

instance LO.Modal.Modal.S4Point4.Kripke.instCanonicalLogicNatS4Point4S4Point4 : Kripke.Canonical Modal.S4Point4 Kripke.FrameClass.S4Point4

instance LO.Modal.Modal.S4Point4.Kripke.instCompleteLogicNatFormulaFrameClassS4Point4S4Point4 : Complete Modal.S4Point4 Kripke.FrameClass.S4Point4

instance LO.Modal.Modal.S4Point4.Kripke.instStrictlyWeakerThanFormulaNatLogicS4Point3S4Point4 : Modal.S4Point3 ⪱ Modal.S4Point4