@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.refl_symm : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.refl_symm = {F : LO.Modal.Kripke.Frame | IsRefl F.World F.Rel ∧ IsSymm F.World F.Rel}

Instances For

• LO.Modal.Hilbert.KTB.Kripke.canonical
• LO.Modal.Hilbert.KTB.Kripke.complete
• LO.Modal.Hilbert.KTB.Kripke.sound

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.finite_refl_symm : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.finite_refl_symm = {F : LO.Modal.Kripke.Frame | Finite F.World ∧ IsRefl F.World F.Rel ∧ IsSymm F.World F.Rel}

Instances For

• LO.Modal.Hilbert.KTB.Kripke.finite_complete

instance LO.Modal.Hilbert.KTB.Kripke.sound : Sound Hilbert.KTB Kripke.FrameClass.refl_symm

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

instance LO.Modal.Hilbert.KTB.Kripke.canonical : Kripke.Canonical Hilbert.KTB Kripke.FrameClass.refl_symm

instance LO.Modal.Hilbert.KTB.Kripke.complete : Complete Hilbert.KTB Kripke.FrameClass.refl_symm

instance LO.Modal.Hilbert.KTB.Kripke.finite_complete : Complete Hilbert.KTB Kripke.FrameClass.finite_refl_symm