[FOM] Alternative foundations?

[Staffan Angere]

The realization that "sets with relations on them" is not sufficient as a theory of mathematical structure goes back at least to Bourbaki; topologies are some pertinent examples, and Bourbabki's theory of structures is much more general. However, my guess is that Professor Frenkel is referring to category-theoretic or type-theoretic foundations. Among these, the Univalent Foundations / Homotopy Type Theory program seems to be the most actively developed at the moment:

http://homotopytypetheory.org

Category theory itself furnishes several examples of objects that have no existence in set theory, such as the category of all sets. However, the main point of HTT as opposed to set theory, as I understand it, is not that set theory does not postulate enough sets, but that HTT allows one to formalize many parts of mathematics in a much less arbitrary manner than in set theory. Frenkel's remark that "mathematical structures constitute but a small island of modern mathematics" should perhaps be taken not to say that these parts would necessarily be unformalizable in set theory, but rather that such a formalization may not be the most useful or enlightening one.

Staffan Angere
University of Lund