S4Dot2

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveConfluentFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.ReflexiveTransitiveConfluentFrameClass = {F : LO.Modal.Kripke.Frame | Std.Refl F.Rel ∧ IsTrans F.World F.Rel ∧ Confluent F.Rel}

instance LO.Modal.Hilbert.S4Dot2.Kripke.sound : Sound Hilbert.S4Dot2 Kripke.ReflexiveTransitiveConfluentFrameClass

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

instance LO.Modal.Hilbert.S4Dot2.Kripke.complete : Complete Hilbert.S4Dot2 Kripke.ReflexiveTransitiveConfluentFrameClass