 was in a paper by Smiley in 1963 about the logical basis of ethics, which did not consider arithmetic at all. More relevant investigations, however, seriously started only almost twenty years after publication of Löb’s paper. The early 1970s saw the rapid development of propositional provability logic, where several researchers in different countries independently proved the most important results, discussed in Sections  2,  3, and  4.  Propositional provability logic turned out to capture exactly what many formal theories of arithmetic can say by propositional means about their own provability predicate. More recently, researchers have investigated the boundaries of this approach and have proposed several interesting more expressive extensions of provability logic (see  Section 5).