instance LO.Modal.Kripke.axiomL_definability {α : Type u} [Inhabited α] : 𝔽(𝗟).DefinedBy LO.Kripke.TransitiveConverseWellFoundedFrameClass

Equations

• LO.Modal.Kripke.axiomL_definability = { define := ⋯, nonempty := LO.Modal.Kripke.axiomL_definability.proof_2 }

instance LO.Modal.Kripke.instSoundHilbertFormulaDepGLAltTransitiveConverseWellFoundedFrameClass {α : Type u} [Inhabited α] : LO.Sound 𝐆𝐋 LO.Kripke.TransitiveConverseWellFoundedFrameClass#α

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.axiomL_finite_definability {α : Type u} [Inhabited α] : 𝔽ꟳ(𝗟).DefinedBy LO.Kripke.TransitiveIrreflexiveFrameClassꟳ

Equations

• LO.Modal.Kripke.axiomL_finite_definability = { define := ⋯, nonempty := LO.Modal.Kripke.axiomL_finite_definability.proof_2 }

instance LO.Modal.Kripke.GL_finite_sound {α : Type u} [Inhabited α] : LO.Sound 𝐆𝐋 LO.Kripke.TransitiveIrreflexiveFrameClassꟳ#α

Equations

• ⋯ = ⋯