instance LO.Modal.Kripke.axiomDot3_Definability {α : Type u} [atleast : Atleast 2 α] : 𝔽(.𝟯).DefinedBy LO.Kripke.ConnectedFrameClass

Equations

• LO.Modal.Kripke.axiomDot3_Definability = { define := ⋯, nonempty := LO.Modal.Kripke.axiomDot3_Definability.proof_3 }

instance LO.Modal.Kripke.axiomS4Dot3_defines {α : Type u} [Inhabited α] [atleast : Atleast 2 α] : 𝔽(𝗧 ∪ 𝟰 ∪ .𝟯).DefinedBy LO.Kripke.ReflexiveTransitiveConnectedFrameClass

Equations

• One or more equations did not get rendered due to their size.

instance LO.Modal.Kripke.S4Dot3_defines {α : Type u} [Inhabited α] [atleast : Atleast 2 α] : LO.Kripke.FrameClass.DefinedBy 𝔽(𝐒𝟒.𝟑) LO.Kripke.ReflexiveTransitiveConnectedFrameClass

Equations

• LO.Modal.Kripke.S4Dot3_defines = inferInstance

instance LO.Modal.Kripke.instConsistentFormulaHilbertS4Dot3 {α : Type u} [Inhabited α] [atleast : Atleast 2 α] : LO.System.Consistent 𝐒𝟒.𝟑

Equations

• ⋯ = ⋯

theorem LO.Modal.Kripke.connected_CanonicalFrame {α : Type u} [DecidableEq α] {Ax : LO.Modal.Theory α} (hAx : .𝟯 ⊆ Ax) [LO.System.Consistent 𝝂Ax] : Connected (LO.Modal.Kripke.CanonicalFrame 𝝂Ax).Rel

instance LO.Modal.Kripke.instCompleteHilbertFormulaDepS4Dot3AltReflexiveTransitiveConnectedFrameClass {α : Type u} [Inhabited α] [DecidableEq α] [atleast : Atleast 2 α] : LO.Complete 𝐒𝟒.𝟑 LO.Kripke.ReflexiveTransitiveConnectedFrameClass#α

Equations

• ⋯ = ⋯