S4

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveFiniteFrameClass : FiniteFrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.ReflexiveTransitiveFiniteFrameClass = {F : LO.Modal.Kripke.FiniteFrame | Std.Refl F.Rel ∧ IsTrans F.World F.Rel}

instance LO.Modal.instDefinedByReflexiveTransitiveFrameClassAxiomsNatS4 : Kripke.ReflexiveTransitiveFrameClass.DefinedBy Hilbert.S4.axioms

instance LO.Modal.Hilbert.S4.Kripke.sound : Sound Hilbert.S4 Kripke.ReflexiveTransitiveFrameClass

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

instance LO.Modal.Hilbert.S4.Kripke.complete : Complete Hilbert.S4 Kripke.ReflexiveTransitiveFrameClass

instance LO.Modal.Hilbert.S4.Kripke.finiteComplete : Complete Hilbert.S4 Kripke.ReflexiveTransitiveFiniteFrameClass