Documentation

LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Triv

Triv #

source
@[reducible, inline]
abbrev LO.Modal.Kripke.ReflexiveCoreflexiveFrameClass :
FrameClass

Imported declaration from the Incompleteness formalization.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Kripke.EqualityFrameClass :
    FrameClass

    Imported declaration from the Incompleteness formalization.

    Equations
    Instances For
      source
      theorem LO.Modal.Kripke.eq_EqualityFrameClass_ReflexiveCoreflexiveFrameClass :
      EqualityFrameClass = ReflexiveCoreflexiveFrameClass
      source
      instance LO.Modal.Hilbert.Triv.Kripke.soundReflCorefl :
      Sound Hilbert.Triv Kripke.ReflexiveCoreflexiveFrameClass
      source
      instance LO.Modal.Hilbert.Triv.Kripke.soundEquality :
      Sound Hilbert.Triv Kripke.EqualityFrameClass
      source
      instance LO.Modal.Hilbert.Triv.Kripke.consistent :
      Entailment.Consistent Hilbert.Triv
      source
      instance LO.Modal.Hilbert.Triv.Kripke.completeReflCorefl :
      Complete Hilbert.Triv Kripke.ReflexiveCoreflexiveFrameClass
      source
      instance LO.Modal.Hilbert.Triv.Kripke.completeEquality :
      Complete Hilbert.Triv Kripke.EqualityFrameClass