FOM: Elimination of analytic methods in number theory.

[Solomon Feferman]

In answer to a question of Joe Shipman, Martin Davis cited work of Takeuti
and myself which shows the formalizability of analytic number theory in
systems conservative over PA.  This is supported by development of the
requisite portions of analysis in the systems in question.  Moreover, 
case studies of specific results in analytic theory have been
demonstrated to be provable in PA (and perhaps weaker systems) by Patrick
Cegielski in his Univ. of Paris VII thesis, "Quleques contributions a 
l'etude des arithmetiques faibles" (1990).  I don't know if this work 
has been published subsequently.  At any rate, Steve Simpson
(25 Feb) went us one better by citing a system in which the requisite
analysis can be
done, conservative over PRA, Primitive Recursive Arithmetic.  (Whether
that is an embodiment of Hilbert's finitism, claimed by Tait and Simpson,
is a separate, perhaps controversial, issue.)  I would like to
bring attention to the work of Ulrich Kohlenbach, which pushes somewhat
further down the proof-theoretic and computational complexity of systems 
in which analytic number theory can be carried out, to be specific a
system G_2 A^omega at level 2 in the Grzegorczyck hierarchy; see his paper 
"Mathematically strong subsystems of analysis with low rate of
growth of provably recursive functionals", Arch. Math. Logic 36 (1996)
31-71.  At least the needed analysis can be done there in principle.  It
would be of interest to carry out case studies of specific theorems in
analytic number theory in this or related systems, e.g. of Littlewood's
theorem on the changes of sign of pi(x) - li(x).  

Sol Feferman