 Henkin on the other hand wanted to know whether anything could be said about sentences asserting their own provability: supposing that Peano Arithmetic proves \(B \leftrightarrow \Prov(\ulcorner B \urcorner)\), what does this imply about \(B\)? Three years later, M. Löb took up the challenge and answered Henkin’s question in a surprising way. Even though all sentences provable in Peano Arithmetic are indeed true about the natural numbers, Löb showed that the formalized version of this fact, \(\Prov(\ulcorner B \urcorner) \rightarrow B\), can be proved in Peano Arithmetic only in the trivial case that Peano Arithmetic already proves \(B\) itself. This result, now called Löb’s theorem, immediately answers Henkin’s question. (For a proof of Löb’s theorem, see  Section 4.)  Löb also showed a formalized version of his theorem, namely that Peano Arithmetic proves