証明可能性論理GLの別定義
すなわち$ \mathfrak{H}_\mathsf{GL} = \mathfrak{H}_\mathsf{K} + \lbrack \Box(\Box \Phi \to \Phi) \to \Box \Phi \rbrack
一方，正規様相論理K4に様々な公理または規則を足しても証明能力が等価なものが得られるということもわかっている． ref:
Thm.$ \mathfrak{H}_\mathsf{K4}による$ \mathfrak{H}_\mathsf{GL}と等価な証明体系
Löb推論規則$ \mathrm{(L)} \colon \Box A \to A \mid A Löbの定理$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner \varphi \urcorner}) \to \varphi \implies T \vdash \varphi Henkin推論規則$ \mathrm{(H)} \colon \Box A \harr A \mid A Henkin文$ H（$ T \vdash H \leftrightarrow \mathrm{Pr}_T(\overline{\ulcorner H \urcorner})なる文$ H）がLöbの定理より$ T \vdash Hであることに対応． Henkin公理図式$ \mathbf{H} \colon \Box(\Box \Phi \harr \Phi) \to \Box \Phi としたとき，次が成り立つ．
$ \mathfrak{H}_\mathsf{GL} = \mathfrak{H}_\mathsf{K4} + (\mathrm{L}) = \mathfrak{H}_\mathsf{K4} + (\mathrm{H}) = \mathfrak{H}_\mathsf{K4} + \mathbf{H}