[FOM] Godel's First/corrected

[Harvey Friedman]

This is a continuation of
http://www.cs.nyu.edu/pipermail/fom/2006-March/010207.html

The new versions I gave of Godel's First there were too strong. I think they
are false as stated.

So, I do NOT have anything really new to say about Godel's First here.
HOWEVER, I do have a lot of questions.

By the way, I really should have given those formulations of Godel's First
using many sorted logic, since, as they stand, they do not include Godel's
First for set theories. Here are the corrected statements.

We again start with the well known versions due to R.M. Robinson:

THEOREM 1. Let T be a consistent many sorted theory whose language contains
a sort for natural numbers and the theory Q on that sort. 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 many sorted theory whose language contains
a sort for natural numbers and the theory Q on that sort. 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.

Perhaps the last conclusion about complete r.e. is not due to R.M. Robinson?

1. UNIVERSALLY QUANTIFIED BOUNDED SENTENCES.

Universally quantified bounded sentences are sentences in L(Q) of the form

(forall x1,...,xk)(phi)

where phi is a formula whose quantifiers are all bounded to the variables
x1,...,xk. Here < is defined as usual in Q, although Q proves very little
about <. 

THEOREM 1.1. Let T be a consistent many sorted theory whose language
contains a sort for natural numbers and the theory Q on that sort. Assume
that the set of axioms of T is recursive. Then there is a universally
quantified bounded sentence that is neither provable nor refutable in T.

THEOREM 1.2. Let T be a consistent many sorted theory whose language
contains a sort for natural numbers and the theory Q on that sort. Then the
set of all universally quantified bounded sentences that are provable in T
is not recursive. Also the set of all universally quantified bounded
sentences that are refutable in T is not recursive. Moreover, if the set of
axioms of T is recursive, then these two sets are complete r.e.

It is easy to derive Theorem 1.1 from Theorem 1.2.

In Theorem 1.1 we can arrange for the universally quantified bounded
sentences to have the form

(forall x1,...,xn)(therexists y1,...,ym < max(x1,...,xn))(phi)

where phi is quantifier free.

Using Matiyasevich's nine variable theorem, we can get away with n = m = 9.
Can you do better (without improving on Matiyasevich)? Also, it would be
nicer to insist that phi is an equation between polynomials presented with
coefficients that are numerals (i.e., of the form S...S0). Does that cost
any quantifiers?

2. DIOPHANTINE SENTENCES.

Diophantine sentences are sentences in L(Q) of the form

(forall x1,...,xk)(P(x1,...,xk) not= Q(x1,...,xk))

where P,Q are presented as polynomials whose coefficients are numerals;
i.e., S...S0. 

THEOREM 2.1. Let T be a consistent many sorted theory whose language
contains a sort for natural numbers and the theory Q on that sort. Assume
that the set of axioms of T is recursive. Then there is a true Diophantine
sentence that is not provable in T.

Using Matiyasevich, one can get a Diophantine sentence with in Theorem 2.1
with 9 quantifiers. In fact, we give a sketch of the following.

THEOREM 2.2. There is a nine quantifier Diophantine formula phi(n) with only
the free variable n such that the following holds. Let T be a consistent
many sorted theory whose language contains a sort for natural numbers and
the theory Q on that sort. Assume that the set of axioms of T is recursive.
Then there exists n such that phi(n*) is true but unprovable in T.

Theorem 2.2 is straightforward, and also easily implies Theorem 3.1. Let
phi(n) be a nine quantifier Diophantine formula such that {n: phi(n)} is not
recursive. Suppose that for all n, if phi(n*) is true then phi(n*) is
provable in T. Obviously if phi(n*) is provable in T then phi(n*) is true,
since T is consistent and extends Q. Hence {n: phi(n)} is r.e. and co-r.e.
Therefore {n: phi(n)} is recursive, which is a contradiction. QED

When I wrote http://www.cs.nyu.edu/pipermail/fom/2006-March/010207.html I
thought I could strengthen Theorems 2.1 and 2.2 to have the Diophantine
sentence neither provable nor refutable in T. I now doubt that this can be
done. Can you prove that it cannot be done? This question is also asked by
Martin Davis in http://www.cs.nyu.edu/pipermail/fom/2006-March/010226.html

3. OVER EFA.

If we replace Q by EFA, then there is no problem strengthening Theorems 2.1
and 2.2, in light of the known thorough treatment of Hilbert's 10th problem
in EFA = exponential function arithmetic = ISigma0(exp).

THEOREM 3.1. Let T be a consistent many sorted theory whose language
contains a sort for natural numbers and the theory EFA on that sort. Assume
that the set of axioms of T is recursive. Then there is a Diophantine
sentence that is neithe provable nor refutable in T.

THEOREM 3.2. There is a nine quantifier Diophantine formula phi(n) with only
the free variable n such that the following holds. Let T be a consistent
many sorted theory whose language contains a sort for natural numbers and
the theory EFA on that sort. Assume that the set of axioms of T is
recursive. Then there exists n such that phi(n*) is neither provable nor
refutable in T. 

Can we get away with something (significantly) weaker than EFA here? For
instance, what about PFA = polynomial function arithmetic = ISigma0, and
that natural hierarchy of well studied systems strictly between ISigma0 and
EFA?

Harvey Friedman