instance LO.Modal.Kripke.axiomGrz_defineability {α : Type u} [Inhabited α] [DecidableEq α] : 𝔽(𝗚𝗿𝘇).DefinedBy LO.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass

Equations

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

instance LO.Modal.Kripke.instSoundHilbertFormulaDepGrzAltReflexiveTransitiveWeaklyConverseWellFoundedFrameClass {α : Type u} [Inhabited α] [DecidableEq α] : LO.Sound 𝐆𝐫𝐳 LO.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass#α

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.instConsistentFormulaHilbertGrz {α : Type u} [Inhabited α] [DecidableEq α] : LO.System.Consistent 𝐆𝐫𝐳

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.axiomGrz_finite_defines {α : Type u} [Inhabited α] [DecidableEq α] : 𝔽ꟳ(𝗚𝗿𝘇).DefinedBy LO.Kripke.ReflexiveTransitiveAntisymmetricFrameClassꟳ

Equations

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

instance LO.Modal.Kripke.instSoundHilbertFormulaDepGrzAltToFiniteFrameClassReflexiveTransitiveAntisymmetricFrameClass {α : Type u} [Inhabited α] [DecidableEq α] : LO.Sound 𝐆𝐫𝐳 LO.Kripke.ReflexiveTransitiveAntisymmetricFrameClassꟳ#α

Equations

• ⋯ = ⋯