@[reducible, inline]

abbrev LO.Modal.Kripke.ConnectedFrameClass : FrameClass

Equations

• LO.Modal.Kripke.ConnectedFrameClass = {F : LO.Modal.Kripke.Frame | Connected F.Rel}

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveConnectedFrameClass : FrameClass

Equations

• LO.Modal.Kripke.ReflexiveTransitiveConnectedFrameClass = {F : LO.Modal.Kripke.Frame | Reflexive F.Rel ∧ Transitive F.Rel ∧ Connected F.Rel}

theorem LO.Modal.Kripke.ConnectedFrameClass.is_defined_by_Dot3 : ConnectedFrameClass.DefinedBy .𝟯

theorem LO.Modal.Kripke.ReflexiveTransitiveConnectedFrameClass.is_defined_by_T_Four_Dot3 : ReflexiveTransitiveConnectedFrameClass.DefinedBy (𝗧 ∪ 𝟰 ∪ .𝟯)

instance LO.Modal.Hilbert.S4Dot3.Kripke.sound : Sound (Hilbert.S4Dot3 ℕ) Kripke.ReflexiveTransitiveConnectedFrameClass

instance LO.Modal.Hilbert.S4Dot3.consistent : System.Consistent (Hilbert.S4Dot3 ℕ)

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.is_connected_of_subset_Dot3 {Ax : Set (Formula ℕ)} (hAx : .𝟯 ⊆ Ax) [(Hilbert.ExtK Ax).Consistent] : Connected (canonicalFrame (Hilbert.ExtK Ax)).Rel

instance LO.Modal.Hilbert.S4Dot3.complete : Complete (Hilbert.S4Dot3 ℕ) Kripke.ReflexiveTransitiveConnectedFrameClass