@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.TransitiveCWFFrameClass : LO.Modal.Standard.Kripke.FrameClass

Equations

• LO.Modal.Standard.Kripke.TransitiveCWFFrameClass = {F : LO.Modal.Standard.Kripke.Frame | Transitive F.Rel ∧ ConverseWellFounded F.Rel}

theorem LO.Modal.Standard.Kripke.axiomL_defines {α : Type u} [Inhabited α] : LO.Modal.Standard.AxiomSet.DefinesKripkeFrameClass 𝗟 LO.Modal.Standard.Kripke.TransitiveCWFFrameClass

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.TransitiveIrreflexiveFrameClass : LO.Modal.Standard.Kripke.FrameClass

Equations

• LO.Modal.Standard.Kripke.TransitiveIrreflexiveFrameClass = {F : LO.Modal.Standard.Kripke.Frame | Transitive F.Rel ∧ Irreflexive F.Rel}

theorem LO.Modal.Standard.Kripke.axiomL_finite_defines {α : Type u} [Inhabited α] : LO.Modal.Standard.AxiomSet.FinitelyDefinesKripkeFrameClass 𝗟 LO.Modal.Standard.Kripke.TransitiveIrreflexiveFrameClass.toFiniteFrameClass

instance LO.Modal.Standard.Kripke.GL_sound {α : Type u} [Inhabited α] : LO.Sound 𝐆𝐋 LO.Modal.Standard.Kripke.TransitiveIrreflexiveFrameClassꟳ.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterGL {α : Type u} [Inhabited α] : LO.System.Consistent 𝐆𝐋

Equations

• ⋯ = ⋯