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

Question

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?

Answer 1

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").

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] is due to Löb." As well as the entry "Provability Logic" 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]".

Answer 2

Both results are due to Feferman. They appear as Lemma 3.10 and Corollary 5.5 of Arithmetization of metamathematics in a general setting, Fundamenta Mathematicae 49:35-92, 1960.