class LO.Modal.Kripke.Frame.IsKB5 (F : Frame) extends Std.Symm F.Rel, IsRightEuclidean F.Rel : Prop

• symm (a b : F.World) : F.Rel a b → F.Rel b a
• reucl : RightEuclidean F.Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.KB5 : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.KB5 = {F : LO.Modal.Kripke.Frame | F.IsKB5}

instance LO.Modal.instSoundLogicNatFormulaFrameClassKB5KB5 : Sound Modal.KB5 Kripke.FrameClass.KB5

instance LO.Modal.instConsistentFormulaNatLogicKB5 : Entailment.Consistent Modal.KB5

instance LO.Modal.instCanonicalLogicNatKB5KB5 : Kripke.Canonical Modal.KB5 Kripke.FrameClass.KB5

instance LO.Modal.instCompleteLogicNatFormulaFrameClassKB5KB5 : Complete Modal.KB5 Kripke.FrameClass.KB5