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?