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.instSoundNormalNatFormulaFrameClassKD :
      Sound Hilbert.KD Kripke.FrameClass.KD
      source
      instance LO.Modal.Hilbert.KD.Kripke.instConsistentFormulaNatNormal :
      Entailment.Consistent Hilbert.KD
      source
      instance LO.Modal.Hilbert.KD.Kripke.instCanonicalNormalNatKD :
      Kripke.Canonical Hilbert.KD Kripke.FrameClass.KD
      source
      instance LO.Modal.Hilbert.KD.Kripke.instCompleteNormalNatFormulaFrameClassKD :
      Complete Hilbert.KD Kripke.FrameClass.KD
      source
      instance LO.Modal.Hilbert.instStrictlyWeakerThanFormulaNatNormalKKD :
      Hilbert.K ⪱ Hilbert.KD
      source
      instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicKKD :
      Modal.K ⪱ Modal.KD