Moved to https://matteocapucci.eu/mathematicians-dont-care-about-foundations/
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.
General abstract nonsense. 
Very nice! When I express similar sentiments to colleagues in mathematical logic, they unfortunately think I’m attacking their chosen mathematical discipline, say set theory. Set theory is a beautiful area of math but it is not the “foundation” of math. Rather, the foundations of mathematics are phenomenological in the sense of Husserl.
LikeLike
“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 notions of non-constructive and non-structural are rather independent of each other. Most mathematicians will likely continue to work with AC and LEM even if they switch to a structural set theory like ETCS or a dependent type theory like the one in Lean. On the other hand, constructivists are and have in the past been very comfortable using non-structural set theories like IZF or CZF.
“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.”
Personally, I’ve come to the conclusion that if naive dependent type theory is to succeed at replacing naive set theory as the default syntax that mathematicians use, dependent type theorists would have to present their theories with universes satisfying LEM and (the set-theoretic) AC, so that the subject could be made more accessible to classical mathematicians. Compared to the general population of mathematicians, constructive mathematicians are a small minority, and predicative constructive mathematics even smaller of a minority; the population of classical mathematicians dwarf them both.
In practice, the dominant approaches to dependent type theory, MLTT and cubical type theory, are primarily constructive and predicative in nature, which means that not only is there a material-structural gap in understanding, there is also a gap on what statements are provable in the foundations. It is hard enough to get a mathematician who is used to membership being a proposition which could be negated and sets being elements of other sets to adjust to the notion that sets and elements are completely different things and membership is a typing judgment with no truth value. One doesn’t need the additional hardship of telling classical mathematicians that they have to give up on LEM and AC, that in the foundations the intermediate value theorem cannot be proven, the fundamental theorem of algebra cannot be proven, that all real numbers have an infinite decimal expansion cannot be proven, and that all vector spaces are free cannot be proven, all facts that a classical mathematician would take to simply be true.
LikeLike
Re the first thing, yes I’m aware they’re distinct that’s why I said both things in that sentence 🙂
Re the second, I fully agree!
LikeLike
“One doesn’t need the additional hardship of telling classical mathematicians that they have to give up on LEM and AC, that in the foundations the intermediate value theorem cannot be proven, the fundamental theorem of algebra cannot be proven, that all real numbers have an infinite decimal expansion cannot be proven, and that all vector spaces are free cannot be proven, all facts that a classical mathematician would take to simply be true.”
On second thought, while constructive mathematicians cannot prove that these statements are true in constructive mathematicians, they still can prove that “LEM implies the intermediate value theorem”, “LEM implies the fundamental theorem of algebra”, et cetera, in the sense that one could construct a function with domain a type representing LEM for a universe and codomain a type representing the IVT or the FTA, et cetera.
LikeLike
Mathematicians can do mathematics without a knowledge of foundations because the human brain and organism are highly organized, but in a different manner than a formal conceptual system. That human thinking and understanding is, on the whole, not a matter of logically manipulating formalized ideas is generally accepted in philosophy today, as in the later Wittgenstein.
LikeLike