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 }
Equations
- LO.Modal.Kripke.S4Dot3_defines = inferInstance
instance
LO.Modal.Kripke.instConsistentFormulaHilbertS4Dot3
{α : Type u}
[Inhabited α]
[atleast : Atleast 2 α]
:
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 α]
:
Equations
- ⋯ = ⋯