[FOM] Is Con_Q provable in Q?

[Curtis Franks]

Arnon Avron wrote:

> In all texts I know about Godel second incompleteness theorem (the
> theorem about consistency proofs), it is proved for theories which
> are "strong enough", where "strong enough" means: consistent axiomatic
> extensions of PRA. My intuition, which is not very reliable, tells me
> that the theorem should apply also to weaker theories, for example: to
> Robinson's arithmetics Q. Can anybody give me references to works 
> which might be relevant to this question?

My impression is that the answer to this question is very subtle and 
remains one area where foundations research turns critically on one's 
philosphical and methodological point of view.

The most crucial reference for your specific question is Bezboruah and 
Sheperdson's 1976 "G/"odel's Second Incompleteness Theorem for Q" from 
the JSL. They prove the theorem in its standard form for Q.

It is worth pointing out that Kriesel anticipated this result nearly 25 
years earlier and suggested that even if his conjecture were true, the 
theorem would probably not be very meaningful. Bezboruah and Sheperdson 
echo this sentiment in their own study, "We must agree with Kriesel that 
this [theorem] is devoid of any philosophical interst and that in such a 
weak system this formula cannot be said to express consistency but only 
an algebraic property which in a stronger system ... could reasonably be 
said to express the consistency of Q." One attempt to explain the 
problem of a theory "understanding" the metatheoretic content of its own 
theorems is in terms of the intensionality of the arithmetization being 
used. This is the topic of Feferman's famous 1971 study. In short, one 
might say that since Q does not prove salient facts about for example 
the provability predicate used in the proof (e. g. that it is closed 
under modus ponens), the fact that this particular theorem expresses the 
unprovability in Q of Q's consistency is one that we can verify only 
extensionally--i. e. only after stepping outside of the constraints of 
Robinson's theory, presumably to a setting where questions about Q's 
consistency already are assumed.

(In his discussion in his book on Hilbert's Program, Detlefsen 
describe's descriptions of intensional arithmetizations as attempted 
solutions to the stability problem that he poses for the 
Hilbert-Bernay's-L/:ob derivability conditions, and he questions these 
attempts on the grounds that they favor a particularly realist 
philosophy. I recommend studying Detlefsen's argument if you are 
interested in the traditional philosophy of math concerns around the issue.)

The contemporary view is that Q can prove the unprovability of it's own 
consistency even granting Kreisel, Bezboruah, and Shepherdson's concern. 
The argument is due to Pavel Pudl/'ak [1994 essay for G/"odel Society 
"On the Length of Proofs of Consistency"]: Since the theory 
$I/Delta_0+/Omega_1$ interprets the consistency of Q unambiguously and 
proves G/"odel's second incompleteness theorem for Q, and since 
$I/Delta_0+/Omega_1$ is interpretable in Q, Q proves not only G/"odel's 
second incompleteness theorem but also ``the unprovability of Q's 
consistency'' by virtue of the fact that Bezboruah and Shepherdson's 
proof can be strengthened to the following.

Theorem: Q proves that it is consistent to assume that there is a 
contradiction encoded already by a number in a proper syntactic cut of 
its numbers. This syntactic cut can be shortened using a method of 
Solovay so that it is a definition in Q of a model of I-/Delta_0 + 
/Omega_1 which ``interprets'' consistency unproblematically.

Pudl/'ak argues that this allows a sort of semantic bootstrapping from Q 
to I-/Delta_0 + /Omega_1.

Pudl'ak's argument has gained a lot of support. For example Buss cites 
the possibility of an intensional arithmetization of syntax in Q in the 
second chapter of the Handbook of Proof Theory. I, however, question the 
argument on two points. First, I do not believe that I-/Delta_0 + 
/Omega_1 which "interprets consistency unproblematically". In fact, 
several formualtions of consistency do separate in the theory. This is 
because the predicates that say "there is a standard Hilbert style proof 
of y", "there is a finite Herbrand disjunction of the open matrix of y", 
and "there is a cut-free sequence calculus proof of y" are not provably 
equivalent in I-/Delta_0 + /Omega_1. This is not a purely academic 
point, because in bounded arithmetic thre is reason to think that some 
of the more "nonstandard" formualtions of provability are primative. 
Second, I question the coherence of the semantic bootstrapping argument 
in general. While the standard provability predicates relativized to the 
appropriate syntactic cuts do meet Feferman's criteria for 
intensionality, it is questionable whether these criteria are 
appropriate in the weak setting of Robinson's theory. Since this theory 
doesn't even prove Herbrand's theorem, it is not clear that closure 
under modus ponens is part of the essential content of provability for 
that theory.

Finally, it is worth noting that Herbrand's famous finitistic proof of 
the consistency of the arithmetic he defines is, as he points out, 
formalizable in that theory. In the appendix he wrote to that study he 
points out that G/"odel's theorem does not contradict his result, 
because Herbrand's arithmetic cannot define itself. From the point of 
view that I have presented above, we might say then that the derivation 
of the consistency of Herbrand's theory can be formalized in Herbrand's 
theory, but that it takes some additional reasoning external to that 
theory to determine that the formal object is a consistency proof of the 
theory. A question then might be whether G/:odel's second theorem arises 
in all theories that exhibit self-reference. In the case of Q, we have 
both self-reference and G/"odel's theorem, but we may not have the 
metatheoretic content of G/"odel's theorem. So the relationship between 
self-refernce and the unprovability of consistency is delicate.

Curtis Franks
Dept. Logic and Philosophy of Science
University of California, Irvine