# 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. Dec 30, 2016 at 20:11
• Let me live neath your spell Do do that voodoo that you do so well Dec 30, 2016 at 20:36
• @WillJagy I'm not proud to say that my mind went instead to "Shoop" azlyrics.com/lyrics/saltnpepa/shoop.html Dec 30, 2016 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." Dec 30, 2016 at 20:56
• @WillJagy That was awesomely delivered. Gotta love Harvey Korman. Dec 30, 2016 at 21:53

## 2 Answers

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

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.

• I'd expect an earlier date: that paper's introduction says "in general the material in sections 2-4 is quite familiar". Jan 5, 2017 at 15:38
• I think Lob currently has my vote based on Gro-Tsen's answer, but +1: I'm pleased to know about that paper by Feferman! Jan 5, 2017 at 17:53