[FOM] Strong forms of Gödel's incompletenewss theorem

[Martin Davis]

In a recent FOM post, Harvey Friedman noted the theorem:

 >THEOREM 3. Let T be a consistent extension of Q, whose language contains
 >L(Q). Assume that the set of axioms of T is recursive. Then there is an
 >A...A sentence of L(Q) that is neither provable nor refutable in T. (No
 >bounded existential quantifiers allowed).

Using Yuri Matiyasevich's reduction of the number of unknowns in a 
universal Diophantine equation to 9, we can easily see that the prefix 
A...A in the above can be assumed to be of length 9 provided we replace 
"consistent" by "omega-consistent" in the statement. Can the same be said 
if we stick to simple consistency?

Martin