Foundations of mathematics

This is a long story which I would not attempt to tell even if I were qualified at a level beyond undergraduate. ZFC set theory (“Zermelo—Fraenkel plus axiom of choice”) and its relatives are the default foundations for mathematics used by working mathematicians, and they are certainly better than no foundations. They have many irritating features, however, such as tying up armies of mathematicians in disputes about the Axiom of Choice, and leaving people such as me who do measure theory spending far too much time on the pathologies of set theory in infinite limits because of said axiom.

If one is dissatisfied with this state of affairs, one can do several different things: One can come up with variations on the theme of axiom of choice, which is a great way of starting especially smug arguments from partisans of each side, or one can throw the whole set theoretic basis out and try something different, such as category-theory-esque Type theory which… possibly avoids this mess? Or something else?

The latter sounds much more satisfying to someone of my temper. Although nothing I’ve mentioned so far sounds gripping enough for me to actually, you know, do.

Unmeasurable sets don’t plague me every day, and the foundations work if you sweep the Cantor dust under the carpet. It’s still unsatisfying though, so just in case I’ll record some stuff here…

Vladimir Voevodsky and et al have Homotopy Type Theory (HoTT to its friends):

Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy theory and type theory. It touches on topics as seemingly distant as the homotopy groups of spheres, the algorithms for type checking, and the definition of weak ∞-groupoids. Homotopy type theory offers a new “univalent” foundation of mathematics, in which a central role is played by Voevodsky’s univalence axiom and higher inductive types. The present book is intended as a first systematic exposition of the basics of univalent foundations, and a collection of examples of this new style of reasoning — but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant. We believe that univalent foundations will eventually become a viable alternative to set theory as the “implicit foundation” for the unformalized mathematics done by most mathematicians.

David McAllester’s Morphoid Type Theory. Relation?