[FOM] Is Con_Q provable in Q?

[Richard Zach]

Hi Arnon,

The problem is that Q doesn't prove the "provability conditions," so the
standard proofs of the 2nd incomleteness theorem don't work.  (Recall
that Q doesn't even prove commutativity of addition!)

I think it was first shown that Q in fact doesn't prove Con(Q) by
Bezboruah and Shepherdson (Gödel's Second Incompleteness Theorem for Q 
The Journal of Symbolic Logic, Vol. 41, No. 2. (1976), pp. 503-512) but
more more informative results have been available since the work of
Wilkie and Paris on weak fragments of arithmetic, e.g., Pudlák, Cuts,
Consistency Statements and Interpretations, 
The Journal of Symbolic Logic, Vol. 50, No. 2. (1985), pp. 423-441).

See also the references in Bezboruah & Sheperdson's paper to discussions
of the philosophical implications of the (non)derivability of the
provability conditions.  Kreisel argues that a predicate Pr doesn't
count as a provability predicate for a theory T unless T proves the
provability conditions for Pr. (Counterexamples, ie, predicates Pr which
binumerate the provability relation in strong theories such as PA but
for which Con_Pr is provable are familiar from Sol Feferman's
Arithmetization paper.)

Best,
Richard



On Sat, 2005-05-28 at 10:20 +0300, 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?
> 
> Thanks
> 
> Arnon Avron
> 
> School of CS
> Tel-Aviv University
>