instance
LO.Modal.Standard.Kripke.axiomDot3_Definability
{α : Type u}
[atleast : Atleast 2 α]
:
𝔽(.𝟯).DefinedBy LO.Kripke.ConnectedFrameClass
Equations
- LO.Modal.Standard.Kripke.axiomDot3_Definability = { define := ⋯, nonempty := LO.Modal.Standard.Kripke.axiomDot3_Definability.proof_3 }
instance
LO.Modal.Standard.Kripke.S4Dot3_defines
{α : Type u}
[Inhabited α]
[atleast : Atleast 2 α]
:
Equations
- LO.Modal.Standard.Kripke.S4Dot3_defines = inferInstance
instance
LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterS4Dot3
{α : Type u}
[Inhabited α]
[atleast : Atleast 2 α]
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.Kripke.connected_CanonicalFrame
{α : Type u}
[DecidableEq α]
{Ax : LO.Modal.Standard.AxiomSet α}
(hAx : .𝟯 ⊆ Ax)
[LO.System.Consistent 𝝂Ax]
:
instance
LO.Modal.Standard.Kripke.instCompleteDeductionParameterFormulaDepS4Dot3AltReflexiveTransitiveConnectedFrameClass
{α : Type u}
[Inhabited α]
[DecidableEq α]
[atleast : Atleast 2 α]
:
Equations
- ⋯ = ⋯