class LO.Modal.Kripke.Frame.IsInfiniteGL (F : Frame) extends IsTrans F.World F.Rel, IsConverseWellFounded F.World F.Rel : Prop

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

class LO.Modal.Kripke.Frame.IsFiniteGL (F : Frame) extends F.IsFinite, F.IsStrictPreorder : Prop

• world_finite : Finite F.World
• irrefl (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

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.infinite_GL : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.infinite_GL = {F : LO.Modal.Kripke.Frame | F.IsInfiniteGL}

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.finite_GL : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.finite_GL = {F : LO.Modal.Kripke.Frame | F.IsFiniteGL}

instance LO.Modal.Kripke.instIsFiniteGLBlackpoint : blackpoint.IsFiniteGL

instance LO.Modal.instSoundLogicNatFormulaFrameClassGLInfinite_GL : Sound Modal.GL Kripke.FrameClass.infinite_GL

instance LO.Modal.instSoundLogicNatFormulaFrameClassGLFinite_GL : Sound Modal.GL Kripke.FrameClass.finite_GL

instance LO.Modal.instConsistentFormulaNatLogicGL : Entailment.Consistent Modal.GL

instance LO.Modal.instConsistentFormulaNatLogicGL_1 : Entailment.Consistent Modal.GL