  In provability logics, \(\Box p\) is interpreted as a formula (of arithmetic) that expresses that what \(p\) denotes is provable in \(\mathbf{PA}\). Using this notation, sentences of provability logic express facts about provability. Suppose that \(\bot\) is a constant of provability logic denoting a contradiction. Then \({\sim}\Box \bot\) says that \(\mathbf{PA}\) is consistent and \(\Box A\rightarrow A\) says that \(\mathbf{PA}\) is sound in the sense that when it proves \(A, A\) is indeed true. Furthermore, the box may be iterated. So, for example, \(\Box{\sim}\Box \bot\) makes the dubious claim that \(\mathbf{PA}\) is able to prove its own consistency, and \({\sim}\Box \bot \rightarrow{\sim}\Box{\sim}\Box \bot\) asserts (correctly as Gödel proved) that if \(\mathbf{PA}\) is consistent then \(\mathbf{PA}\) is unable to prove its own consistency.