Documentation

Foundation.Modal.System

class LO.System.HasDiaDuality {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
Type (max u_2 u_3)
Instances
    class LO.System.Necessitation {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
    Type (max u_2 u_3)
    • nec : {p : F} → 𝓢 p𝓢 p
    Instances
      class LO.System.Unnecessitation {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
      Type (max u_2 u_3)
      • unnec : {p : F} → 𝓢 p𝓢 p
      Instances
        class LO.System.LoebRule {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
        Type (max u_2 u_3)
        Instances
          class LO.System.HenkinRule {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
          Type (max u_2 u_3)
          Instances
            class LO.System.HasAxiomK {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
            Type (max u_2 u_3)
            Instances
              class LO.System.HasAxiomT {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
              Type (max u_2 u_3)
              Instances
                class LO.System.HasAxiomD {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
                Type (max u_2 u_3)
                Instances
                  class LO.System.HasAxiomP {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
                  Type u_3
                  • P : 𝓢 LO.Axioms.P
                  Instances
                    class LO.System.HasAxiomB {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
                    Type (max u_2 u_3)
                    Instances
                      class LO.System.HasAxiomFour {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
                      Type (max u_2 u_3)
                      Instances
                        class LO.System.HasAxiomFive {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
                        Type (max u_2 u_3)
                        Instances
                          class LO.System.HasAxiomL {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
                          Type (max u_2 u_3)
                          Instances
                            class LO.System.HasAxiomDot2 {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
                            Type (max u_2 u_3)
                            Instances
                              class LO.System.HasAxiomDot3 {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
                              Type (max u_2 u_3)
                              Instances
                                class LO.System.HasAxiomGrz {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
                                Type (max u_2 u_3)
                                Instances
                                  class LO.System.HasAxiomTc {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
                                  Type (max u_2 u_3)
                                  Instances
                                    class LO.System.HasAxiomVer {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
                                    Type (max u_2 u_3)
                                    Instances
                                      class LO.System.HasAxiomH {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :
                                      Type (max u_2 u_3)
                                      Instances
                                        class LO.System.KT {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomT :
                                        Type (max u_2 u_3)
                                          Instances
                                            class LO.System.KD {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomD :
                                            Type (max u_2 u_3)
                                              Instances
                                                class LO.System.K4 {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomFour :
                                                Type (max u_2 u_3)
                                                  Instances
                                                      Instances
                                                          Instances
                                                            class LO.System.S4Dot2 {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.S4 , LO.System.HasAxiomDot2 :
                                                            Type (max u_2 u_3)
                                                              Instances
                                                                class LO.System.S4Dot3 {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.S4 , LO.System.HasAxiomDot3 :
                                                                Type (max u_2 u_3)
                                                                  Instances
                                                                    class LO.System.S4Grz {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.S4 , LO.System.HasAxiomGrz :
                                                                    Type (max u_2 u_3)
                                                                      Instances
                                                                        class LO.System.GL {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomL :
                                                                        Type (max u_2 u_3)
                                                                          Instances
                                                                            class LO.System.Grz {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomGrz :
                                                                            Type (max u_2 u_3)
                                                                              Instances
                                                                                  Instances
                                                                                    class LO.System.Ver {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomVer :
                                                                                    Type (max u_2 u_3)
                                                                                      Instances
                                                                                        class LO.System.K4H {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K4 , LO.System.HasAxiomH :
                                                                                        Type (max u_2 u_3)
                                                                                          Instances
                                                                                            class LO.System.K4Loeb {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K4 , LO.System.LoebRule :
                                                                                            Type (max u_2 u_3)
                                                                                              Instances
                                                                                                class LO.System.K4Henkin {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K4 , LO.System.HenkinRule :
                                                                                                Type (max u_2 u_3)
                                                                                                  Instances
                                                                                                    def LO.System.nec {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [self : LO.System.Necessitation 𝓢] {p : F} :
                                                                                                    𝓢 p𝓢 p

                                                                                                    Alias of LO.System.Necessitation.nec.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      theorem LO.System.nec! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Necessitation 𝓢] :
                                                                                                      𝓢 ⊢! p𝓢 ⊢! p
                                                                                                      def LO.System.multinec {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Necessitation 𝓢] {n : } :
                                                                                                      𝓢 p𝓢 □^[n]p
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        theorem LO.System.multinec! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Necessitation 𝓢] {n : } :
                                                                                                        𝓢 ⊢! p𝓢 ⊢! □^[n]p
                                                                                                        def LO.System.axiomK {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.HasAxiomK 𝓢] :
                                                                                                        𝓢 (p q) p q
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[simp]
                                                                                                          theorem LO.System.axiomK! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.HasAxiomK 𝓢] :
                                                                                                          𝓢 ⊢! (p q) p q
                                                                                                          Equations
                                                                                                          def LO.System.axiomK' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 (p q)) :
                                                                                                          𝓢 p q
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[simp]
                                                                                                            theorem LO.System.axiomK'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢! (p q)) :
                                                                                                            𝓢 ⊢! p q
                                                                                                            def LO.System.axiomK'' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] (h₁ : 𝓢 (p q)) (h₂ : 𝓢 p) :
                                                                                                            𝓢 q
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[simp]
                                                                                                              theorem LO.System.axiomK''! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] (h₁ : 𝓢 ⊢! (p q)) (h₂ : 𝓢 ⊢! p) :
                                                                                                              𝓢 ⊢! q
                                                                                                              def LO.System.multibox_axiomK {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } :
                                                                                                              𝓢 □^[n](p q) □^[n]p □^[n]q
                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              Instances For
                                                                                                                @[simp]
                                                                                                                theorem LO.System.multibox_axiomK! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } :
                                                                                                                𝓢 ⊢! □^[n](p q) □^[n]p □^[n]q
                                                                                                                def LO.System.multibox_axiomK' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } (h : 𝓢 □^[n](p q)) :
                                                                                                                𝓢 □^[n]p □^[n]q
                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[simp]
                                                                                                                  theorem LO.System.multibox_axiomK'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } (h : 𝓢 ⊢! □^[n](p q)) :
                                                                                                                  theorem LO.System.multiboxed_imply_distribute! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } (h : 𝓢 ⊢! □^[n](p q)) :

                                                                                                                  Alias of LO.System.multibox_axiomK'!.

                                                                                                                  @[simp]
                                                                                                                  theorem LO.System.box_iff! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢! p q) :
                                                                                                                  𝓢 ⊢! p q
                                                                                                                  def LO.System.multiboxIff' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } (h : 𝓢 p q) :
                                                                                                                  𝓢 □^[n]p □^[n]q
                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[simp]
                                                                                                                    theorem LO.System.multibox_iff! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } (h : 𝓢 ⊢! p q) :
                                                                                                                    Equations
                                                                                                                    • LO.System.instHasDiaDualityOfModalDeMorganOfHasAxiomDNE = { dia_dual := fun (p : F) => .mpr (LO.System.iffId (p)) }
                                                                                                                    Equations
                                                                                                                    def LO.System.diaDuality {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasDiaDuality 𝓢] :
                                                                                                                    𝓢 p (p)
                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[simp]
                                                                                                                      theorem LO.System.dia_duality! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasDiaDuality 𝓢] :
                                                                                                                      def LO.System.diaDuality_mp {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasDiaDuality 𝓢] :
                                                                                                                      𝓢 p (p)
                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[simp]
                                                                                                                        theorem LO.System.diaDuality_mp! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasDiaDuality 𝓢] :
                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[simp]
                                                                                                                          theorem LO.System.diaDuality_mpr! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasDiaDuality 𝓢] :
                                                                                                                          def LO.System.diaDuality'.mp {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasDiaDuality 𝓢] (h : 𝓢 p) :
                                                                                                                          𝓢 (p)
                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            def LO.System.diaDuality'.mpr {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasDiaDuality 𝓢] (h : 𝓢 (p)) :
                                                                                                                            𝓢 p
                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              theorem LO.System.dia_duality'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasDiaDuality 𝓢] :
                                                                                                                              𝓢 ⊢! p 𝓢 ⊢! (p)
                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For
                                                                                                                                def LO.System.diaIff' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] (h : 𝓢 p q) :
                                                                                                                                𝓢 p q
                                                                                                                                Equations
                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                Instances For
                                                                                                                                  @[simp]
                                                                                                                                  theorem LO.System.dia_iff! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] (h : 𝓢 ⊢! p q) :
                                                                                                                                  𝓢 ⊢! p q
                                                                                                                                  def LO.System.multidiaIff' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] {n : } (h : 𝓢 p q) :
                                                                                                                                  𝓢 ◇^[n]p ◇^[n]q
                                                                                                                                  Equations
                                                                                                                                  Instances For
                                                                                                                                    @[simp]
                                                                                                                                    theorem LO.System.multidia_iff! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] {n : } (h : 𝓢 ⊢! p q) :
                                                                                                                                    Equations
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For
                                                                                                                                      Equations
                                                                                                                                      • LO.System.boxDuality = LO.System.multiboxDuality
                                                                                                                                      Instances For
                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  @[simp]
                                                                                                                                                  theorem LO.System.box_dne! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :
                                                                                                                                                  def LO.System.box_dne' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 (p)) :
                                                                                                                                                  𝓢 p
                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    theorem LO.System.box_dne'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢! (p)) :
                                                                                                                                                    𝓢 ⊢! p
                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[simp]
                                                                                                                                                      Equations
                                                                                                                                                      • LO.System.boxverum = LO.System.multiboxverum
                                                                                                                                                      Instances For
                                                                                                                                                        @[simp]
                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[simp]
                                                                                                                                                          theorem LO.System.imply_multibox_distribute'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } (h : 𝓢 ⊢! p q) :
                                                                                                                                                          theorem LO.System.imply_box_distribute'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢! p q) :
                                                                                                                                                          𝓢 ⊢! p q
                                                                                                                                                          def LO.System.distribute_multibox_and {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } :
                                                                                                                                                          𝓢 □^[n](p q) □^[n]p □^[n]q
                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            @[simp]
                                                                                                                                                            theorem LO.System.distribute_multibox_and! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } :
                                                                                                                                                            𝓢 ⊢! □^[n](p q) □^[n]p □^[n]q
                                                                                                                                                            def LO.System.distribute_box_and {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :
                                                                                                                                                            𝓢 (p q) p q
                                                                                                                                                            Equations
                                                                                                                                                            • LO.System.distribute_box_and = LO.System.distribute_multibox_and
                                                                                                                                                            Instances For
                                                                                                                                                              @[simp]
                                                                                                                                                              theorem LO.System.distribute_box_and! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :
                                                                                                                                                              𝓢 ⊢! (p q) p q
                                                                                                                                                              def LO.System.distribute_multibox_and' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } (h : 𝓢 □^[n](p q)) :
                                                                                                                                                              𝓢 □^[n]p □^[n]q
                                                                                                                                                              Equations
                                                                                                                                                              Instances For
                                                                                                                                                                theorem LO.System.distribute_multibox_and'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } (d : 𝓢 ⊢! □^[n](p q)) :
                                                                                                                                                                theorem LO.System.distribute_box_and'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (d : 𝓢 ⊢! (p q)) :
                                                                                                                                                                𝓢 ⊢! p q
                                                                                                                                                                theorem LO.System.conj_cons! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {Γ : List F} {𝓢 : S} [LO.System.Classical 𝓢] :
                                                                                                                                                                𝓢 ⊢! p Γ (p :: Γ)
                                                                                                                                                                def LO.System.collect_multibox_and {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } :
                                                                                                                                                                𝓢 □^[n]p □^[n]q □^[n](p q)
                                                                                                                                                                Equations
                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                Instances For
                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem LO.System.collect_multibox_and! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } :
                                                                                                                                                                  𝓢 ⊢! □^[n]p □^[n]q □^[n](p q)
                                                                                                                                                                  def LO.System.collect_box_and {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :
                                                                                                                                                                  𝓢 p q (p q)
                                                                                                                                                                  Equations
                                                                                                                                                                  • LO.System.collect_box_and = LO.System.collect_multibox_and
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[simp]
                                                                                                                                                                    theorem LO.System.collect_box_and! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :
                                                                                                                                                                    𝓢 ⊢! p q (p q)
                                                                                                                                                                    def LO.System.collect_multibox_and' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } (h : 𝓢 □^[n]p □^[n]q) :
                                                                                                                                                                    𝓢 □^[n](p q)
                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      theorem LO.System.collect_multibox_and'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } (h : 𝓢 ⊢! □^[n]p □^[n]q) :
                                                                                                                                                                      𝓢 ⊢! □^[n](p q)
                                                                                                                                                                      def LO.System.collect_box_and' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 p q) :
                                                                                                                                                                      𝓢 (p q)
                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        theorem LO.System.collect_box_and'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢! p q) :
                                                                                                                                                                        𝓢 ⊢! (p q)
                                                                                                                                                                        theorem LO.System.multiboxConj'_iff! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {Γ : List F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } :
                                                                                                                                                                        𝓢 ⊢! □^[n]Γ pΓ, 𝓢 ⊢! □^[n]p
                                                                                                                                                                        theorem LO.System.boxConj'_iff! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {Γ : List F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :
                                                                                                                                                                        𝓢 ⊢! Γ pΓ, 𝓢 ⊢! p
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem LO.System.multibox_cons_conjAux₁! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {Γ : List F} {𝓢 : S} [LO.System.Classical 𝓢] {n : } :
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem LO.System.multibox_cons_conjAux₂! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {Γ : List F} {𝓢 : S} [LO.System.Classical 𝓢] {n : } :
                                                                                                                                                                        𝓢 ⊢! □'^[n](p :: Γ) □^[n]p
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem LO.System.multibox_cons_conj! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {Γ : List F} {𝓢 : S} [LO.System.Classical 𝓢] {n : } :
                                                                                                                                                                        def LO.System.collect_multibox_or {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } :
                                                                                                                                                                        𝓢 □^[n]p □^[n]q □^[n](p q)
                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem LO.System.collect_multibox_or! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } :
                                                                                                                                                                          𝓢 ⊢! □^[n]p □^[n]q □^[n](p q)
                                                                                                                                                                          def LO.System.collect_box_or {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :
                                                                                                                                                                          𝓢 p q (p q)
                                                                                                                                                                          Equations
                                                                                                                                                                          • LO.System.collect_box_or = LO.System.collect_multibox_or
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[simp]
                                                                                                                                                                            theorem LO.System.collect_box_or! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :
                                                                                                                                                                            𝓢 ⊢! p q (p q)
                                                                                                                                                                            def LO.System.collect_multibox_or' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } (h : 𝓢 □^[n]p □^[n]q) :
                                                                                                                                                                            𝓢 □^[n](p q)
                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              theorem LO.System.collect_multibox_or'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : } (h : 𝓢 ⊢! □^[n]p □^[n]q) :
                                                                                                                                                                              𝓢 ⊢! □^[n](p q)
                                                                                                                                                                              def LO.System.collect_box_or' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 p q) :
                                                                                                                                                                              𝓢 (p q)
                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                theorem LO.System.collect_box_or'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢! p q) :
                                                                                                                                                                                𝓢 ⊢! (p q)
                                                                                                                                                                                Equations
                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                Instances For
                                                                                                                                                                                  Equations
                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    Equations
                                                                                                                                                                                    • LO.System.collect_dia_or = LO.System.or₃'' LO.System.diaOrInst₁ LO.System.diaOrInst₂
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      def LO.System.collect_dia_or' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] (h : 𝓢 p q) :
                                                                                                                                                                                      𝓢 (p q)
                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[simp]
                                                                                                                                                                                        theorem LO.System.collect_dia_or'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] (h : 𝓢 ⊢! p q) :
                                                                                                                                                                                        𝓢 ⊢! (p q)
                                                                                                                                                                                        def LO.System.boxdotAxiomK {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] :
                                                                                                                                                                                        𝓢 (p q) p q
                                                                                                                                                                                        Equations
                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem LO.System.boxdot_axiomK! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] :
                                                                                                                                                                                          𝓢 ⊢! (p q) p q
                                                                                                                                                                                          def LO.System.boxdotAxiomT {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] :
                                                                                                                                                                                          𝓢 p p
                                                                                                                                                                                          Equations
                                                                                                                                                                                          • LO.System.boxdotAxiomT = LO.System.and₁
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem LO.System.boxdot_axiomT! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] :
                                                                                                                                                                                            𝓢 ⊢! p p
                                                                                                                                                                                            def LO.System.boxdotNec {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] (d : 𝓢 p) :
                                                                                                                                                                                            𝓢 p
                                                                                                                                                                                            Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              theorem LO.System.boxdot_nec! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] (d : 𝓢 ⊢! p) :
                                                                                                                                                                                              𝓢 ⊢! p
                                                                                                                                                                                              def LO.System.boxdotBox {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] :
                                                                                                                                                                                              𝓢 p p
                                                                                                                                                                                              Equations
                                                                                                                                                                                              • LO.System.boxdotBox = LO.System.and₂
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                theorem LO.System.boxdot_box! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] :
                                                                                                                                                                                                𝓢 ⊢! p p
                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  def LO.System.axiomT {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomT 𝓢] :
                                                                                                                                                                                                  𝓢 p p
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    @[simp]
                                                                                                                                                                                                    theorem LO.System.axiomT! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomT 𝓢] :
                                                                                                                                                                                                    𝓢 ⊢! p p
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    def LO.System.axiomT' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomT 𝓢] (h : 𝓢 p) :
                                                                                                                                                                                                    𝓢 p
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      @[simp]
                                                                                                                                                                                                      theorem LO.System.axiomT'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomT 𝓢] (h : 𝓢 ⊢! p) :
                                                                                                                                                                                                      𝓢 ⊢! p
                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        @[simp]
                                                                                                                                                                                                        def LO.System.diaTc' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomT 𝓢] (h : 𝓢 p) :
                                                                                                                                                                                                        𝓢 p
                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          theorem LO.System.diaTc'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomT 𝓢] (h : 𝓢 ⊢! p) :
                                                                                                                                                                                                          𝓢 ⊢! p
                                                                                                                                                                                                          def LO.System.axiomB {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomB 𝓢] :
                                                                                                                                                                                                          𝓢 p p
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            @[simp]
                                                                                                                                                                                                            theorem LO.System.axiomB! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomB 𝓢] :
                                                                                                                                                                                                            𝓢 ⊢! p p
                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            def LO.System.axiomD {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomD 𝓢] :
                                                                                                                                                                                                            𝓢 p p
                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              @[simp]
                                                                                                                                                                                                              theorem LO.System.axiomD! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomD 𝓢] :
                                                                                                                                                                                                              𝓢 ⊢! p p
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                • LO.System.instHasAxiomP = { P := LO.System.P_of_D }
                                                                                                                                                                                                                def LO.System.axiomP {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.HasAxiomP 𝓢] :
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                • LO.System.axiomP = LO.System.HasAxiomP.P
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                                  theorem LO.System.axiomP! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.HasAxiomP 𝓢] :
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  • LO.System.instHasAxiomD = { D := fun (x : F) => LO.System.D_of_P }
                                                                                                                                                                                                                  def LO.System.axiomFour {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomFour 𝓢] :
                                                                                                                                                                                                                  𝓢 p p
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    @[simp]
                                                                                                                                                                                                                    theorem LO.System.axiomFour! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomFour 𝓢] :
                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    def LO.System.axiomFour' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomFour 𝓢] (h : 𝓢 p) :
                                                                                                                                                                                                                    𝓢 p
                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      def LO.System.axiomFour'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomFour 𝓢] (h : 𝓢 ⊢! p) :
                                                                                                                                                                                                                      𝓢 ⊢! p
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      • =
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              • =
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                • LO.System.iff_Box_BoxBoxdot = LO.System.iffIntro LO.System.imply_Box_BoxBoxdot LO.System.imply_BoxBoxdot_Box
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    @[simp]
                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        def LO.System.iff_box_boxdot {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomT 𝓢] :
                                                                                                                                                                                                                                        𝓢 p p
                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                          @[simp]
                                                                                                                                                                                                                                          theorem LO.System.iff_box_boxdot! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomT 𝓢] :
                                                                                                                                                                                                                                          𝓢 ⊢! p p
                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                            def LO.System.axiomFive {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomFive 𝓢] :
                                                                                                                                                                                                                                            𝓢 p p
                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              @[simp]
                                                                                                                                                                                                                                              theorem LO.System.axiomFive! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomFive 𝓢] :
                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                      def LO.System.axiomTc {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomTc 𝓢] :
                                                                                                                                                                                                                                                      𝓢 p p
                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                        @[simp]
                                                                                                                                                                                                                                                        theorem LO.System.axiomTc! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomTc 𝓢] :
                                                                                                                                                                                                                                                        𝓢 ⊢! p p
                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                        • LO.System.instHasAxiomFour = { Four := fun (x : F) => LO.System.axiomFour_of_Tc }
                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                          @[simp]
                                                                                                                                                                                                                                                          def LO.System.diaT' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomTc 𝓢] [LO.System.HasDiaDuality 𝓢] (h : 𝓢 p) :
                                                                                                                                                                                                                                                          𝓢 p
                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                            theorem LO.System.diaT'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasAxiomTc 𝓢] [LO.System.HasDiaDuality 𝓢] (h : 𝓢 ⊢! p) :
                                                                                                                                                                                                                                                            𝓢 ⊢! p
                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                            • LO.System.instHasAxiomFive = { Five := fun (x : F) => LO.System.axiomFive_of_Tc }
                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                            • LO.System.instHasAxiomGrzOfHasAxiomT = { Grz := fun (x : F) => LO.System.axiomGrz_of_Tc_and_T }
                                                                                                                                                                                                                                                            def LO.System.axiomVer {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomVer 𝓢] :
                                                                                                                                                                                                                                                            𝓢 p
                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                              @[simp]
                                                                                                                                                                                                                                                              theorem LO.System.axiomVer! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomVer 𝓢] :
                                                                                                                                                                                                                                                              𝓢 ⊢! p
                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                              • LO.System.instHasAxiomTc = { Tc := fun (x : F) => LO.System.axiomTc_of_Ver }
                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                              • LO.System.instHasAxiomL = { L := fun (x : F) => LO.System.axiomL_of_Ver }
                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                  def LO.System.axiomL {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomL 𝓢] :
                                                                                                                                                                                                                                                                  𝓢 (p p) p
                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                    @[simp]
                                                                                                                                                                                                                                                                    theorem LO.System.axiomL! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomL 𝓢] :
                                                                                                                                                                                                                                                                    𝓢 ⊢! (p p) p
                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    • LO.System.instHasAxiomFour_1 = { Four := fun (x : F) => LO.System.axiomFour_of_L }
                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                      • LO.System.instHasAxiomH = { H := fun (x : F) => LO.System.axiomH_of_GL }
                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                        def LO.System.axiomH {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomH 𝓢] :
                                                                                                                                                                                                                                                                        𝓢 (p p) p
                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                          @[simp]
                                                                                                                                                                                                                                                                          theorem LO.System.axiomH! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomH 𝓢] :
                                                                                                                                                                                                                                                                          𝓢 ⊢! (p p) p
                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                          def LO.System.loeb {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [self : LO.System.LoebRule 𝓢] {p : F} :
                                                                                                                                                                                                                                                                          𝓢 p p𝓢 p

                                                                                                                                                                                                                                                                          Alias of LO.System.LoebRule.loeb.

                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                            theorem LO.System.loeb! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.LoebRule 𝓢] :
                                                                                                                                                                                                                                                                            𝓢 ⊢! p p𝓢 ⊢! p
                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                            • LO.System.instHasAxiomLOfK4Loeb = { L := fun (x : F) => LO.System.axiomL_of_K4Loeb }
                                                                                                                                                                                                                                                                            def LO.System.henkin {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [self : LO.System.HenkinRule 𝓢] {p : F} :
                                                                                                                                                                                                                                                                            𝓢 p p𝓢 p

                                                                                                                                                                                                                                                                            Alias of LO.System.HenkinRule.henkin.

                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                              theorem LO.System.henkin! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HenkinRule 𝓢] :
                                                                                                                                                                                                                                                                              𝓢 ⊢! p p𝓢 ⊢! p
                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                              def LO.System.unnec {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [self : LO.System.Unnecessitation 𝓢] {p : F} :
                                                                                                                                                                                                                                                                              𝓢 p𝓢 p

                                                                                                                                                                                                                                                                              Alias of LO.System.Unnecessitation.unnec.

                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                theorem LO.System.unnec! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Unnecessitation 𝓢] :
                                                                                                                                                                                                                                                                                𝓢 ⊢! p𝓢 ⊢! p
                                                                                                                                                                                                                                                                                def LO.System.multiunnec {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Unnecessitation 𝓢] {n : } :
                                                                                                                                                                                                                                                                                𝓢 □^[n]p𝓢 p
                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                  theorem LO.System.multiunnec! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Unnecessitation 𝓢] {n : } :
                                                                                                                                                                                                                                                                                  𝓢 ⊢! □^[n]p𝓢 ⊢! p
                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                  • LO.System.instUnnecessitationOfHasAxiomT = { unnec := fun {p : F} (hp : 𝓢 p) => LO.System.axiomThp }
                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                    def LO.System.imply_boxdot_axiomT_of_imply_boxdot_boxdot {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] (h : 𝓢 p q) :
                                                                                                                                                                                                                                                                                    𝓢 p q q
                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                      theorem LO.System.imply_boxdot_axiomT_of_imply_boxdot_boxdot! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] (h : 𝓢 ⊢! p q) :
                                                                                                                                                                                                                                                                                      𝓢 ⊢! p q q
                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                        def LO.System.axiomGrz {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomGrz 𝓢] :
                                                                                                                                                                                                                                                                                        𝓢 ((p p) p) p
                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                          @[simp]
                                                                                                                                                                                                                                                                                          theorem LO.System.axiomGrz! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomGrz 𝓢] :
                                                                                                                                                                                                                                                                                          𝓢 ⊢! ((p p) p) p
                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                          noncomputable def LO.System.lemma_Grz₁ {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :
                                                                                                                                                                                                                                                                                          𝓢 p ((p (p p) (p (p p))) p (p p))
                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                              • LO.System.instHasAxiomFour_2 = { Four := fun (x : F) => LO.System.Four_of_Grz }
                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                              • LO.System.instHasAxiomT = { T := fun (x : F) => LO.System.T_of_Grz }
                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                              • LO.System.instHasAxiomTcOfHasAxiomTOfHasAxiomFiveOfHasAxiomGrzOfHasDiaDuality = { Tc := fun (x : F) => LO.System.Tc_of_S5Grz }
                                                                                                                                                                                                                                                                                              theorem LO.System.contextual_nec! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {Γ : List F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : Γ ⊢[𝓢]! p) :
                                                                                                                                                                                                                                                                                              (□'Γ) ⊢[𝓢]! p
                                                                                                                                                                                                                                                                                              class LO.System.ModalDisjunctive {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] {S : Type u_2} [LO.System F S] (𝓢 : S) :
                                                                                                                                                                                                                                                                                              Instances
                                                                                                                                                                                                                                                                                                theorem LO.System.ModalDisjunctive.modal_disjunctive {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] {S : Type u_2} [LO.System F S] {𝓢 : S} [self : LO.System.ModalDisjunctive 𝓢] {p : F} {q : F} :
                                                                                                                                                                                                                                                                                                𝓢 ⊢! p q𝓢 ⊢! p 𝓢 ⊢! q
                                                                                                                                                                                                                                                                                                theorem LO.System.Context.provable_iff_boxed {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] {S : Type u_2} [LO.System F S] [DecidableEq F] {𝓢 : S} [LO.System.Minimal 𝓢] {X : Set F} {p : F} :
                                                                                                                                                                                                                                                                                                (□''X) *⊢[𝓢]! p ∃ (Δ : List F), (q□'Δ, q □''X) (□'Δ) ⊢[𝓢]! p