Documentation

Foundation.Modal.System.KTc

source
def LO.System.diaT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.KTc 𝓒] {Ο† : F} :
𝓒 ⊒ β—‡Ο† ➝ Ο†
Equations
Instances For
    source
    @[simp]
    theorem LO.System.diaT! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.KTc 𝓒] {Ο† : F} :
    𝓒 ⊒! β—‡Ο† ➝ Ο†
    source
    def LO.System.diaT' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.KTc 𝓒] {Ο† : F} (h : 𝓒 ⊒ β—‡Ο†) :
    𝓒 ⊒ Ο†
    Equations
    Instances For
      source
      theorem LO.System.diaT'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓒 : S} [System.KTc 𝓒] {Ο† : F} (h : 𝓒 ⊒! β—‡Ο†) :
      𝓒 ⊒! Ο†
      source
      def LO.System.KTc.axiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓒 : S} [System.KTc 𝓒] {Ο† : F} :
      𝓒 ⊒ Axioms.Four Ο†
      Equations
      Instances For
        source
        instance LO.System.KTc.instHasAxiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓒 : S} [System.KTc 𝓒] :
        HasAxiomFour 𝓒
        Equations
        source
        def LO.System.KTc.axiomFive {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓒 : S} [System.KTc 𝓒] {Ο† : F} :
        𝓒 ⊒ β—‡Ο† ➝ β–‘β—‡Ο†
        Equations
        Instances For
          source
          instance LO.System.KTc.instHasAxiomFive {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓒 : S} [System.KTc 𝓒] :
          HasAxiomFive 𝓒
          Equations