Documentation

Foundation.Modal.Hilbert.Systems

@[reducible, inline]
abbrev LO.Modal.Hilbert.K (α : Type u_1) :
Equations
Instances For
    instance LO.Modal.Hilbert.instIsNormalK (α : Type u_1) :
    (Hilbert.K α).IsNormal
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.ExtK {α : Type u_1} (Ax : Theory α) :
    Equations
    Instances For
      instance LO.Modal.Hilbert.instIsNormalExtK {α✝ : Type u_1} {Ax : Theory α✝} :
      (Hilbert.ExtK Ax).IsNormal
      theorem LO.Modal.Hilbert.ExtK.def_ax {α : Type u_1} {Ax : Theory α} :
      (Hilbert.ExtK Ax).axioms = 𝗞 Ax
      theorem LO.Modal.Hilbert.ExtK.maxm! {α : Type u_1} {Ax : Theory α} {φ : Formula α} (h : φ Ax) :
      @[reducible, inline]
      abbrev LO.Modal.Hilbert.KT (α : Type u_1) :
      Equations
      Instances For
        @[reducible, inline]
        abbrev LO.Modal.Hilbert.KB (α : Type u_1) :
        Equations
        Instances For
          @[reducible, inline]
          abbrev LO.Modal.Hilbert.KD (α : Type u_1) :
          Equations
          Instances For
            @[reducible, inline]
            abbrev LO.Modal.Hilbert.KP (α : Type u_1) :
            Equations
            Instances For
              @[reducible, inline]
              abbrev LO.Modal.Hilbert.KTB (α : Type u_1) :
              Equations
              Instances For
                @[reducible, inline]
                abbrev LO.Modal.Hilbert.K4 (α : Type u_1) :
                Equations
                Instances For
                  @[reducible, inline]
                  abbrev LO.Modal.Hilbert.K5 (α : Type u_1) :
                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev LO.Modal.Hilbert.KD45 (α : Type u_1) :
                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev LO.Modal.Hilbert.K45 (α : Type u_1) :
                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev LO.Modal.Hilbert.KB4 (α : Type u_1) :
                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev LO.Modal.Hilbert.KB5 (α : Type u_1) :
                          Equations
                          Instances For
                            @[reducible, inline]
                            abbrev LO.Modal.Hilbert.KDB (α : Type u_1) :
                            Equations
                            Instances For
                              @[reducible, inline]
                              abbrev LO.Modal.Hilbert.KD4 (α : Type u_1) :
                              Equations
                              Instances For
                                @[reducible, inline]
                                abbrev LO.Modal.Hilbert.KD5 (α : Type u_1) :
                                Equations
                                Instances For
                                  @[reducible, inline]
                                  abbrev LO.Modal.Hilbert.ExtS4 {α : Type u_1} (Ax : Theory α) :
                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem LO.Modal.Hilbert.ExtS4.def_ax {α✝ : Type u_1} {Ax : Theory α✝} :
                                    @[reducible, inline]
                                    abbrev LO.Modal.Hilbert.S4 (α : Type u_1) :
                                    Equations
                                    Instances For
                                      @[reducible, inline]
                                      abbrev LO.Modal.Hilbert.S4Dot2 (α : Type u_1) :
                                      Equations
                                      Instances For
                                        @[reducible, inline]
                                        abbrev LO.Modal.Hilbert.S4Dot3 (α : Type u_1) :
                                        Equations
                                        Instances For
                                          @[reducible, inline]
                                          abbrev LO.Modal.Hilbert.S4Grz (α : Type u_1) :
                                          Equations
                                          Instances For
                                            @[reducible, inline]
                                            abbrev LO.Modal.Hilbert.KT4B (α : Type u_1) :
                                            Equations
                                            Instances For
                                              @[reducible, inline]
                                              abbrev LO.Modal.Hilbert.S5 (α : Type u_1) :
                                              Equations
                                              Instances For
                                                @[reducible, inline]
                                                abbrev LO.Modal.Hilbert.Triv (α : Type u_1) :
                                                Equations
                                                Instances For
                                                  @[reducible, inline]
                                                  abbrev LO.Modal.Hilbert.Ver (α : Type u_1) :
                                                  Equations
                                                  Instances For
                                                    @[reducible, inline]
                                                    abbrev LO.Modal.Hilbert.GL (α : Type u_1) :
                                                    Equations
                                                    Instances For
                                                      @[reducible, inline]
                                                      abbrev LO.Modal.Hilbert.Grz (α : Type u_1) :
                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]
                                                        abbrev LO.Modal.Hilbert.GLS (α : Type u_1) :

                                                        Solovey's Provability Logic of True Arithmetic. Remark necessitation is not permitted.

                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]
                                                          abbrev LO.Modal.Hilbert.N (α : Type u_1) :

                                                          Logic of Pure Necessitation

                                                          Equations
                                                          Instances For
                                                            instance LO.Modal.Hilbert.instHasNecOnlyN (α : Type u_1) :
                                                            (Hilbert.N α).HasNecOnly