FOM: elimination of analytic methods in number theory

[Stephen G Simpson]

In answer to my posting of 25 Feb 1998 14:14:59, Joe Shipman asks:

 > Two questions for you, Steve: 1) What "big theorems" of number
 > theory have actually been proved without going beyond the methods
 > you reduce to PRA or PA?  Can Wiles's theorem be so proved?
 > Faltings's theorem?  Goldfeld's result on the zeroes of the Riemann
 > zeta function?  The result that every sufficiently large even
 > number is the sum of a prime and the product of two primes?

I once sat down and convinced myself that the analytic proofs of some
classical theorems of analytic number theory go through in WKL_0, and
hence the theorems have "elementary" proofs in PRA.  I'm pretty
confident about Dirichlet's theorem on distribution of primes, and the
prime number theorem.  Beyond that, I don't know.  I haven't gone
through the new stuff like Wiles' theorem, and I haven't gotten any
number theorists sufficiently interested to bother about it, either.

Faltings' theorem is intriguing, because it's a finiteness theorem,
and it's known that finiteness theorems sometimes go beyond PRA.  I'm
thinking of applications of WQO theory such as the Hilbert basis
theorem, Kruskal's theorem on finite trees, and the Robertson-Seymour
graph minor theorem.  But I haven't had the time or energy to examine
Faltings' theorem from this perspective.

 >  2) What kind of blowup is there in length of proof in your reductions?

I haven't studied this, but it's a good question.  I think Alexander
Ignjatovic told me he had some results on this.  I think the results
are something like: there is no blowup between WKL_0 and Sigma^0_1
induction, but there is blowup between Sigma^0_1 induction and PRA.
But don't trust me on this.  If anybody knows better, please chime in.

-- Steve