[FOM] Is there a "naturally occurring" theorem provable in EFA but not in predicative arithmetic?

[Harvey Friedman]

On 11/1/06 5:56 PM, "Rupert McCallum" <rupertmccallum at yahoo.com> wrote:

> My friend Norman Wildberger thinks there is a part of mathematical
> reasoning which is self-evident and doesn't need to be analyzed by the
> axiomatic method. I want to cast doubt on this belief of his by giving
> him an example of a "naturally occurring" theorem, of the kind
> mainstream mathematicians would be interested in, which can be proved
> in EFA but not in predicative arithmetic as developed in Edward
> Nelson's book "Predicative Arithmetic". Of course one example is
> "exponentiation is total", but that is not the sort of theorem which
> would be of interest to a mainstream mathematician.
> 

1. For all n, the Pell equation

x^2 = dy^2 + 1

where d > 0 and not a square, has at least n solutions. This can be proved
in EFA but not in, say, PFA = Idelta0. There is known exponential behavior
here, even for fixed d = 2.

2. Consider the statement

"every Pell equation has a solution".

If I recall properly, D'Aquino proved that EFA is equivalent to PFA + "every
Pell equation has a solution". In particular, it is provable in EFA but not
in PFA.

3. For all 0 < p < 1, there exists n such that the probability that a
positive integer < n is prime is less than p.

4. Burnside problems in group theory (3rd ursl below). Also van der
Waerden's theorem, although the known lower bounds are very low, even the
Gowers proof seriously uses exponentials (I think it works in EFA).

5. Falting's theorem should be looked at from this point of view.

6. People tend to believe that FLT can be proved in EFA but not in PFA. One
reason is that an appropriate statement in PFA is awkward.

7. Various Ramsey theory statements.

http://www.cs.nyu.edu/pipermail/fom/2006-April/010367.html
http://www.cs.nyu.edu/pipermail/fom/2006-April/010366.html
http://www.cs.nyu.edu/pipermail/fom/2006-April/010379.html

Harvey Friedman