Basic

@[reducible, inline]

abbrev LO.IntProp.Kripke.EuclideanFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.IntProp.Kripke.EuclideanFrameClass = {F : LO.IntProp.Kripke.Frame | Euclidean F.Rel}

instance LO.IntProp.Kripke.EuclideanFrameClass.definedByLEM : EuclideanFrameClass.DefinedByFormula (Axioms.LEM (Formula.atom 0))

instance LO.IntProp.instIsNonemptyEuclideanFrameClass : Kripke.EuclideanFrameClass.IsNonempty

instance LO.IntProp.Hilbert.Cl.Kripke.instDefinedByEuclideanFrameClassAxiomsNat : Kripke.EuclideanFrameClass.DefinedBy Hilbert.Cl.axioms

instance LO.IntProp.Hilbert.Cl.Kripke.sound : Sound Hilbert.Cl Kripke.EuclideanFrameClass

instance LO.IntProp.Hilbert.Cl.Kripke.consistent : Entailment.Consistent Hilbert.Cl