4
$\begingroup$

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?

1 Answers 1

2

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.

  • 0
    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.2011-12-12