class LO.InterpretabilityLogic.Veltman.Frame.IsILM (F : Frame) extends F.IsILMinus_J1_J2_J5, 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 {w x y z : F.World} : x ≺[w] y → y ≺ z → x ≺ z

@[reducible, inline]

abbrev LO.InterpretabilityLogic.Veltman.FrameClass.ILM : FrameClass

Equations

• LO.InterpretabilityLogic.Veltman.FrameClass.ILM = {F : LO.InterpretabilityLogic.Veltman.Frame | F.IsILM}

instance LO.InterpretabilityLogic.Veltman.instIsILMTrivialFrame : trivialFrame.IsILM

instance LO.InterpretabilityLogic.ILM.Veltman.sound : Sound InterpretabilityLogic.ILM Veltman.FrameClass.ILM

instance LO.InterpretabilityLogic.ILM.instConsistentFormulaNatLogic : Entailment.Consistent InterpretabilityLogic.ILM

instance LO.InterpretabilityLogic.instStrictlyWeakerThanFormulaNatLogicILILM : InterpretabilityLogic.IL ⪱ InterpretabilityLogic.ILM