 Under the assumption that a provability predicate for a theory satisfies the derivability conditions (or, by Jeroslow’s trick, at least D1 and D2) it is relatively easy to prove the relevant case of the second incompleteness theorem. However, in practise one has to establish whether a proposed arithmetized provability predicate really satisfies the conditions case by case, and typically this is long and tedious.