Documentation

Foundation.Modal.System.S4

def LO.System.iff_box_boxdot {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓒 : S} [LO.System.S4 𝓒] {Ο† : F} :
𝓒 ⊒ β–‘Ο† β­€ βŠ‘Ο†
Equations
Instances For
    @[simp]
    theorem LO.System.iff_box_boxdot! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓒 : S} [LO.System.S4 𝓒] {Ο† : F} :
    𝓒 ⊒! β–‘Ο† β­€ βŠ‘Ο†
    def LO.System.iff_dia_diadot {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓒 : S} [LO.System.S4 𝓒] {Ο† : F} :
    𝓒 ⊒ β—‡Ο† β­€ βŸΟ†
    Equations
    Instances For
      @[simp]
      theorem LO.System.iff_dia_diadot! {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓒 : S} [LO.System.S4 𝓒] {Ο† : F} :
      𝓒 ⊒! β—‡Ο† β­€ βŸΟ†