*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](http://dspace.library.uu.nl/bitstream/handle/1874/310731/preprint324.pdf?sequence=1), 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?



Who first proved that we can prove that we prove things we prove?
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"](http://www.math.umd.edu/~laskow/Pubs/713/Lob.pdf), *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").


As evidence that Löb was the first to state this fact, I offer the following quote from G. Boolos in *The Logic of Provability* (1995), chapter 2: "Hilbert and Bernays had listed three somewhat ungainly conditions […]. The isolation of (the attractive) (i), (ii), and (iii) [essentially as [on Wikipedia](https://en.wikipedia.org/wiki/Hilbert%E2%80%93Bernays_provability_conditions)] is due to Löb." As well as [the entry "Provability Logic"](https://plato.stanford.edu/entries/logic-provability/) from the Stanford Encyclopedia of Philosophy: "In the same paper, Löb formulated three conditions on the provability predicate of Peano Arithmetic, that form a useful modification of the complicated conditions that Hilbert and Bernays introduced in 1939 for their proof of Gödel's second incompleteness theorem [again the same conditions as on Wikipedia]".


