AxiomDot3

theorem LO.Modal.Kripke.connected_of_validate_dot3 {F : Frame} (hCon : Connected F.Rel) : F ⊧ Axioms.Dot3 (Formula.atom 0) (Formula.atom 1)

theorem LO.Modal.Kripke.validate_dot3_of_connected {F : Frame} : F ⊧ Axioms.Dot3 (Formula.atom 0) (Formula.atom 1) → Connected F.Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.ConnectedFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

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

instance LO.Modal.Kripke.ConnectedFrameClass.DefinedByDot3 : ConnectedFrameClass.DefinedBy {Axioms.Dot3 (Formula.atom 0) (Formula.atom 1)}