Many people seem to believe mathematicians work in non-constructive, non-structural, battered foundations because they love their Platonic realm and have a kink for AC and LEM. The reality is most mathematicians don’t have a clue about foundations, they don’t care, and happily work informally for all their lives.
Case in point, mathematical foundations are a pretty recent thing (19th century if we are being generous) but their establishment didn’t deprecate previous mathematics, which continued to be studied and used just as well. Even during the so-called ‘crisis in foundations’ at the start of the 20th century most mathematicians didn’t blink an eye. Only a few pages of math had to be rewritten, and they were about foundations themselves.
I’m being intentionally provocative in calling out foundations here so, let me throw a bucket of water on this fire already. Foundations are not useless to study at all! On the contrary, mathematicians are thankful someone figured out foundations for them, so that they just need to know some TL;DR about which logical maneuvers they are allowed to perform and which objects they are allowed to claim the existence of.
Such ‘irrelevance’ witnesses a robustness in mathematics, betraying a deeper nature behind it’s facade of rigour. Mathematics is irreducibly informal (even foundations), i.e. relying on some unspoken mutual understanding on how to interpret signs, concepts, and norms. The difference among mathematicians is how deep they have to shell such conventions before being satisfied.
Thus math is not a castle built on a bedrock of unshakeable foundations. Math is rather a collective codification of intuitions squeezed into formal frames in the best way possible. This is why the ‘crisis in foundations’ didn’t really matter for most mathematics: what broke was the frame, not the ideas. This is also why we get new and improved mathematical theories every now and then. Saying ‘space’ today doesn’t evoke the same suggestions it used to do two-hundred years ago.
In fact formal definitions never fully capture the essence of the ideas they intend to embody, being mere vessels to reason and communicate deeper, intangible intuitions about them. This essence is shaped by the discourse among mathematicians, and the unrelenting murmuration of teaching and learning. This is the true mathematical platonic realm: the socially determined, impalpable world of shared intuitions and understandings, substantiating all the formal language.
Formality is relevant, don’t get me wrong. Mathematicians hold it in great respect, and agree to abide to its rule. I myself recognize the importance of choosing good formal language (meaning definitions and notational devices) to guide our thoughts. After all, boundaries shape creativity. But here I’m making the point that what ‘formal enough’ means is entirely a social construction, dependent on who, more than what, you are working with.
If this isn’t already liberating (or obvious) enough for you, here’s a silver-lining. The carelessness mathematicians have towards foundational matters has the interesting corollary that they don’t feel strongly about any of the options on the menu. In particular they are not committed to ZFC as much as some people like to complain.
Mathematicians point in the direction of ZFC when asked about foundations because this is what they’ve heard justifies set theory, and that’s what they care about. Naive set theory supplies the raw material they’ve learned to build mathematical concepts with, and ZFC provides quality assurance for it. But that’s it: the average mathematician barely knows how ZFC actually limits their set manipulations.
For people who, like me, are enamoured of structural foundations, and think more mathematicians should be aware of them, this is great news! Potentially, agnostics can be convinced to adopt more expressive foundations if we don’t insist this to be a matter of religious faith, but a more convenient justification for their mathematics.
In fact, I’m sure if at the start of an undergrad mathematical curriculum we provided students with a good ‘naive type theory’, mathematicians would just grow to use it. They’d still won’t care, but they’d happily credit Martin-Löf for giving legitimacy to their mathematics instead of Cantor, Zermelo and Fraenkel.
Published