 If this is read arithmetically, the direction from left to right is just the formalized version of Gödel’s second incompleteness theorem: if a sufficiently strong formal theory \(T\) like Peano Arithmetic does not prove a contradiction, then it is not provable in \(T\) that \(T\) does not prove a contradiction. Thus, sufficiently strong consistent arithmetical theories cannot prove their own consistency. We will turn to study the relation between provability logic and arithmetic more precisely in  Section 4,  but to that end another “modal” aspect of GL needs to be provided first: semantics.