class LO.InterpretabilityLogic.Veltman.Frame.IsIL_P₀ (F : Frame) extends F.IsIL, 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_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_P₀ : FrameClass

Equations

• LO.InterpretabilityLogic.Veltman.FrameClass.IL_P₀ = {F : LO.InterpretabilityLogic.Veltman.Frame | F.IsIL_P₀}

instance LO.InterpretabilityLogic.Veltman.instHasAxiomRTrivialFrame : trivialFrame.HasAxiomR

instance LO.InterpretabilityLogic.Veltman.instIsIL_P₀TrivialFrame : trivialFrame.IsIL_P₀

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

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

instance LO.InterpretabilityLogic.instStrictlyWeakerThanFormulaNatLogicILIL_P₀ : InterpretabilityLogic.IL ⪱ InterpretabilityLogic.IL_P₀