My understanding is that yes, axiom of choice (or more generally non-constructive methods) is convenient and it “works”, and if you naively take definitions and concepts from those realm and see what results / properties hold when removing the axiom of choice (or only use constructive methods), many of the important results / properties no longer hold (as you mentioned: Tychonoff, existence of basis, … ).
But it is often the case that you can redevelop these concepts in a choice-free / constructive context in such a way that it captures the spirit of what those definitions and concepts originally intended to capture, and yes it is harder this way, but 1) doing so often lets one recover the “morally correct” equivalent of those results / properties that do in fact hold in this context, and more importantly, 2) doing so has a lot of conceptual value.
For example, equivalent definitions become non-equivalent (such as finiteness; trying to do computable analysis and make sense of the intermediate value theorem in this context leads to new ideas like locale theory, abstract stone duality, overtness (dual of compactness, which is trivial classically), etc) where each has different and new interpretation, and the role of computability and approximation is made explicit which requires bringing in new / additional mathematical structures, etc. Also, many classical theorems have their choice-free / constructive equivalent, eg Tychonoff’s theorem for locales (arbitrary coproduct of compact frames is compact—no axiom of choice required to prove!) - and all of this gives us new and sometimes deep insight about the concept that would have been overlooked in the classical realm[1].
To put it differently: Choice turns structure into property. Without choice, we can instead treat those structure as additional data. This lets various theorems re-emerge, often in many non-equivalent forms—and this is good.
I have only heard of these examples (I am not at all familiar with them) in the context of constructive / computable analysis, but I expect this to be a lesson that holds broadly throughout mathematics (and more narrowly: that it is possible to come up with a “morally correct” choice-free equivalent of the theory that in its current form crucially depends on choice, and that this gives new conceptual insights), and this not having been done already for some subject X is more of an issue of lack-of-mathematician-years put into it.
Oh yeah, I totally agree that it is interesting to investigate what happens in non-choice worlds as an exercise in mathematical foundations, which sounds kind of like what you’re saying? But correct me if I’m misinterpreting.
I know someone doing a PhD in this, and I think it’s pretty cool stuff.
I think you misinterpreted me—my claim is that working without choice often reveals genuine hidden mathematical structures that AC collapses into one. This isn’t just an exercise in foundations, in the same way that relaxing the parallel postulate to study the resulting inequivalent geometries (which were equivalent, or rather, not allowed under the postulate) isn’t just an “exercise in foundations.”
Insofar as [the activity of capturing natural concepts of reality into formal structures, and investigating their properties] is a core part of mathematics, the choice of working choice-free is just business as usual.
Oh, yeah sure. I mean I think as a matter of pragmatics it mostly is an exercise in foundations these days. But I agree that splitting up concepts of finitude—for example—is a super interesting investigation. Just, like, the majority of algebraic geometers, functional analysts, algebraic topologists, analytic number theorists, algebraic number theorists, galois theorists, representation theorists, differential geometers, etc etc etc, would not be all that interested in such an investigation these days.
Agree with the last sentence. I think in a majority of the fields, lines of investigation with higher insight-per-effort, in the current margin, are those done with choice (or with even more controversial things like the large cardinal axioms).
Edit: this comment by Terence Tao also expresses a similar perspective:
In general, it seems that infinitary methods are good for “long-range” mathematics, as by ignoring all quantitative issues one can move more rapidly to uncover qualitatively new kinds of results, whereas finitary methods are good for “short-range” mathematics, in which existing “soft” results are refined and understood much better via the process of making them increasingly sharp, precise, and quantitative. I feel therefore that these two methods are complementary, and are both important to deepening our understanding of mathematics as a whole.
My understanding is that yes, axiom of choice (or more generally non-constructive methods) is convenient and it “works”, and if you naively take definitions and concepts from those realm and see what results / properties hold when removing the axiom of choice (or only use constructive methods), many of the important results / properties no longer hold (as you mentioned: Tychonoff, existence of basis, … ).
But it is often the case that you can redevelop these concepts in a choice-free / constructive context in such a way that it captures the spirit of what those definitions and concepts originally intended to capture, and yes it is harder this way, but 1) doing so often lets one recover the “morally correct” equivalent of those results / properties that do in fact hold in this context, and more importantly, 2) doing so has a lot of conceptual value.
For example, equivalent definitions become non-equivalent (such as finiteness; trying to do computable analysis and make sense of the intermediate value theorem in this context leads to new ideas like locale theory, abstract stone duality, overtness (dual of compactness, which is trivial classically), etc) where each has different and new interpretation, and the role of computability and approximation is made explicit which requires bringing in new / additional mathematical structures, etc. Also, many classical theorems have their choice-free / constructive equivalent, eg Tychonoff’s theorem for locales (arbitrary coproduct of compact frames is compact—no axiom of choice required to prove!) - and all of this gives us new and sometimes deep insight about the concept that would have been overlooked in the classical realm[1].
To put it differently: Choice turns structure into property. Without choice, we can instead treat those structure as additional data. This lets various theorems re-emerge, often in many non-equivalent forms—and this is good.
See also: Five Stages of accepting Constructive Mathematics, Expanding the domain of discourse reveals structure already there but hidden.
I have only heard of these examples (I am not at all familiar with them) in the context of constructive / computable analysis, but I expect this to be a lesson that holds broadly throughout mathematics (and more narrowly: that it is possible to come up with a “morally correct” choice-free equivalent of the theory that in its current form crucially depends on choice, and that this gives new conceptual insights), and this not having been done already for some subject X is more of an issue of lack-of-mathematician-years put into it.
Oh yeah, I totally agree that it is interesting to investigate what happens in non-choice worlds as an exercise in mathematical foundations, which sounds kind of like what you’re saying? But correct me if I’m misinterpreting.
I know someone doing a PhD in this, and I think it’s pretty cool stuff.
I think you misinterpreted me—my claim is that working without choice often reveals genuine hidden mathematical structures that AC collapses into one. This isn’t just an exercise in foundations, in the same way that relaxing the parallel postulate to study the resulting inequivalent geometries (which were equivalent, or rather, not allowed under the postulate) isn’t just an “exercise in foundations.”
Insofar as [the activity of capturing natural concepts of reality into formal structures, and investigating their properties] is a core part of mathematics, the choice of working choice-free is just business as usual.
Oh, yeah sure. I mean I think as a matter of pragmatics it mostly is an exercise in foundations these days. But I agree that splitting up concepts of finitude—for example—is a super interesting investigation. Just, like, the majority of algebraic geometers, functional analysts, algebraic topologists, analytic number theorists, algebraic number theorists, galois theorists, representation theorists, differential geometers, etc etc etc, would not be all that interested in such an investigation these days.
Agree with the last sentence. I think in a majority of the fields, lines of investigation with higher insight-per-effort, in the current margin, are those done with choice (or with even more controversial things like the large cardinal axioms).
Edit: this comment by Terence Tao also expresses a similar perspective:
Ah I really need to write a megasequence about the large cardinal axioms! They’re awesome (I wrote a thesis on them).
Consider my vote to be placed on writing that megasequence, I know next to nothing about large cardinals and would be eager to know more about them!