@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.preorder_sobocinski : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.preorder_sobocinski = {F : LO.Modal.Kripke.Frame | IsPreorder F.World F.Rel ∧ SatisfiesSobocinskiCondition F.World F.Rel}

Instances For

• LO.Modal.Hilbert.S4Point4.Kripke.canonical
• LO.Modal.Hilbert.S4Point4.Kripke.complete
• LO.Modal.Hilbert.S4Point4.Kripke.sound

instance LO.Modal.Hilbert.S4Point4.Kripke.sound : Sound Hilbert.S4Point4 Kripke.FrameClass.preorder_sobocinski

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

instance LO.Modal.Hilbert.S4Point4.Kripke.canonical : Kripke.Canonical Hilbert.S4Point4 Kripke.FrameClass.preorder_sobocinski

instance LO.Modal.Hilbert.S4Point4.Kripke.complete : Complete Hilbert.S4Point4 Kripke.FrameClass.preorder_sobocinski

theorem LO.Modal.Logic.S4Point4.Kripke.preorder_sobocinski : Logic.S4Point4 = Kripke.FrameClass.preorder_sobocinski.logic

@[simp]

theorem LO.Modal.Logic.S4Point4.proper_extension_of_S4Point3 : Logic.S4Point3 ⊂ Logic.S4Point4