Documentation

Foundation.Modal.System.KT

source
def LO.System.diaTc {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.KT 𝓒] {Ο† : F} :
𝓒 ⊒ Ο† ➝ β—‡Ο†
Equations
Instances For
    source
    @[simp]
    theorem LO.System.diaTc! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.KT 𝓒] {Ο† : F} :
    𝓒 ⊒! Ο† ➝ β—‡Ο†
    source
    def LO.System.diaTc' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.KT 𝓒] {Ο† : F} [HasDiaDuality 𝓒] (h : 𝓒 ⊒ Ο†) :
    𝓒 ⊒ β—‡Ο†
    Equations
    Instances For
      source
      theorem LO.System.diaTc'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.KT 𝓒] {Ο† : F} [HasDiaDuality 𝓒] (h : 𝓒 ⊒! Ο†) :
      𝓒 ⊒! β—‡Ο†