Documentation

Foundation.Modal.Entailment.E

source
def LO.Entailment.C_replace {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.Minimal 𝓒] {Οˆβ‚ φ₁ Ο†β‚‚ Οˆβ‚‚ : F} [HasAxiomImply₁ 𝓒] [HasAxiomImplyβ‚‚ 𝓒] (h₁ : 𝓒 ⊒! Οˆβ‚ ➝ φ₁) (hβ‚‚ : 𝓒 ⊒! Ο†β‚‚ ➝ Οˆβ‚‚) :
𝓒 ⊒! φ₁ ➝ Ο†β‚‚ β†’ 𝓒 ⊒! Οˆβ‚ ➝ Οˆβ‚‚
Equations
Instances For
    source
    def LO.Modal.Entailment.ELLNN! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : 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 F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
      𝓒 ⊒ β–‘Ο† β­€ β–‘(βˆΌβˆΌΟ†)
      source
      def LO.Modal.Entailment.ILLNN! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : 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 F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
        𝓒 ⊒ β–‘Ο† ➝ β–‘(βˆΌβˆΌΟ†)
        source
        def LO.Modal.Entailment.box_dni {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
            𝓒 ⊒ β–‘(βˆΌβˆΌΟ†) ➝ β–‘Ο†
            source
            def LO.Modal.Entailment.box_dne {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] (h : 𝓒 ⊒ β–‘(βˆΌβˆΌΟ†)) :
                𝓒 ⊒ β–‘Ο†
                source
                def LO.Modal.Entailment.INMNL! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : 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 F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                  𝓒 ⊒ βˆΌβ—‡(βˆΌΟ†) ➝ β–‘Ο†
                  source
                  def LO.Modal.Entailment.INLMN! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : 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 F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                    𝓒 ⊒ βˆΌβ–‘Ο† ➝ β—‡(βˆΌΟ†)
                    source
                    def LO.Modal.Entailment.multiDiaDuality {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                                  𝓒 ⊒ βˆΌβ–‘(βˆΌΟ†) ➝ β—‡Ο†
                                  source
                                  theorem LO.Modal.Entailment.dia_duality'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} :
                                  𝓒 ⊒ β—‡Ο† ↔ 𝓒 ⊒ βˆΌβ–‘(βˆΌΟ†)
                                  source
                                  theorem LO.Modal.Entailment.multidia_duality'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                                              𝓒 ⊒ β–‘Ο† ➝ βˆΌβ—‡(βˆΌΟ†)
                                              source
                                              def LO.Modal.Entailment.boxDuality_mp' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : 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 F S] {𝓒 : 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 F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] :
                                                𝓒 ⊒ βˆΌβ—‡(βˆΌΟ†) ➝ β–‘Ο†
                                                source
                                                def LO.Modal.Entailment.boxDuality_mpr' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : 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 F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] (h : 𝓒 ⊒ βˆΌβ—‡(βˆΌΟ†)) :
                                                  𝓒 ⊒ β–‘Ο†
                                                  source
                                                  instance LO.Modal.Entailment.HasAxiomFour.of_dual {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.E 𝓒] [DecidableEq F] (h : (Ο† : F) β†’ 𝓒 ⊒! β—‡β—‡Ο† ➝ β—‡Ο†) :
                                                  HasAxiomFour 𝓒
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  source
                                                  def LO.Modal.Entailment.axiomFourDual! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] [HasAxiomFour 𝓒] :
                                                  𝓒 ⊒! β—‡β—‡Ο† ➝ β—‡Ο†
                                                  Equations
                                                  Instances For
                                                    source
                                                    @[simp]
                                                    theorem LO.Modal.Entailment.axiomFourDual {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] [HasAxiomFour 𝓒] :
                                                    𝓒 ⊒ β—‡β—‡Ο† ➝ β—‡Ο†
                                                    source
                                                    def LO.Modal.Entailment.axiomFiveDual! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] [HasAxiomFive 𝓒] :
                                                    𝓒 ⊒! β—‡β–‘Ο† ➝ β–‘Ο†
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      source
                                                      @[simp]
                                                      theorem LO.Modal.Entailment.axiomFiveDual {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] [HasAxiomFive 𝓒] :
                                                      𝓒 ⊒ β—‡β–‘Ο† ➝ β–‘Ο†
                                                      source
                                                      def LO.Modal.Entailment.axiomTDual! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] [HasAxiomT 𝓒] :
                                                      𝓒 ⊒! Ο† ➝ β—‡Ο†
                                                      Equations
                                                      Instances For
                                                        source
                                                        @[simp]
                                                        theorem LO.Modal.Entailment.axiomTDual {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓒 : S} [Entailment.E 𝓒] {Ο† : F} [DecidableEq F] [HasAxiomT 𝓒] :
                                                        𝓒 ⊒ Ο† ➝ β—‡Ο†