 The logical language of propositional provability logic contains, in addition to propositional atoms and the usual truth-functional operators as well as the contradiction symbol \(\bot\), a modal operator \(\Box\) with intended meaning “is provable in \(T\),” where \(T\) is a sufficiently strong formal theory, let us say Peano Arithmetic (see  Section 4).  \(\Diamond A\) is an abbreviation for \(\neg\,\Box\neg\, A\). Thus, the language is the same as that of modal systems such as K and S4 presented in the entry  modal logic.