KD4

@[reducible, inline]

abbrev LO.Modal.Kripke.SerialTransitiveFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

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

instance LO.Modal.Hilbert.KD4.Kripke.sound : Sound Hilbert.KD4 Kripke.SerialTransitiveFrameClass

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

instance LO.Modal.Hilbert.KD4.Kripke.complete : Complete Hilbert.KD4 Kripke.SerialTransitiveFrameClass