Documentation

LeanPool.Incompleteness.Foundation.Modal.Entailment.K4

K4 #

source
def LO.Entailment.implyBoxBoxdotBox {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} :
𝓒 ⊒ β–‘βŠ‘Ο† ==> β–‘Ο†

Imported declaration from the Incompleteness formalization.

Equations
Instances For
    source
    @[simp]
    theorem LO.Entailment.imply_boxboxdot_box {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} :
    𝓒 ⊒! β–‘βŠ‘Ο† ==> β–‘Ο†
    source
    def LO.Entailment.implyBoxBoxBoxdot {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} :
    𝓒 ⊒ β–‘Ο† ==> β–‘βŠ‘Ο†

    Imported declaration from the Incompleteness formalization.

    Equations
    Instances For
      source
      @[simp]
      theorem LO.Entailment.imply_box_boxboxdot! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} :
      𝓒 ⊒! β–‘Ο† ==> β–‘βŠ‘Ο†
      source
      def LO.Entailment.implyBoxBoxBoxdot' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} (h : 𝓒 ⊒ β–‘Ο†) :
      𝓒 ⊒ β–‘βŠ‘Ο†

      Imported declaration from the Incompleteness formalization.

      Equations
      Instances For
        source
        theorem LO.Entailment.implyBoxBoxBoxdot'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} (h : 𝓒 ⊒! β–‘Ο†) :
        𝓒 ⊒! β–‘βŠ‘Ο†

        Imported declaration from the Incompleteness formalization.

        source
        def LO.Entailment.iffBoxBoxBoxdot {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} :
        𝓒 ⊒ β–‘Ο† <=> β–‘βŠ‘Ο†

        Imported declaration from the Incompleteness formalization.

        Equations
        Instances For
          source
          @[simp]
          theorem LO.Entailment.iff_box_boxboxdot! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} :
          𝓒 ⊒! β–‘Ο† <=> β–‘βŠ‘Ο†
          source
          def LO.Entailment.iffBoxBoxdotBox {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} :
          𝓒 ⊒ β–‘Ο† <=> βŠ‘β–‘Ο†

          Imported declaration from the Incompleteness formalization.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem LO.Entailment.iff_box_boxdotbox! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} :
            𝓒 ⊒! β–‘Ο† <=> βŠ‘β–‘Ο†
            source
            def LO.Entailment.iffBoxdotBoxdotBoxdot {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} :
            𝓒 ⊒ βŠ‘Ο† <=> βŠ‘βŠ‘Ο†

            Imported declaration from the Incompleteness formalization.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem LO.Entailment.iff_boxdot_boxdotboxdot {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} :
              𝓒 ⊒! βŠ‘Ο† <=> βŠ‘βŠ‘Ο†
              source
              def LO.Entailment.boxdotAxiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} :
              𝓒 ⊒ βŠ‘Ο† ==> βŠ‘βŠ‘Ο†

              Imported declaration from the Incompleteness formalization.

              Equations
              Instances For
                source
                @[simp]
                theorem LO.Entailment.boxdot_axiomFour! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.K4 𝓒] {Ο† : F} :
                𝓒 ⊒! βŠ‘Ο† ==> βŠ‘βŠ‘Ο†