# Does robinson arithmetic satisfy modal logic's “axiom 4”?

Does Robinson arithmetic prove the theorem "if sigma is provable then 'sigma is provable' is provable' for a fixed sentence sigma?

It's clear to me that you can get a primitive recursive function f from (proofs of sigma) to (proofs of "there is a proof of sigma"). Q can represent f, but can it actually prove that f has this property?

If not, then how do you get Godel's second incompleteness theorem for Q?

-

This is the third Hilbert-Bernays-Löb derivability condition.

My source (Mendelson, Introduction to Mathematical Logic) just asserts it and notes that it "requires a careful and difficult proof". The impression I get is that this careful and difficult proof is indeed claimed to be doable in System Q, but that is not stated in so many words.

Mendelson refers to Boolos, The Logic of Provability (1993), ch. 2, and Shoenfield, Mathematical Logic (1967), pp. 211-213 -- neither of which I have.

Edit: This answer to an earlier question claims that Q itself cannot verify the HBL conditions.

-
It's would seem amazing for $Q$ to be able to prove something like this, since $Q$ does not have induction, and one would seem to want to prove such a thing by induction on the size of the assumed proof. – JDH Dec 11 '11 at 2:20
@JDH: Good point. – Henning Makholm Dec 11 '11 at 2:22
I was interested in this a few months ago and looked into it some. As far as I can tell, the common belief is that $Q$ is not able to prove the derivability conditions, but at the same time I was not able to find an actual proof in print that $Q$ does not prove them. However, there are published proofs that the conclusion of the second incompleteness theorem holds for $Q$, and these proofs simply avoid the derivability conditions altogether. – Carl Mummert Dec 11 '11 at 2:50
Oh I see. Q can't prove Con(Q) for the same reason it can't prove the derivability condition: because it's so weak that it can't prove much of anything. It probably can't even prove that the various ways of saying Con(Q) are equivalent. – Larry D'Anna Dec 12 '11 at 1:55