Documentation

Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J2Plus

@[reducible, inline]

abbrev LO.InterpretabilityLogic.Veltman.FrameClass.ILMinus_J2Plus :

Equations

LO.InterpretabilityLogic.Veltman.FrameClass.ILMinus_J2Plus = {F : LO.InterpretabilityLogic.Veltman.Frame | F.HasAxiomJ2}

Instances For

instance LO.InterpretabilityLogic.Veltman.instHasAxiomJ2TrivialFrame :

trivialFrame.HasAxiomJ2

instance LO.InterpretabilityLogic.ILMinus_J2Plus.Veltman.sound :

Sound ILMinus_J2Plus Veltman.FrameClass.ILMinus_J2Plus

instance LO.InterpretabilityLogic.ILMinus_J2Plus.instConsistentFormulaNatLogic :

Entailment.Consistent ILMinus_J2Plus

instance LO.InterpretabilityLogic.instStrictlyWeakerThanFormulaNatLogicILMinus_J4PlusILMinus_J2Plus :

ILMinus_J4Plus ⪱ ILMinus_J2Plus