class LO.Modal.Kripke.Frame.IsS4Point4 (F : Frame) extends IsRefl F.World F.Rel, IsTrans F.World F.Rel, F.SatisfiesSobocinskiCondition : 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

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.S4Point4 : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.S4Point4 = {F : LO.Modal.Kripke.Frame | F.IsS4Point4}

instance LO.Modal.Kripke.instIsS4Point3OfIsS4Point4 {F : Frame} [F.IsS4Point4] : F.IsS4Point3

instance LO.Modal.Hilbert.S4Point4.Kripke.instSoundNormalNatFormulaFrameClassS4Point4 : Sound Hilbert.S4Point4 Kripke.FrameClass.S4Point4

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

instance LO.Modal.Hilbert.S4Point4.Kripke.instCanonicalNormalNatS4Point4 : Kripke.Canonical Hilbert.S4Point4 Kripke.FrameClass.S4Point4

instance LO.Modal.Hilbert.S4Point4.Kripke.instCompleteNormalNatFormulaFrameClassS4Point4 : Complete Hilbert.S4Point4 Kripke.FrameClass.S4Point4

instance LO.Modal.Hilbert.S4Point4.Kripke.instStrictlyWeakerThanFormulaNatNormalS4Point3 : Hilbert.S4Point3 ⪱ Hilbert.S4Point4

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicS4Point3S4Point4 : Modal.S4Point3 ⪱ Modal.S4Point4