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).
This is all I could find from Boolos (LoP).”Certain appreciably weaker systems, whose axioms do not include all of the induction axioms, suffice for the theory of finite sequences and the proofs of the derivability condtiions (for PA and for those weaker systems themselves). In those weaker theories, it should also be noted, stronger theorems about the syntax fo PA than those we have stated can also be proved. One example is the single sentence of the language of PA that generalizes condition (ii) [your (2)]…another is a similar generalization of conditions (iii) [your (3)].”He doesn’t say specifically what those “appreciably weaker systems” are, but later he proves the diagonal lemma specifically for Q. (The converse of (1) is also provable in Q–see his “Computability and Logic”.) Posted by lumpy pea coat
sorry for this comment but I have some questions and don’t know where to askI don’t understand why can we construct a set theory using math.logic and construct math. logic using a set theory…isn’t it incorrect construction(of foundations)?I can’t find answer in a books, net, google…maybe it’s trivial please help me, thanks