K45

@[reducible, inline]

abbrev LO.Modal.Kripke.TransitiveEuclideanFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.TransitiveEuclideanFrameClass = {F : LO.Modal.Kripke.Frame | IsTrans F.World F.Rel ∧ Euclidean F.Rel}

instance LO.Modal.Hilbert.K45.Kripke.sound : Sound Hilbert.K45 Kripke.TransitiveEuclideanFrameClass

instance LO.Modal.Hilbert.K45.Kripke.consistent : Entailment.Consistent Hilbert.K45

instance LO.Modal.Hilbert.K45.Kripke.complete : Complete Hilbert.K45 Kripke.TransitiveEuclideanFrameClass