Documentation

Foundation.Modal.Kripke.Logic.KD

source
@[reducible, inline]
abbrev LO.Modal.Kripke.Frame.IsKD (F : Frame) :
Prop
Equations
Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Kripke.FrameClass.KD :
    FrameClass
    Equations
    Instances For
      source
      instance LO.Modal.Hilbert.KD.Kripke.instSoundLogicNatFormulaFrameClassKDKD :
      Sound Modal.KD Kripke.FrameClass.KD
      source
      instance LO.Modal.Hilbert.KD.Kripke.instConsistentFormulaNatLogicKD :
      Entailment.Consistent Modal.KD
      source
      instance LO.Modal.Hilbert.KD.Kripke.instCanonicalLogicNatKDKD :
      Kripke.Canonical Modal.KD Kripke.FrameClass.KD
      source
      instance LO.Modal.Hilbert.KD.Kripke.instCompleteLogicNatFormulaFrameClassKDKD :
      Complete Modal.KD Kripke.FrameClass.KD
      source
      instance LO.Modal.Hilbert.instStrictlyWeakerThanFormulaNatLogicKKD :
      Modal.K ⪱ Modal.KD