Documentation

Logic.Modal.Axioms

@[reducible, inline]
abbrev LO.Axioms.DiaDuality {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] :
F

is duality of .

Equations
Instances For
    @[reducible, inline]
    Equations
    Instances For
      @[reducible, inline]
      abbrev LO.Axioms.K {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) (q : F) :
      F
      Equations
      Instances For
        @[reducible, inline]
        abbrev LO.Axioms.K.set {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] :
        Set F
        Equations
        Instances For
          @[reducible, inline]
          abbrev LO.Axioms.T {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) :
          F
          Equations
          Instances For
            @[reducible, inline]
            abbrev LO.Axioms.T.set {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] :
            Set F
            Equations
            Instances For
              @[reducible, inline]
              abbrev LO.Axioms.B {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] :
              F
              Equations
              Instances For
                @[reducible, inline]
                abbrev LO.Axioms.B.set {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] [LO.Dia F] :
                Set F
                Equations
                Instances For
                  @[reducible, inline]
                  abbrev LO.Axioms.B₂ {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) :
                  F

                  -only version of axiom 𝗕.

                  Equations
                  Instances For
                    @[reducible, inline]
                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev LO.Axioms.D {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] :
                      F
                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev LO.Axioms.D.set {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] [LO.Dia F] :
                        Set F
                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev LO.Axioms.D₂ {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] :
                          F

                          Alternative form of axiom 𝗗. In sight of provability logic, this can be seen as consistency of theory.

                          Equations
                          Instances For
                            @[reducible, inline]
                            Equations
                            Instances For
                              @[reducible, inline]
                              abbrev LO.Axioms.Four {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) :
                              F
                              Equations
                              Instances For
                                @[reducible, inline]
                                Equations
                                Instances For
                                  @[reducible, inline]
                                  abbrev LO.Axioms.Five {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] :
                                  F
                                  Equations
                                  Instances For
                                    @[reducible, inline]
                                    Equations
                                    Instances For
                                      @[reducible, inline]
                                      abbrev LO.Axioms.Five₂ {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) :
                                      F

                                      -only version of axiom 𝟱.

                                      Equations
                                      Instances For
                                        @[reducible, inline]
                                        Equations
                                        Instances For
                                          @[reducible, inline]
                                          abbrev LO.Axioms.Dot2 {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] :
                                          F
                                          Equations
                                          Instances For
                                            @[reducible, inline]
                                            Equations
                                            Instances For
                                              @[reducible, inline]
                                              abbrev LO.Axioms.C4 {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) :
                                              F
                                              Equations
                                              Instances For
                                                @[reducible, inline]
                                                Equations
                                                Instances For
                                                  @[reducible, inline]
                                                  abbrev LO.Axioms.CD {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] :
                                                  F
                                                  Equations
                                                  Instances For
                                                    @[reducible, inline]
                                                    abbrev LO.Axioms.CD.set {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] [LO.Dia F] :
                                                    Set F
                                                    Equations
                                                    Instances For
                                                      @[reducible, inline]
                                                      abbrev LO.Axioms.Tc {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) :
                                                      F
                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]
                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]
                                                          abbrev LO.Axioms.Ver {F : Type u_1} [LO.Box F] (p : F) :
                                                          F
                                                          Equations
                                                          Instances For
                                                            @[reducible, inline]
                                                            abbrev LO.Axioms.Ver.set {F : Type u_1} [LO.Box F] :
                                                            Set F
                                                            Equations
                                                            Instances For
                                                              @[reducible, inline]
                                                              abbrev LO.Axioms.Dot3 {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) (q : F) :
                                                              F
                                                              Equations
                                                              Instances For
                                                                @[reducible, inline]
                                                                Equations
                                                                Instances For
                                                                  @[reducible, inline]
                                                                  abbrev LO.Axioms.Grz {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) :
                                                                  F
                                                                  Equations
                                                                  Instances For
                                                                    @[reducible, inline]
                                                                    Equations
                                                                    Instances For
                                                                      @[reducible, inline]
                                                                      abbrev LO.Axioms.M {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] :
                                                                      F
                                                                      Equations
                                                                      Instances For
                                                                        @[reducible, inline]
                                                                        abbrev LO.Axioms.M.set {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] [LO.Dia F] :
                                                                        Set F
                                                                        Equations
                                                                        Instances For
                                                                          @[reducible, inline]
                                                                          abbrev LO.Axioms.L {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) :
                                                                          F
                                                                          Equations
                                                                          Instances For
                                                                            @[reducible, inline]
                                                                            abbrev LO.Axioms.L.set {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] :
                                                                            Set F
                                                                            Equations
                                                                            Instances For
                                                                              @[reducible, inline]
                                                                              abbrev LO.Axioms.H {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) :
                                                                              F
                                                                              Equations
                                                                              Instances For
                                                                                @[reducible, inline]
                                                                                abbrev LO.Axioms.H.set {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] :
                                                                                Set F
                                                                                Equations
                                                                                Instances For