@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass : FrameClass

Equations

• LO.Modal.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass = {F : LO.Modal.Kripke.Frame | Reflexive F.Rel ∧ Transitive F.Rel ∧ WeaklyConverseWellFounded F.Rel}

Instances For

• LO.Modal.Hilbert.Grz.Kripke.sound

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveAntiSymmetricFiniteFrameClass : FiniteFrameClass

Equations

• LO.Modal.Kripke.ReflexiveTransitiveAntiSymmetricFiniteFrameClass = {F : LO.Modal.Kripke.FiniteFrame | Reflexive F.Rel ∧ Transitive F.Rel ∧ AntiSymmetric F.Rel}

Instances For

• LO.Modal.Hilbert.Grz.Kripke.complete
• LO.Modal.Hilbert.Grz.Kripke.finite_sound
• LO.Modal.Hilbert.Grz.Kripke.instFiniteFramePropertyNatReflexiveTransitiveAntiSymmetricFiniteFrameClass

theorem LO.Modal.Kripke.Grz_of_WCWF {F : Frame} : Reflexive F.Rel ∧ Transitive F.Rel ∧ WeaklyConverseWellFounded F.Rel → F ⊧* 𝗚𝗿𝘇

theorem LO.Modal.Kripke.valid_on_frame_T_and_Four_of_Grz {F : Frame} (h : F ⊧* 𝗚𝗿𝘇) : F ⊧* {x : Formula ℕ | ∃ (φ : Formula ℕ), □φ ➝ φ ⋏ (□φ ➝ □□φ) = x}

theorem LO.Modal.Kripke.valid_on_frame_T_of_Grz {F : Frame} (h : F ⊧* 𝗚𝗿𝘇) : F ⊧* 𝗧

theorem LO.Modal.Kripke.valid_on_frame_Four_of_Grz {F : Frame} (h : F ⊧* 𝗚𝗿𝘇) : F ⊧* 𝟰

theorem LO.Modal.Kripke.refl_of_Grz {F : Frame} (h : F ⊧* 𝗚𝗿𝘇) : Reflexive F.Rel

theorem LO.Modal.Kripke.trans_of_Grz {F : Frame} (h : F ⊧* 𝗚𝗿𝘇) : Transitive F.Rel

theorem LO.Modal.Kripke.WCWF_of_Grz {F : Frame} (h : F ⊧* 𝗚𝗿𝘇) : WCWF F.Rel

theorem LO.Modal.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass.is_defined_by_Grz : ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass.DefinedBy 𝗚𝗿𝘇

theorem LO.Modal.Kripke.ReflexiveTransitiveAntiSymmetricFiniteFrameClass.is_defined_by_Grz : ReflexiveTransitiveAntiSymmetricFiniteFrameClass.DefinedBy 𝗚𝗿𝘇

instance LO.Modal.Hilbert.Grz.Kripke.sound : Sound (Hilbert.Grz ℕ) Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass

instance LO.Modal.Hilbert.Grz.Kripke.finite_sound : Sound (Hilbert.Grz ℕ) Kripke.ReflexiveTransitiveAntiSymmetricFiniteFrameClass

instance LO.Modal.Hilbert.Grz.consistent : System.Consistent (Hilbert.Grz ℕ)