class LO.InterpretabilityLogic.Veltman.Frame.IsIL_M₀ (F : Frame) extends F.IsIL, F.HasAxiomM₀ : Prop

• S_J1 {w x : F.World} : w ≺ x → x ≺[w] x
• S_J4 {w x y : F.World} : x ≺[w] y → w ≺ y
• S_J2 {w x y z : F.World} : x ≺[w] y → y ≺[w] z → x ≺[w] z
• S_J5 {w x y : F.World} : w ≺ x → x ≺ y → x ≺[w] y
• S_M₀ {a b c d e : F.World} : a ≺ b → b ≺ c → c ≺[a] d → d ≺ e → b ≺ e

@[reducible, inline]

abbrev LO.InterpretabilityLogic.Veltman.FrameClass.IL_M₀ : FrameClass

Equations

• LO.InterpretabilityLogic.Veltman.FrameClass.IL_M₀ = {F : LO.InterpretabilityLogic.Veltman.Frame | F.IsIL_M₀}

instance LO.InterpretabilityLogic.Veltman.instIsIL_M₀TrivialFrame : trivialFrame.IsIL_M₀

instance LO.InterpretabilityLogic.IL_M₀.Veltman.sound : Sound InterpretabilityLogic.IL_M₀ Veltman.FrameClass.IL_M₀

instance LO.InterpretabilityLogic.IL_M₀.instConsistentFormulaNatLogic : Entailment.Consistent InterpretabilityLogic.IL_M₀

instance LO.InterpretabilityLogic.instStrictlyWeakerThanFormulaNatLogicILIL_M₀ : InterpretabilityLogic.IL ⪱ InterpretabilityLogic.IL_M₀