What are some good expositions of the Hilbert-Bernays-Löb derivability conditions for PA?

Question

The Hilbert-Bernays-Löb derivability conditions state that for $P$ to be a provability predicate it must obey the following for all sentences $A, B$:

1. If $A$ is provable, so is $P(\ulcorner A\urcorner)$.
2. $P(\ulcorner A\urcorner) \rightarrow P\bigl(\ulcorner P(\ulcorner A\urcorner)\urcorner\bigr)$ is provable.
3. $P(\ulcorner A \rightarrow B \urcorner) \rightarrow \bigl(P(\ulcorner A \urcorner) \rightarrow P(\ulcorner B \urcorner)\bigr)$ is provable.

From these three conditions the second incompleteness theorem as well as Löb's theorem follow. However, the fact that PA has such a proof predicate is almost universally omitted, usually with a reference to Hilbert and Bernays' 1939 Volume II of Grundlagen der Mathematik. Surely there's been some improvements since then. Is a more modern treatment available somewhere?