 The first detailed proof of the second incompleteness theorem appeared in (Hilbert &amp; Bernays 1939) (mainly written by Bernays), though only for one specific theory, PA. It uses a rather awkward set of conditions for the provability predicate. These were more technical lemmas for the needs of a particular proof and not any sort of analysis of “natural” provability predicates. A much more elegant, now standard list of “derivability conditions” was presented by Löb (1955)—though their intended use was somewhat different (see below).