[FOM] What are foundations for?

[Martin Davis]

>From my perspective, the argument posed as set theory vs category
theory is taking place in a pre-Goedel world when foundations were
supposed to be the single solid rock supporting the corpus of
mathematics.

In the post -Goedel world, that's a remote and forgotten Eden. As
Goedel himself pointed out already in his 1933 lecture, instead of a
single system we are confronted by a hierarchy of systems, and as we
rise in the hierarchy, more and more previously unproved propositions
become provable. These include Pi-0-1 propositions that each may be
interpreted as stating that some polynomial equation has no integer
roots. In this world what is important is systems that can be used to
calibrate the strength of propositions.

The proof of FLT famously not only used categorical methods, but
freely used Grothendiek universes. This immediately raised the
questions: is it provable in PA, in second-order arithmetic, or what?
Category theory is a wonderful tool, but what use is it here?

Goedel, in effect, conjectured in his Gibbs lecture that the Riemann
Hypothesis is not provable in PA.  Can category theory hope to resolve
this?

I believe (someone correct me if I've got this one wrong) Tony Martin
proved that Borel determinancy is provable from the Zermelo axioms but
not from n-th order arithmetic for any n. What use would categorical
methods be in making that kind of fine discrimination?

Martin