Documentation

Foundation.Modal.Kripke.Logic.Ver

source
@[reducible, inline]
abbrev LO.Modal.Kripke.Frame.IsVer (F : Frame) :
Prop
Equations
Instances For
    source
    class LO.Modal.Kripke.Frame.IsFiniteVer (F : Frame) extends F.IsFinite, IsIsolated F.Rel :
    Prop
    Instances
      source
      instance LO.Modal.Kripke.instIsFiniteGLPoint3'OfIsFiniteVer {F : Frame} [F.IsFiniteVer] :
      F.IsFiniteGLPoint3'
      source
      @[simp]
      theorem LO.Modal.Kripke.Frame.isolated {F : Frame} [F.IsVer] {x y : F.World} :
      ¬x ≺ y
      source
      @[reducible, inline]
      abbrev LO.Modal.Kripke.FrameClass.Ver :
      FrameClass
      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev LO.Modal.Kripke.FrameClass.finite_Ver :
        FrameClass
        Equations
        Instances For
          source
          instance LO.Modal.instSoundLogicNatFormulaFrameClassVerVer :
          Sound Modal.Ver Kripke.FrameClass.Ver
          source
          instance LO.Modal.instSoundLogicNatFormulaFrameClassVerFinite_Ver :
          Sound Modal.Ver Kripke.FrameClass.finite_Ver
          source
          instance LO.Modal.instConsistentFormulaNatLogicVer :
          Entailment.Consistent Modal.Ver
          source
          instance LO.Modal.instCanonicalLogicNatVerVer :
          Kripke.Canonical Modal.Ver Kripke.FrameClass.Ver
          source
          instance LO.Modal.instCompleteLogicNatFormulaFrameClassVerVer :
          Complete Modal.Ver Kripke.FrameClass.Ver
          source
          instance LO.Modal.instCompleteLogicNatFormulaFrameClassVerFinite_Ver :
          Complete Modal.Ver Kripke.FrameClass.finite_Ver
          source
          instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicKTcVer :
          Modal.KTc ⪱ Modal.Ver
          source
          instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicGLPoint3Ver :
          Modal.GLPoint3 ⪱ Modal.Ver