[FOM] Godel's First

[Harvey Friedman]

I would like to start two threads on Godel's incompleteness theorems. Here I
start the first of these threads, on Godel's First incompleteness theorem.

My idea is that the FOM can serve to be the place of record that brings
together the state of the art knowledge of the sharpest formulations - e.g.,
weakest hypotheses and strongest conclusions. In particular, in the case of
Godel's Second, there are real serious issues of formulation. A clear
symptom of this is that at present, there is no decent way of teaching
Godel's Second without some substantial classroom handwaving.

In particular, I have no doubt that our understanding of Godel's First and
Second can be seriously strengthened by active participation of interested
parties in these two threads.

I am NOT talking about issues of natural independence results, about which I
regularly post (mainly) in my numbered postings.

Here are two strong forms of Godel's First that are  very well known.

Let Q be (Raphael) Robinson's system in the language L(Q) = 0,S,+,dot, with
equality, and the following proper axioms:

1. not Sx = 0.
2. Sx = Sy implies x = y.
3. not x = 0 implies (therexists y)(x = Sy).
4. x + 0 = x.
5. x + Sy = S(x + y).
6. x dot 0 = 0.
7. x dot Sy = (x dot y) + x.

THEOREM 1. 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 a
sentence of L(Q) that is neither provable nor refutable in T.

THEOREM 2. Let T be a consistent extension of Q, whose language contains
L(Q). Then the set of all sentences of L(Q) that are provable in T is not
recursive. Moreover, if T is recursively axiomatized, then the set of all
sentences of L(Q) that are provable in T is complete r.e.

I think that these Theorems are due to Raphael Robinson, but I am not sure
about the last claim of Theorem 2.

There is a small ambiguity concerning Theorem 2. What does "the set of
axioms of T is recursive" mean if the language L(T) is infinite?

The answer is that there is a one-one enumeration of the symbols of L(T)
such that on the basis of that enumeration, the set of axioms of T is
recursive. 

We now give a sharp extension of the above two theorems, that
seems to be somewhat sharper than what I have seen. I have not been keeping
up with the literature in this area, and so I hope somebody looking at this
will tell me where they were first proved.

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).

THEOREM 4. Let T be a consistent extension of Q, whose language contains
L(Q). Then the set of all A...A sentences of L(Q) that are provable in T is
not recursive. Also the set of all E...E sentences of L(Q) that are provable
in T is not recursive. Moreover, if the set of axioms of T is recursive,
then these two sets are complete r.e.

We can sharpen these further.

THEOREM 5. There is a fixed polynomial P of several variables, with integer
coefficients (positive, negative, or zero), such that the following holds.
Let T be a consistent extension of Q, whose language contains L(Q). Assume
that the set of axioms of T is recursive. Then for infinitely many n >= 0,
the sentence "P is somewhere n" is neither provable nor refutable in T.

THEOREM 6. There is a fixed polynomial P of several variables, with integer
coefficients (positive, negative, or zero), such that the following holds.
Let T be a consistent extension of Q, whose language contains L(Q). Then {n
>= 0: T proves that P is somewhere n} and {n >= 0: T proves that P is
nowhere n} are not recursive. Moreover, if the set of axioms of T is
recursive, then these two sets are complete r.e.

REMARK: When we say "somewhere" we can be referring either to arguments from
the nonnegative integers (the objects of the theory, since we are extending
Q), or the integers, positive, negative, or zero.

Note that in Theorems 5,6, we do not assume that T is 1-consistent. It is
also true that we do NOT use the Rosser trick. The Rosser trick might
introduce unwanted bounded existential quantifiers into the mix, and to
avoid this, we need to avoid the Rosser trick. Of course, also Theorems 5
and 6 use the solution to Hilbert's 10th problem by Y. Matiyasevich, J.
Robinson, M. Davis, H. Putnam, completed in 1970.

I hadn't realized before that one could eliminate Rosser's trick even for
proving that the far stronger system PA (far stronger than Q) is incomplete
under the assumption that PA is consistent. In fact, one does not need
Rosser's trick to show that PA is incomplete for Pi01 sentences.

Perhaps this is well known, but here is how it is done. Assume that PA is
complete for Pi01 sentences. A bit informally, let phi be the sentence

"phi is a Pi01 sentence that is not provable"

formalized using a suitable representation in PA of the supposed algorithm
for determining the provability of Pi01 sentences. (This supposed algorithm
exists because we have assumed that PA is complete for Pi01 sentences).

Note that phi is in fact a Pi01 sentence. The provability predicate that we
used must either demonstrability hold of phi or demonstrability fail of phi,
according to whether phi is provable in PA or refutable in PA. In the former
case, phi is refutable in PA, and therefore PA is inconsistent. In the
latter case, phi is provable in PA, and therefore PA is inconsistent. Since
PA has been assumed to be consistent, we have the desired contradiction.

In fact, the above argument shows that "the set of all Pi01 consequences of
PA is not recursive" without the Rosser trick, or using recursively
inseparable r.e. sets.

Harvey Friedman