The other day, Arnon Avron asked on FOM whether the Second Incompleteness Theorem holds for Robinson’s Q. I remembered wondering about that myself back when I was preparing for the foundations qual. The issue is this: the usual proof of the unprovability of Con(T) requires that T is not just “sufficiently strong” in the usual sense, i.e., you can arithmetize syntax in T, but the provability predicate used to formalize Con(T) must satisfy the Hilbert-Bernays-Löb provability conditions:
- If T proves A, then T proves Pr(A)
- T proves Pr(A → B) → (Pr(A) → Pr(B))
- T proves Pr(A) → Pr(Pr(A))
Now Q doesn’t have induction, so it can prove only very few universal claims, in particular, it does not satisfy condition 3. (Does it satisfy condition 2?) So does Q prove Con(Q), i.e., ¬PrQ(0 = 1)? It does not. The first result to this effect, as far as I know, is Bezboruah and Shepherdson, Gödel’s Second Incompleteness Theorem for Q (JSL 1976). In the late 70s, Wilkie and others developed the model theory of weak fragments of arithmetic sufficiently for more informative results to be obtained, e.g., Pudlák’s 1985 “Cuts, consistency statements and interpretations.” Wilkie and Paris (On the scheme of induction for bounded arithmetic formulas, APAL 1987, Thm 3.5) showed that Con(Q) isn’t even provable in IΔ0 + exp.
I recommend Bezboruah and Shepherdson’s paper also for the references to the discussion in Kreisel’s papers and elsewhere about the philosophical significance of the derivability conditions. The classic treatment of the logic of provability predicates satisfying these conditions is Boolos’s Logic of Provability.
UPDATE: There are some good replies to Arnon’s question in the FOM archives, especially that by Curtis Franks and the one by Arnold Beckmann. Incidentally, Curtis’s post made me look up Buss’s article on proof theory of arithmetic in the Handbook of Proof Theory, where Buss formulates the Second Incompleteness Theorem as:
Let T be a decidable [should be: axiomatizable], consistent theory and suppose T ⊇ Q. The T does not prove Con(T). (p. 121).