Documentation

Foundation.Modal.Kripke.S5

source
@[reducible, inline]
abbrev LO.Modal.Kripke.UniversalFrameClass :
LO.Modal.Kripke.FrameClass
Equations
Instances For
    source
    theorem LO.Modal.Kripke.iff_Universal_ReflexiveEuclidean_validOnFrameClass {φ : LO.Modal.Formula ℕ} :
    LO.Modal.Kripke.UniversalFrameClass ⊧ φ ↔ LO.Modal.Kripke.ReflexiveEuclideanFrameClass ⊧ φ
    source
    instance LO.Modal.Hilbert.S5.Kripke.complete_universal :
    LO.Complete (LO.Modal.Hilbert.S5 ℕ) LO.Modal.Kripke.UniversalFrameClass
    Equations