S5

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveEuclideanFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.ReflexiveEuclideanFrameClass = {F : LO.Modal.Kripke.Frame | Std.Refl F.Rel ∧ Euclidean F.Rel}

instance LO.Modal.Hilbert.S5.Kripke.sound : Sound Hilbert.S5 Kripke.ReflexiveEuclideanFrameClass

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

instance LO.Modal.Hilbert.S5.Kripke.complete : Complete Hilbert.S5 Kripke.ReflexiveEuclideanFrameClass

@[reducible, inline]

abbrev LO.Modal.Kripke.UniversalFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.UniversalFrameClass = {F : LO.Modal.Kripke.Frame | Universal F.Rel}

theorem LO.Modal.Kripke.iff_validOnUniversalFrameClass_validOnReflexiveEuclideanFrameClass {φ : Formula ℕ} : UniversalFrameClass ⊧ φ ↔ ReflexiveEuclideanFrameClass ⊧ φ

instance LO.Modal.Hilbert.S5.Kripke.soundUniversal : Sound Hilbert.S5 Kripke.UniversalFrameClass

instance LO.Modal.Hilbert.S5.Kripke.completeUniversal : Complete Hilbert.S5 Kripke.UniversalFrameClass

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveEuclideanFiniteFrameClass : FiniteFrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.ReflexiveEuclideanFiniteFrameClass = {F : LO.Modal.Kripke.FiniteFrame | Std.Refl F.Rel ∧ Euclidean F.Rel}

theorem LO.Modal.Kripke.eq_ReflexiveTransitiveSymmetricFiniteFrameClass_ReflexiveEuclideanFiniteFrameClass : ReflexiveTransitiveSymmetricFiniteFrameClass = ReflexiveEuclideanFiniteFrameClass