class LO.Modal.Kripke.Frame.IsS4Point4McK (F : Frame) extends IsRefl F.World F.Rel, IsTrans F.World F.Rel, F.SatisfiesSobocinskiCondition, F.SatisfiesMcKinseyCondition : Prop

• refl (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
• sobocinski ⦃x y z : F.World⦄ : x ≠ y → x ≺ y → x ≺ z → z ≺ y
• mckinsey (x : F.World) : ∃ (y : F.World), x ≺ y ∧ ∀ (z : F.World), y ≺ z → y = z

instance LO.Modal.Kripke.instIsS4Point3McKOfIsS4Point4McK {F : Frame} [F.IsS4Point4McK] : F.IsS4Point3McK

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.S4Point4McK : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.S4Point4McK = {F : LO.Modal.Kripke.Frame | F.IsS4Point4McK}

instance LO.Modal.Modal.S4Point4McK.Kripke.instSoundLogicNatFormulaFrameClassS4Point4McKS4Point4McK : Sound Modal.S4Point4McK Kripke.FrameClass.S4Point4McK

instance LO.Modal.Modal.S4Point4McK.Kripke.instConsistentFormulaNatLogicS4Point4McK : Entailment.Consistent Modal.S4Point4McK

instance LO.Modal.Modal.S4Point4McK.Kripke.instCanonicalLogicNatS4Point4McKS4Point4McK : Kripke.Canonical Modal.S4Point4McK Kripke.FrameClass.S4Point4McK

instance LO.Modal.Modal.S4Point4McK.Kripke.instCompleteLogicNatFormulaFrameClassS4Point4McKS4Point4McK : Complete Modal.S4Point4McK Kripke.FrameClass.S4Point4McK

instance LO.Modal.Modal.S4Point4McK.Kripke.instStrictlyWeakerThanFormulaNatLogicS4Point3McKS4Point4McK : Modal.S4Point3McK ⪱ Modal.S4Point4McK

instance LO.Modal.Modal.S4Point4McK.Kripke.instStrictlyWeakerThanFormulaNatLogicS4Point4S4Point4McK : Modal.S4Point4 ⪱ Modal.S4Point4McK