*Sorry about the title, I couldn't resist.*

It's a classic fact that, not only does $PA$ prove every true $\Sigma_1$ sentence, but $PA$ *proves* that $PA$ proves every true $\Sigma_1$ sentence! In particular, restricting attention to $\Sigma_1$ sentences of the form "$PA$ proves ---", in the modal logic of $PA$-provability we have $$\Box(\Box p\implies \Box\Box p).$$

Indeed, even more is true: in the paper Oracle bites theory, Visser states

It is well known that, in the context of EA, all theories extending the very weak arithmetic R prove all true $\Sigma_1$-sentences.

And various proofs of these facts can be found in various places.

My question is: who first proved (and where) that a strong enough theory of arithmetic proves every true $\Sigma_1$ sentence, and moreover proves that it proves every true $\Sigma_1$ sentence?

The Logic of Provability(1995), chapter 2, G. Boolos writes that "Hilbert and Bernays had listed three somewhat ungainly conditions […]. The isolation of (the attractive) (i), (ii), and (iii) [essentially as on Wikipedia] is due to Löb." $\endgroup$16more comments