Who first proved that we can prove that we prove things we prove?

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?

• Motivation: I would like to cite it appropriately in my answer to this question, since it's a simultaneously useful and subtle enough point that it deserves a good citation IMO. – Noah Schweber Dec 30 '16 at 20:11
• Let me live neath your spell Do do that voodoo that you do so well – Will Jagy Dec 30 '16 at 20:36
• @WillJagy I'm not proud to say that my mind went instead to "Shoop" azlyrics.com/lyrics/saltnpepa/shoop.html – Todd Trimble Dec 30 '16 at 20:44
• I have always heard the theorem $\Box P \Rightarrow \Box\Box P$ referred to as one of the Hilbert-Bernays, or Hilbert-Bernays-Löb provability conditions. In his books 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." – Gro-Tsen Dec 30 '16 at 20:56
• @WillJagy That was awesomely delivered. Gotta love Harvey Korman. – Todd Trimble Dec 30 '16 at 21:53

The theorem $\Box P \Rightarrow \Box\Box P$ is due to Martin Löb and first appears in his 1955 paper "Solution of a Problem of Leon Henkin", J. Symb. Logic 20 115–118: it appears as condition (V) (page 116) in the paper in question, and whereas conditions (I)–(IV) are referred there to the earlier (1939) book by Hilbert and Bernays, Grundlagen der Mathematik, condition (V) (although easily deduced from the others) is new.
The reasoning "that a strong enough theory of arithmetic proves every true $\Sigma_1$ sentence" is exactly the one which Löb uses in his proof (if we grant that "$\exists x.(f(x)=0)$" for a recursive $f$ qualifies as "every $\Sigma_1$ sentence").