[FOM] Is Con_Q provable in Q?

[carniell@cle.unicamp.br]

Dear Arnon:

Your intuition is right (at least this time :-)): Gödel´s second
incompleteness theorem also holds for Robinson's Arithmetic Q, cf.

A. Bezboruah, John C. Shepherdson: Godel's Second Incompleteness Theorem
for Q. The Journal of Symbolic Logic, Volume 41, Number 2, June 197, pp.
503-512.

See also Computability and Logic
G.Boolos and R. C. Jeffrey, Cambridge University Press, 2nd. edition, 1980
 (but there is also a 2002 edition).

However, it is possible to give a finitary consistency proof of Q within PA
(see especially p. 214 of J. R. Shoenfield, "Mathematical Logic",
Addison-Wesley, 1967).

We explain this in detail in chapter 24 of our book "Computability:
Computable Functions, Logic, and the Foundations of Mathematics, with
Computability: A Timeline" (R. L. Epstein and W. Carnielli, Wadsworth,
2000).

Best regards,


Walter Carnielli

Centre for Logic, Epistemology and the History of Science - CLE
State University of Campinas - UNICAMP
P.O. Box 6133, 13083-970 Campinas -SP, Brazil
http://www.cle.unicamp.br/prof/carnielli/

> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>