theorem LO.Modal.Kripke.iff_Universal_ReflexiveEuclidean_validOnFrameClass {α : Type u} {p : LO.Modal.Formula α} : LO.Kripke.UniversalFrameClass#α ⊧ p ↔ LO.Kripke.ReflexiveEuclideanFrameClass#α ⊧ p

instance LO.Modal.Kripke.S5_complete_universal {α : Type u} [Inhabited α] [DecidableEq α] : LO.Complete 𝐒𝟓 LO.Kripke.UniversalFrameClass#α

Equations

• ⋯ = ⋯