[FOM] Is Con_Q provable in Q?
Curtis Franks
cfranks at uci.edu
Sun May 29 17:57:45 EDT 2005
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
More information about the FOM
mailing list