@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.finite_strict_linear_order : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.finite_strict_linear_order = {F : LO.Modal.Kripke.Frame | Finite F.World ∧ IsStrictOrder F.World F.Rel ∧ IsWeakConnected F.World F.Rel}

Instances For

• LO.Modal.Hilbert.GLPoint3.Kripke.finite_complete
• LO.Modal.Hilbert.GLPoint3.Kripke.finite_sound

instance LO.Modal.Hilbert.GLPoint3.Kripke.finite_sound : Sound Hilbert.GLPoint3 Kripke.FrameClass.finite_strict_linear_order

instance LO.Modal.Hilbert.GLPoint3.Kripke.consistent : Entailment.Consistent Hilbert.GLPoint3

instance LO.Modal.Hilbert.GLPoint3.Kripke.finite_complete : Complete Hilbert.GLPoint3 Kripke.FrameClass.finite_strict_linear_order

theorem LO.Modal.Logic.GLPoint3.Kripke.finite_strict_linear_order : Logic.GLPoint3 = Kripke.FrameClass.finite_strict_linear_order.logic

theorem LO.Modal.Logic.GLPoint3.proper_extension_of_GL : Logic.GL ⊂ Logic.GLPoint3

theorem LO.Modal.Logic.GLPoint3.proper_extension_of_K4Point3 : Logic.K4Point3 ⊂ Logic.GLPoint3