Documentation

Foundation.InterpretabilityLogic.Veltman.Logic.IL_M

class LO.InterpretabilityLogic.Veltman.Frame.IsILM (F : Frame) extends F.IsIL, F.HasAxiomM :

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

Instances

@[reducible, inline]

abbrev LO.InterpretabilityLogic.Veltman.FrameClass.IL_M :

Equations

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

Instances For

instance LO.InterpretabilityLogic.Veltman.instIsILMTrivialFrame :

trivialFrame.IsILM

instance LO.InterpretabilityLogic.ILM.Veltman.sound :

Sound InterpretabilityLogic.IL_M Veltman.FrameClass.IL_M

instance LO.InterpretabilityLogic.ILM.instConsistentFormulaNatLogicIL_M :

Entailment.Consistent InterpretabilityLogic.IL_M

instance LO.InterpretabilityLogic.instStrictlyWeakerThanFormulaNatLogicIL_R_WIL_M :

InterpretabilityLogic.IL_R_W ⪱ InterpretabilityLogic.IL_M