[FOM] Is Con_Q provable in Q?

[Arnold Beckmann]

On Sun, 29 May 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?


   The general consistency statement is very strong, Wilkie and
Paris have shown that I\Sigma_0+Exp cannot prove Con(Q)  [1]
(whereas this theory proves restricted forms of Con(Q) like
cut-free consistency of Q). Restricted consistency statements
have been intensively studied in the area of the finite
axiomatizability problem of bounded arithmetic.  E.g., Buss in
his book [2] showed that his theory S^1_2 (which is related to
the complexity class P) can formalize syntax, and he proved
Goedel's incompleteness theorems for S^i_2 for several notions of
formalized derivability like the general (unrestricted) one,
resp. derivability where all occurring formulas are bounded.  On
the other hand, such bounded consitency statements are still too
strong to settle the finite axiomatizability probelm of bounded
arithmetic:  Pudlak has shown that bounded consistency of S^1_2
is not a consequence of the whole bounded arithmetic S_2 (S_2 is
the same as I\Delta_0+\Omega_1) [3].

   Section V.5 in Hajek and Pudlak [4] discusses such results.
Krajicek's book [5] summarizes uses of restricted consistency
notions in the area of the finite axiomatizability problem.


[1] A.Wilkie and J.Paris: On the Scheme of Induction for Bounded
Arithmetic Formulas. APAL, 35: 261-302, 1987.

[2] S.Buss: Bounded Arithmetic. Bibliopolis, 1986.

[3] P.Pudlak, A note on bounded arithmetic, Fund.Math., 136(2)
(1990) pp. 85--89.

[4] P.Hajek and P. Pudlak: Metamathematics of First-Order
Arithmetic. Perspectives in Mathematical Logic, Springer-Verlag,
1993.

[5] J.Krajicek: Bounded Arithmetic, Propositional Logic, and
Complexity Theory. Cambridge University Press, 1995.


Arnold Beckmann


Dr. Arnold Beckmann   |          University of Wales, Swansea
                      |                      Computer Science
                      |
                      |                 a.beckmann at swan.ac.uk
                      |   http://www.cs.swan.ac.uk/~csarnold/