FOM: ReplyToDavis

[Martin Davis]

At 03:00 AM 10/28/97 -0500, Harvey Friedman wrote:
>

>Specifically, one is unable to use MRDP to write down a specific
>Diophantine problem with this metamathematical property. In partcular I
>raise the, as far I know, open question:
>
>QUESTION: Is there a polynomial whose total representation in base 10 has
>at most 1000 symbols, for which the question of whether or not there is a
>solution is independent of ZFC?
>
>By total representation, I mean: the polynomial must be fully written with
>coeffiencts in base 10, exponents in base 10, and subscripts on variables
>in base 10.
>
>Leo told me once that he looked into this in connection with his looking at
>Jones' work, and saw that the coding is one level too high to get a result
>like this.
>
It's certainly out of the question using currently available techniques to
get such a result. To begin with one would have to code an explicit form of
the provability in ZF predicate.

And of course even if one could, noone would really want to look at such a
monster. :-)


>a. A sentence B in discrete mathematics which is independent of ZFC, or
>even necessary uses large cardinals to prove;
>b. B must be considered natural to a relevant mathematical community -
>where this naturalness is evidenced by
>
>	b1. a well attended one hour talk can be given on it to this
>community, and nearly everybody stays till the end
>	b2. the talk is generally considered interesting and successful;
>	b3. subsidiary questions that may or may not be independent, but
>are closely related, are actually taken up by that community in an effort
>to prove them in normal mathematics;
>	b4. there is a real area of problems that are considered
>intriguing, and arguably connected with ongoing concerns.
>

What we'd all find particularly wonderful would be to find an *interesting*
\Pi_1 sentence independent of ZF or even of PA. Consider the Riemann
Hypothesis. I believe it would be very easy to write an explicit Diophantine
equation for it readily meeting Harvey's bounds. But who would care. But a
proof that RH is independent of PA ... ... !

Martin Davis