Documentation

Foundation.Modal.Kripke.Grz.Definability

source
@[reducible, inline]
abbrev LO.Modal.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass :
LO.Modal.Kripke.FrameClass
Equations
Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Kripke.ReflexiveTransitiveAntisymmetricFiniteFrameClass :
    LO.Modal.Kripke.FiniteFrameClass
    Equations
    Instances For
      source
      theorem LO.Modal.Kripke.Grz_of_WCWF {F : LO.Modal.Kripke.Frame} :
      Reflexive F.Rel ∧ Transitive F.Rel ∧ WeaklyConverseWellFounded F.Rel → F ⊧* 𝗚𝗿𝘇
      source
      theorem LO.Modal.Kripke.valid_on_frame_T_and_Four_of_Grz {F : LO.Modal.Kripke.Frame} (h : F ⊧* 𝗚𝗿𝘇) :
      F ⊧* {x : LO.Modal.Formula ℕ | ∃ (φ : LO.Modal.Formula ℕ), □φ ➝ φ ⋏ (□φ ➝ □□φ) = x}
      source
      theorem LO.Modal.Kripke.valid_on_frame_T_of_Grz {F : LO.Modal.Kripke.Frame} (h : F ⊧* 𝗚𝗿𝘇) :
      F ⊧* 𝗧
      source
      theorem LO.Modal.Kripke.valid_on_frame_Four_of_Grz {F : LO.Modal.Kripke.Frame} (h : F ⊧* 𝗚𝗿𝘇) :
      F ⊧* 𝟰
      source
      theorem LO.Modal.Kripke.refl_of_Grz {F : LO.Modal.Kripke.Frame} (h : F ⊧* 𝗚𝗿𝘇) :
      Reflexive F.Rel
      source
      theorem LO.Modal.Kripke.trans_of_Grz {F : LO.Modal.Kripke.Frame} (h : F ⊧* 𝗚𝗿𝘇) :
      Transitive F.Rel
      source
      theorem LO.Modal.Kripke.WCWF_of_Grz {F : LO.Modal.Kripke.Frame} (h : F ⊧* 𝗚𝗿𝘇) :
      WCWF F.Rel
      source
      theorem LO.Modal.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass.is_defined_by_Grz :
      LO.Modal.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass.DefinedBy 𝗚𝗿𝘇
      source
      theorem LO.Modal.Kripke.ReflexiveTransitiveAntisymmetricFiniteFrameClass.is_defined_by_Grz :
      LO.Modal.Kripke.ReflexiveTransitiveAntisymmetricFiniteFrameClass.DefinedBy 𝗚𝗿𝘇
      source
      instance LO.Modal.Hilbert.Grz.Kripke.sound :
      LO.Sound (LO.Modal.Hilbert.Grz ℕ) LO.Modal.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass
      Equations
      source
      instance LO.Modal.Hilbert.Grz.Kripke.finite_sound :
      LO.Sound (LO.Modal.Hilbert.Grz ℕ) LO.Modal.Kripke.ReflexiveTransitiveAntisymmetricFiniteFrameClass
      Equations
      source
      instance LO.Modal.Hilbert.Grz.consistent :
      LO.System.Consistent (LO.Modal.Hilbert.Grz ℕ)
      Equations