  The axiom (4): \(\Box A\rightarrow \Box \Box A\) is provable in \(\mathbf{GL}\), so \(\mathbf{GL}\) is actually a strengthening of \(\mathbf{K4}\). However, axioms such as \((M): \Box A\rightarrow A\), and even the weaker \((D): \Box A\rightarrow \Diamond A\) are not available (nor desirable) in \(\mathbf{GL}\). In provability logic, provability is not to be treated as a brand of necessity. The reason is that when \(p\) is provable in an arbitrary system \(\mathbf{S}\) for mathematics, it does not follow that \(p\) is true, since \(\mathbf{S}\) may be unsound. Furthermore, if \(p\) is provable in \(\mathbf{S} (\Box p)\) it need not even follow that \({\sim}p\) lacks a proof \(({\sim}\Box{\sim}p = \Diamond p). \mathbf{S}\) might be inconsistent and so prove both \(p\) and \({\sim}p\).