KT4B

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveSymmetricFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveSymmetricFiniteFrameClass : FiniteFrameClass

Imported declaration from the Incompleteness formalization.

Equations

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

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

instance LO.Modal.Hilbert.KT4B.Kripke.complete : Complete Hilbert.KT4B Kripke.ReflexiveTransitiveSymmetricFrameClass

instance LO.Modal.Hilbert.KT4B.Kripke.finiteComplete : Complete Hilbert.KT4B Kripke.ReflexiveTransitiveSymmetricFiniteFrameClass