Documentation

Foundation.Modal.Kripke.Geach.Basic

@[reducible, inline]
Equations
Instances For
    @[reducible, inline]

    Frame class of Hilbert.KT

    Equations
    Instances For
      theorem LO.Modal.Kripke.ReflexiveFrameClass.is_geach :
      ReflexiveFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }]
      @[reducible, inline]

      Frame class of Hilbert.KD

      Equations
      Instances For
        theorem LO.Modal.Kripke.SerialFrameClass.is_geach :
        SerialFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }]
        @[reducible, inline]

        Frame class of Hilbert.KB

        Equations
        Instances For
          theorem LO.Modal.Kripke.SymmetricFrameClass.is_geach :
          SymmetricFrameClass.IsGeach [{ i := 0, j := 1, m := 0, n := 1 }]
          @[reducible, inline]

          Frame class of Hilbert.K4

          Equations
          Instances For
            theorem LO.Modal.Kripke.TransitiveFrameClass.is_geach :
            TransitiveFrameClass.IsGeach [{ i := 0, j := 2, m := 1, n := 0 }]
            @[reducible, inline]

            Frame class of Hilbert.K5

            Equations
            Instances For
              theorem LO.Modal.Kripke.EuclideanFrameClass.is_geach :
              EuclideanFrameClass.IsGeach [{ i := 1, j := 1, m := 0, n := 1 }]
              @[reducible, inline]

              Frame class of Hilbert.S5

              Equations
              Instances For
                theorem LO.Modal.Kripke.ReflexiveEuclideanFrameClass.is_geach :
                ReflexiveEuclideanFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }]
                @[reducible, inline]

                Frame class of Hilbert.KTB

                Equations
                Instances For
                  theorem LO.Modal.Kripke.ReflexiveSymmetricFrameClass.is_geach :
                  ReflexiveSymmetricFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }]
                  @[reducible, inline]

                  Frame class of Hilbert.S4

                  Equations
                  Instances For
                    theorem LO.Modal.Kripke.ReflexiveTransitiveFrameClass.is_geach :
                    ReflexiveTransitiveFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }]
                    theorem LO.Modal.Kripke.ReflexiveTransitiveConfluentFrameClass.is_geach :
                    ReflexiveTransitiveConfluentFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 1, j := 1, m := 1, n := 1 }]
                    theorem LO.Modal.Kripke.ReflexiveTransitiveSymmetricFrameClass.is_geach :
                    ReflexiveTransitiveSymmetricFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }]
                    theorem LO.Modal.Kripke.SerialTransitiveEuclideanFrameClass.is_geach :
                    SerialTransitiveEuclideanFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }]
                    @[reducible, inline]

                    Frame class of Hilbert.K45

                    Equations
                    Instances For
                      theorem LO.Modal.Kripke.TransitiveEuclideanFrameClass.is_geach :
                      TransitiveEuclideanFrameClass.IsGeach [{ i := 0, j := 2, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }]
                      @[reducible, inline]

                      Frame class of Hilbert.KB4

                      Equations
                      Instances For
                        theorem LO.Modal.Kripke.SymmetricTransitiveFrameClass.is_geach :
                        SymmetricTransitiveFrameClass.IsGeach [{ i := 0, j := 1, m := 0, n := 1 }, { i := 0, j := 2, m := 1, n := 0 }]
                        @[reducible, inline]

                        Frame class of Hilbert.KB5

                        Equations
                        Instances For
                          theorem LO.Modal.Kripke.SymmetricEuclideanFrameClass.is_geach :
                          SymmetricEuclideanFrameClass.IsGeach [{ i := 0, j := 1, m := 0, n := 1 }, { i := 1, j := 1, m := 0, n := 1 }]
                          @[reducible, inline]

                          Frame class of Hilbert.KDB

                          Equations
                          Instances For
                            theorem LO.Modal.Kripke.SerialSymmetricFrameClass.is_geach :
                            SerialSymmetricFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }, { i := 0, j := 1, m := 0, n := 1 }]
                            @[reducible, inline]

                            Frame class of Hilbert.KD4

                            Equations
                            Instances For
                              theorem LO.Modal.Kripke.SerialTransitiveFrameClass.is_geach :
                              SerialTransitiveFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }, { i := 0, j := 2, m := 1, n := 0 }]
                              @[reducible, inline]

                              Frame class of Hilbert.KD5

                              Equations
                              Instances For
                                theorem LO.Modal.Kripke.SerialEuclideanFrameClass.is_geach :
                                SerialEuclideanFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }, { i := 1, j := 1, m := 0, n := 1 }]