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

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

class LO.Modal.Kripke.Frame.IsFiniteKTB (F : Frame) extends F.IsFinite, F.IsKTB : Prop

• world_finite : Finite F.World
• refl (a : F.World) : F.Rel a a
• symm (a b : F.World) : F.Rel a b → F.Rel b a

instance LO.Modal.Kripke.instIsKDBOfIsKTB {F : Frame} [F.IsKTB] : F.IsKDB

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.KTB : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.KTB = {F : LO.Modal.Kripke.Frame | F.IsKTB}

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.finite_KTB : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.finite_KTB = {F : LO.Modal.Kripke.Frame | F.IsFiniteKTB}

instance LO.Modal.instSoundLogicNatFormulaFrameClassKTBKTB : Sound Modal.KTB Kripke.FrameClass.KTB

instance LO.Modal.instConsistentFormulaNatLogicKTB : Entailment.Consistent Modal.KTB

instance LO.Modal.instCanonicalLogicNatKTBKTB : Kripke.Canonical Modal.KTB Kripke.FrameClass.KTB

instance LO.Modal.instCompleteLogicNatFormulaFrameClassKTBFinite_KTB : Complete Modal.KTB Kripke.FrameClass.finite_KTB

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicKTKTB : Modal.KT ⪱ Modal.KTB

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicKDBKTB : Modal.KDB ⪱ Modal.KTB