Documentation

Foundation.Modal.System.KTc

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