KB5

@[reducible, inline]

abbrev LO.Modal.Kripke.SymmetricEuclideanFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.SymmetricEuclideanFrameClass = {F : LO.Modal.Kripke.Frame | IsSymmetric F.Rel ∧ Euclidean F.Rel}

instance LO.Modal.Hilbert.KB5.Kripke.sound : Sound Hilbert.KB5 Kripke.SymmetricEuclideanFrameClass

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

instance LO.Modal.Hilbert.KB5.Kripke.complete : Complete Hilbert.KB5 Kripke.SymmetricEuclideanFrameClass