To recall, the Hilbert-Bernays-Löb derivability conditions state that $\operatorname{Bew}$ is a derivability predicate if for any pair of sentences $S, T$:
- If $S$ is provable, so is $\operatorname{Bew}(\ulcorner S\urcorner)$.
- $\operatorname{Bew}(\ulcorner S \rightarrow T \urcorner) \rightarrow \bigl(\operatorname{Bew}(\ulcorner S \urcorner) \rightarrow \operatorname{Bew}(\ulcorner T \urcorner)\bigr)$ is provable.
- $\operatorname{Bew}(\ulcorner S \urcorner) \rightarrow \operatorname{Bew}\bigl(\ulcorner \operatorname{Bew}(\ulcorner S \urcorner)\urcorner\bigr)$ is provable.
And it's typically the last condition that gets singled out as he one that causes all the headaches. But what about the second one? On page 44 of the book The Logic of Provability George Boolos verifies this condition simply as follows:
Let $S$ and $T$ be sentences of PA. Then $\vdash \operatorname{Bew}(\ulcorner(S \rightarrow T)\urcorner) \rightarrow (\operatorname{Bew}(\ulcorner S \urcorner) \rightarrow \operatorname{Bew}(\ulcorner T \urcorner))$.
Proof. It is sufficient to observe that $$ \vdash \operatorname{Pf}(y, \ulcorner(S \rightarrow T)\urcorner) \land \operatorname{Pf}(y', \ulcorner S \urcorner) \rightarrow \operatorname{Pf}(y^*y'^*[\ulcorner T \urcorner], \ulcorner T \urcorner) $$ (Intuitively, since modus ponens is one of the two rules of inference of PA, the finite sequence whose values are those of a proof of $S \rightarrow T$, followed by those of a proof of $S$, followed by the sentence $T$, is a proof of $T$.) $\quad\dashv$
(The $^*$-operator denotes concatenation and the pair of square brackets turns its arguments into a sequence.)
I don't see how the above constitutes a proof at all. To me it seems to just slightly rephrase the theorem. Yes, the parenthetical remark Boolos makes is undoubtedly true. But why is it the case that PA proves the formalization of this remark? The more I think about it, the more it seems to me that this fact must rely on a host of minor details of $\operatorname{Pf}$.