Categorical Foundations of Mathematics?
Timothy Y. Chow
tchow at math.princeton.edu
Tue May 24 15:50:10 EDT 2022
Harvey Friedman wrote:
> Furthermore, at least so far, category theory hasn't even been useful
> for ANY of our dramatic foundational revelations, of which we have a
> few. The really useful tool for uncovering the dramatic foundational
> revelations has always been through the usual standard classical set
> theoretic foundations.
While it might not count as "dramatic," the fact that a certain segment of
homotopy theory ("synthetic" homotopy theory), which at first glance seems
to require rather strong set-theoretic axioms to formalize (universes),
actually requires much less proof-theoretic strength (some kind of
Martin-Lof type theory or Kripke-Platek set theory) was discovered by
thinking hard about foundations from the point of view of higher category
theory and type theory.
The above point has been mentioned before on FOM, but perhaps was obscured
by confusing debates about "homotopy type theory as a foundation for all
of mathematics" and the relationship between "synthetic" homotopy theory
and conventional homotopy theory. But if we lay such debates aside and
just focus on the reverse mathematics, it seems to me to be a clear case
in which not only was the insight historically arrived at via
non-set-theoretical methods, but where conventional set-theoretic thinking
may have posed a psychological barrier to making the discovery. The
conventional thinker might object to referring to an argument as a
"computation of the homotopy group of a sphere" unless that statement is
interpreted in terms of conventional homotopy groups of conventional
spheres, and that might present an obstacle to analyzing the logical
structure of the argument on its own terms.
Tim
More information about the FOM
mailing list