instance
LO.Modal.Standard.Kripke.axiomVer_definability
{α : Type u}
:
𝔽(𝗩𝗲𝗿).DefinedBy LO.Kripke.IsolatedFrameClass
Equations
- LO.Modal.Standard.Kripke.axiomVer_definability = { define := ⋯, nonempty := LO.Modal.Standard.Kripke.axiomVer_definability.proof_1 }
Equations
- LO.Modal.Standard.Kripke.Ver_definability = inferInstance
instance
LO.Modal.Standard.Kripke.instSoundDeductionParameterFormulaDepVerAltIsolatedFrameClass
{α : Type u}
:
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.Kripke.isolated_CanonicalFrame
{α : Type u}
[DecidableEq α]
{Ax : LO.Modal.Standard.AxiomSet α}
(h : 𝗩𝗲𝗿 ⊆ Ax)
[LO.System.Consistent 𝝂Ax]
:
instance
LO.Modal.Standard.Kripke.instCompleteDeductionParameterFormulaDepVerAltIsolatedFrameClass
{α : Type u}
[DecidableEq α]
:
Equations
- ⋯ = ⋯