Documentation

Foundation.Modal.Kripke.Logic.KTc

source
@[reducible, inline]
abbrev LO.Modal.Kripke.Frame.IsKTc (F : Frame) :
Prop
Equations
Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Kripke.FrameClass.KTc :
    FrameClass
    Equations
    Instances For
      source
      instance LO.Modal.Kripke.instIsKB4OfIsKTc {F : Frame} [F.IsKTc] :
      F.IsKB4
      source
      instance LO.Modal.KTc.Kripke.instSoundLogicNatFormulaFrameClassKTc :
      Sound Modal.KTc Kripke.FrameClass.KTc
      source
      instance LO.Modal.KTc.Kripke.instConsistentFormulaNatLogic :
      Entailment.Consistent Modal.KTc
      source
      instance LO.Modal.KTc.Kripke.instCanonicalLogicNatKTc :
      Kripke.Canonical Modal.KTc Kripke.FrameClass.KTc
      source
      instance LO.Modal.KTc.Kripke.instCompleteLogicNatFormulaFrameClassKTc :
      Complete Modal.KTc Kripke.FrameClass.KTc
      source
      instance LO.Modal.KTc.Kripke.instStrictlyWeakerThanFormulaNatLogicKB4 :
      Modal.KB4 ⪱ Modal.KTc