Documentation

Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus

source
theorem LO.Modal.Kripke.Frame.isGL_of_isFiniteGL {F : Frame} (hF : F.IsFiniteGL) :
F.IsGL
source
@[reducible, inline]
abbrev LO.InterpretabilityLogic.Veltman.FrameClass.ILMinus :
FrameClass
Equations
Instances For
    source
    @[reducible, inline]
    abbrev LO.InterpretabilityLogic.Veltman.trivialFrame :
    Frame
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance LO.InterpretabilityLogic.ILMinus.Veltman.sound :
      Sound InterpretabilityLogic.ILMinus Veltman.FrameClass.ILMinus
      source
      instance LO.InterpretabilityLogic.ILMinus.instConsistentFormulaNatLogic :
      Entailment.Consistent InterpretabilityLogic.ILMinus