Documentation

Foundation.Modal.Entailment.E

source
def LO.Entailment.C_replace {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.Minimal 𝓒] {Οˆβ‚ φ₁ Ο†β‚‚ Οˆβ‚‚ : F} [HasAxiomImply₁ 𝓒] [HasAxiomImplyβ‚‚ 𝓒] (h₁ : 𝓒 ⊒! Οˆβ‚ ➝ φ₁) (hβ‚‚ : 𝓒 ⊒! Ο†β‚‚ ➝ Οˆβ‚‚) :
𝓒 ⊒! φ₁ ➝ Ο†β‚‚ β†’ 𝓒 ⊒! Οˆβ‚ ➝ Οˆβ‚‚
Equations
Instances For
    source
    def LO.Modal.Entailment.multire {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† ψ : F} {n : β„•} (h : 𝓒 ⊒! Ο† β­€ ψ) :
    𝓒 ⊒! β–‘^[n]Ο† β­€ β–‘^[n]ψ
    Equations
    Instances For
      source
      theorem LO.Modal.Entailment.multire! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† ψ : F} {n : β„•} (h : 𝓒 ⊒ Ο† β­€ ψ) :
      𝓒 ⊒ β–‘^[n]Ο† β­€ β–‘^[n]ψ
      source
      def LO.Modal.Entailment.multi_ELLNN! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
      𝓒 ⊒! β–‘^[n]Ο† β­€ β–‘^[n](βˆΌβˆΌΟ†)
      Equations
      Instances For
        source
        @[simp]
        theorem LO.Modal.Entailment.multi_ELLNN {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
        𝓒 ⊒ β–‘^[n]Ο† β­€ β–‘^[n](βˆΌβˆΌΟ†)
        source
        def LO.Modal.Entailment.ELLNN! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
        𝓒 ⊒! β–‘Ο† β­€ β–‘(βˆΌβˆΌΟ†)
        Equations
        Instances For
          source
          @[simp]
          theorem LO.Modal.Entailment.ELLNN {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
          𝓒 ⊒ β–‘Ο† β­€ β–‘(βˆΌβˆΌΟ†)
          source
          def LO.Modal.Entailment.ILLNN! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
          𝓒 ⊒! β–‘Ο† ➝ β–‘(βˆΌβˆΌΟ†)
          Equations
          Instances For
            source
            @[simp]
            theorem LO.Modal.Entailment.ILLNN {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
            𝓒 ⊒ β–‘Ο† ➝ β–‘(βˆΌβˆΌΟ†)
            source
            def LO.Modal.Entailment.box_dni {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
            𝓒 ⊒! β–‘Ο† ➝ β–‘(βˆΌβˆΌΟ†)

            Alias of LO.Modal.Entailment.ILLNN!.

            Equations
            Instances For
              source
              theorem LO.Modal.Entailment.box_dni! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
              𝓒 ⊒ β–‘Ο† ➝ β–‘(βˆΌβˆΌΟ†)

              Alias of LO.Modal.Entailment.ILLNN.

              source
              def LO.Modal.Entailment.ILNNL! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
              𝓒 ⊒! β–‘(βˆΌβˆΌΟ†) ➝ β–‘Ο†
              Equations
              Instances For
                source
                @[simp]
                theorem LO.Modal.Entailment.ILNNL {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                𝓒 ⊒ β–‘(βˆΌβˆΌΟ†) ➝ β–‘Ο†
                source
                def LO.Modal.Entailment.box_dne {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                𝓒 ⊒! β–‘(βˆΌβˆΌΟ†) ➝ β–‘Ο†

                Alias of LO.Modal.Entailment.ILNNL!.

                Equations
                Instances For
                  source
                  theorem LO.Modal.Entailment.box_dne! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                  𝓒 ⊒ β–‘(βˆΌβˆΌΟ†) ➝ β–‘Ο†

                  Alias of LO.Modal.Entailment.ILNNL.

                  source
                  def LO.Modal.Entailment.box_dne' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] (h : 𝓒 ⊒! β–‘(βˆΌβˆΌΟ†)) :
                  𝓒 ⊒! β–‘Ο†
                  Equations
                  Instances For
                    source
                    theorem LO.Modal.Entailment.box_dne'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] (h : 𝓒 ⊒ β–‘(βˆΌβˆΌΟ†)) :
                    𝓒 ⊒ β–‘Ο†
                    source
                    def LO.Modal.Entailment.INMNL! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                    𝓒 ⊒! βˆΌβ—‡(βˆΌΟ†) ➝ β–‘Ο†
                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem LO.Modal.Entailment.INMNL {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                      𝓒 ⊒ βˆΌβ—‡(βˆΌΟ†) ➝ β–‘Ο†
                      source
                      def LO.Modal.Entailment.INLMN! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                      𝓒 ⊒! βˆΌβ–‘Ο† ➝ β—‡(βˆΌΟ†)
                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem LO.Modal.Entailment.INLMN {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                        𝓒 ⊒ βˆΌβ–‘Ο† ➝ β—‡(βˆΌΟ†)
                        source
                        def LO.Modal.Entailment.multiDiaDuality {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
                        𝓒 ⊒! β—‡^[n]Ο† β­€ βˆΌβ–‘^[n](βˆΌΟ†)
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem LO.Modal.Entailment.multidia_duality! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
                          𝓒 ⊒ β—‡^[n]Ο† β­€ βˆΌβ–‘^[n](βˆΌΟ†)
                          source
                          def LO.Modal.Entailment.multidiaDuality_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
                          𝓒 ⊒! β—‡^[n]Ο† ➝ βˆΌβ–‘^[n](βˆΌΟ†)
                          Equations
                          Instances For
                            source
                            def LO.Modal.Entailment.diaDuality_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                            𝓒 ⊒! β—‡Ο† ➝ βˆΌβ–‘(βˆΌΟ†)
                            Equations
                            Instances For
                              source
                              def LO.Modal.Entailment.multidiaDuality_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
                              𝓒 ⊒! βˆΌβ–‘^[n](βˆΌΟ†) ➝ β—‡^[n]Ο†
                              Equations
                              Instances For
                                source
                                def LO.Modal.Entailment.diaDuality_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                                𝓒 ⊒! βˆΌβ–‘(βˆΌΟ†) ➝ β—‡Ο†
                                Equations
                                Instances For
                                  source
                                  def LO.Modal.Entailment.diaDuality'.mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} (h : 𝓒 ⊒! β—‡Ο†) :
                                  𝓒 ⊒! βˆΌβ–‘(βˆΌΟ†)
                                  Equations
                                  Instances For
                                    source
                                    def LO.Modal.Entailment.diaDuality'.mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} (h : 𝓒 ⊒! βˆΌβ–‘(βˆΌΟ†)) :
                                    𝓒 ⊒! β—‡Ο†
                                    Equations
                                    Instances For
                                      source
                                      @[simp]
                                      theorem LO.Modal.Entailment.multidia_duality!_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
                                      𝓒 ⊒ β—‡^[n]Ο† ➝ βˆΌβ–‘^[n](βˆΌΟ†)
                                      source
                                      @[simp]
                                      theorem LO.Modal.Entailment.dia_duality!_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                                      𝓒 ⊒ β—‡Ο† ➝ βˆΌβ–‘(βˆΌΟ†)
                                      source
                                      @[simp]
                                      theorem LO.Modal.Entailment.multidia_duality!_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
                                      𝓒 ⊒ βˆΌβ–‘^[n](βˆΌΟ†) ➝ β—‡^[n]Ο†
                                      source
                                      @[simp]
                                      theorem LO.Modal.Entailment.dia_duality!_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                                      𝓒 ⊒ βˆΌβ–‘(βˆΌΟ†) ➝ β—‡Ο†
                                      source
                                      theorem LO.Modal.Entailment.dia_duality'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} :
                                      𝓒 ⊒ β—‡Ο† ↔ 𝓒 ⊒ βˆΌβ–‘(βˆΌΟ†)
                                      source
                                      theorem LO.Modal.Entailment.multidia_duality'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
                                      𝓒 ⊒ β—‡^[n]Ο† ↔ 𝓒 ⊒ βˆΌβ–‘^[n](βˆΌΟ†)
                                      source
                                      def LO.Modal.Entailment.multiboxDuality {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
                                      𝓒 ⊒! β–‘^[n]Ο† β­€ βˆΌβ—‡^[n](βˆΌΟ†)
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        @[simp]
                                        theorem LO.Modal.Entailment.multibox_duality! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
                                        𝓒 ⊒ β–‘^[n]Ο† β­€ βˆΌβ—‡^[n](βˆΌΟ†)
                                        source
                                        def LO.Modal.Entailment.multiboxDuality_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
                                        𝓒 ⊒! β–‘^[n]Ο† ➝ βˆΌβ—‡^[n](βˆΌΟ†)
                                        Equations
                                        Instances For
                                          source
                                          def LO.Modal.Entailment.boxDuality_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                                          𝓒 ⊒! β–‘Ο† ➝ βˆΌβ—‡(βˆΌΟ†)
                                          Equations
                                          Instances For
                                            source
                                            def LO.Modal.Entailment.multiboxDuality_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
                                            𝓒 ⊒! βˆΌβ—‡^[n](βˆΌΟ†) ➝ β–‘^[n]Ο†
                                            Equations
                                            Instances For
                                              source
                                              def LO.Modal.Entailment.boxDuality_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                                              𝓒 ⊒! βˆΌβ—‡(βˆΌΟ†) ➝ β–‘Ο†
                                              Equations
                                              Instances For
                                                source
                                                @[simp]
                                                theorem LO.Modal.Entailment.multibox_duality_mp! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
                                                𝓒 ⊒ β–‘^[n]Ο† ➝ βˆΌβ—‡^[n](βˆΌΟ†)
                                                source
                                                theorem LO.Modal.Entailment.multibox_duality_mp'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] (h : 𝓒 ⊒ β–‘^[n]Ο†) :
                                                𝓒 ⊒ βˆΌβ—‡^[n](βˆΌΟ†)
                                                source
                                                @[simp]
                                                theorem LO.Modal.Entailment.multibox_duality_mpr! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] :
                                                𝓒 ⊒ βˆΌβ—‡^[n](βˆΌΟ†) ➝ β–‘^[n]Ο†
                                                source
                                                theorem LO.Modal.Entailment.multibox_duality_mpr'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {n : β„•} {Ο† : F} [DecidableEq F] (h : 𝓒 ⊒ βˆΌβ—‡^[n](βˆΌΟ†)) :
                                                𝓒 ⊒ β–‘^[n]Ο†
                                                source
                                                def LO.Modal.Entailment.boxDuality {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                                                𝓒 ⊒! β–‘Ο† β­€ βˆΌβ—‡(βˆΌΟ†)
                                                Equations
                                                Instances For
                                                  source
                                                  @[simp]
                                                  theorem LO.Modal.Entailment.box_duality! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                                                  𝓒 ⊒ β–‘Ο† β­€ βˆΌβ—‡(βˆΌΟ†)
                                                  source
                                                  @[simp]
                                                  theorem LO.Modal.Entailment.boxDuality_mp! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                                                  𝓒 ⊒ β–‘Ο† ➝ βˆΌβ—‡(βˆΌΟ†)
                                                  source
                                                  def LO.Modal.Entailment.boxDuality_mp' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] (h : 𝓒 ⊒! β–‘Ο†) :
                                                  𝓒 ⊒! βˆΌβ—‡(βˆΌΟ†)
                                                  Equations
                                                  Instances For
                                                    source
                                                    theorem LO.Modal.Entailment.boxDuality_mp'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] (h : 𝓒 ⊒ β–‘Ο†) :
                                                    𝓒 ⊒ βˆΌβ—‡(βˆΌΟ†)
                                                    source
                                                    @[simp]
                                                    theorem LO.Modal.Entailment.boxDuality_mpr! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                                                    𝓒 ⊒ βˆΌβ—‡(βˆΌΟ†) ➝ β–‘Ο†
                                                    source
                                                    def LO.Modal.Entailment.boxDuality_mpr' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] (h : 𝓒 ⊒! βˆΌβ—‡(βˆΌΟ†)) :
                                                    𝓒 ⊒! β–‘Ο†
                                                    Equations
                                                    Instances For
                                                      source
                                                      theorem LO.Modal.Entailment.boxDuality_mpr'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] (h : 𝓒 ⊒ βˆΌβ—‡(βˆΌΟ†)) :
                                                      𝓒 ⊒ β–‘Ο†