@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.serial : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.serial = {F : LO.Modal.Kripke.Frame | IsSerial F.World F.Rel}

instance LO.Modal.Hilbert.KD.Kripke.sound : Sound Hilbert.KD Kripke.FrameClass.serial

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

instance LO.Modal.Hilbert.KD.Kripke.canonical : Kripke.Canonical Hilbert.KD Kripke.FrameClass.serial

instance LO.Modal.Hilbert.KD.Kripke.complete : Complete Hilbert.KD Kripke.FrameClass.serial

theorem LO.Modal.Logic.KD.Kripke.serial : Logic.KD = Kripke.FrameClass.serial.logic

@[simp]

theorem LO.Modal.Logic.KD.proper_extension_of_K : Logic.K ⊂ Logic.KD