class LO.Modal.Kripke.Frame.IsKB4 (F : Frame) extends Std.Symm F.Rel, IsTrans F.World F.Rel : Prop

• symm (a b : F.World) : F.Rel a b → F.Rel b a
• trans (a b c : F.World) : F.Rel a b → F.Rel b c → F.Rel a c

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.KB4 : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.KB4 = {F : LO.Modal.Kripke.Frame | F.IsKB4}

instance LO.Modal.Kripke.instIsK45OfIsKB4 {F : Frame} [F.IsKB4] : F.IsK45

instance LO.Modal.instSoundLogicNatFormulaFrameClassKB4KB4 : Sound Modal.KB4 Kripke.FrameClass.KB4

instance LO.Modal.instConsistentFormulaNatLogicKB4 : Entailment.Consistent Modal.KB4

instance LO.Modal.instCanonicalLogicNatKB4KB4 : Kripke.Canonical Modal.KB4 Kripke.FrameClass.KB4

instance LO.Modal.instCompleteLogicNatFormulaFrameClassKB4KB4 : Complete Modal.KB4 Kripke.FrameClass.KB4

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicK45KB4 : Modal.K45 ⪱ Modal.KB4

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicKBKB4 : Modal.KB ⪱ Modal.KB4