class LO.InterpretabilityLogic.Veltman.Frame.IsIL_R_W (F : Frame) extends F.IsIL, F.HasAxiomW, F.HasAxiomR : 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_W (w : F.World) : ConverseWellFounded fun (x1 x2 : F.World) => x1 ≺≺[w] x2
• S_R {x y z u v : F.World} : x ≺ y → y ≺ z → z ≺[x] u → u ≺ v → z ≺[y] v

@[reducible, inline]

abbrev LO.InterpretabilityLogic.Veltman.FrameClass.IL_R_W : FrameClass

Equations

• LO.InterpretabilityLogic.Veltman.FrameClass.IL_R_W = {F : LO.InterpretabilityLogic.Veltman.Frame | F.IsIL_R_W}

instance LO.InterpretabilityLogic.Veltman.instIsIL_R_WTrivialFrame : trivialFrame.IsIL_R_W

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

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

instance LO.InterpretabilityLogic.instStrictlyWeakerThanFormulaNatLogicIL_M₀_WIL_R_W : InterpretabilityLogic.IL_M₀_W ⪱ InterpretabilityLogic.IL_R_W

instance LO.InterpretabilityLogic.«IL_R ⪱ IL_R_W» : InterpretabilityLogic.IL_R ⪱ InterpretabilityLogic.IL_R_W