@[reducible, inline]

abbrev LO.Modal.Kripke.ConnectedFrameClass : LO.Modal.Kripke.FrameClass

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveConnectedFrameClass : LO.Modal.Kripke.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 : LO.Modal.Kripke.ConnectedFrameClass.DefinedBy .𝟯

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

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

Equations

• LO.Modal.Hilbert.S4Dot3.Kripke.sound = ⋯

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

Equations

• LO.Modal.Hilbert.S4Dot3.consistent = ⋯

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

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

Equations

• LO.Modal.Hilbert.S4Dot3.complete = ⋯