> and the model math is using is evidently not very good.
There isn't really one "model of math". Plenty of people study alternative foundations of math or various axioms you can attach to ZF, etc. and its great that they do - choice, and lots of other set theoretic/foundational stuff, is very weird. But the reason mathematicians have largely settled on ZFC as a default is that it (and maybe nowadays + an inaccessible cardinal) also reduces some pathology and makes math more convenient.
Let's list some things which are related to the axiom of choice:
* The cartesian product of nonempty sets is nonempty (equivalent)
* The reals can be partitioned into more parts than there are real numbers (consistent with the negation of choice)
* All vector spaces have a basis (equivalent)
* All commutative rings have a maximal ideal (equivalent)
* All fields are contained in an algebraic closure (implied by choice)
The first two, at least to me, are similar to Banach-Tarski in that they are things I would like to be true and false, respectively, and are not if we do not accept choice. The point here is that the weirdness of Banach-Tarski is as much related to the axiom of choice as it is to generally the fact that (uncountable) infinities are just very weird, and while introducing choice does introduce pathologies like Banach-Tarski, it also reduces some.
The last three illustrate a more practical perspective. Suppose a universal decree, that math is no longer allowed to be done in ZFC, you could only use ZF, was imposed on mathematicians. This doesn't really change anything - all that mathematicians will do is, if they were perfectly fine with choice before, simply replace instances of "vector space" with "vector space with a basis", or "commutative ring" with "commutative ring with a maximal ideal", because the types of mathematical objects they care about are the ones with these desirable properties - they only use the axiom of choice because it ensures the general objects they work with also have those desirable properties. And mathematicians (often even the same ones as before, just wearing a different hat) who _do_ care about choice will continue studying those weird instances of the general object just as before.
As a final point for the convenience of axiom of choice, there are lots of instances where a proof will use choice purely as a matter of convenience. Maybe with some technical set theory or a smarter argument its possible to completely eliminate the requirement of choice, or use a weaker, less-objectionable version of choice. Other times, while a general vector space having a basis requires choice, the vector spaces in your particular application have a basis regardless of your thoughts on the axiom of choice. But of course its much easier to simply assert "vector spaces have a basis" and introduce a (faux) dependence on the axiom of choice. For a concrete example of this last point, see https://mathoverflow.net/a/35772. While about inaccessible cardinals/"universes" rather than the axiom of choice, the principle I want to illustrate is the same. The proof of Fermat's last theorem, if you trace citations back, eventually depends on "universes". But the actual invocations of those theorems are applied to objects where that generality is not required.
(Why not simply only have done the non-general scenario? Because "holds in general with additional axiom, holds in specificity without" is more knowledge than just "holds in specificity")
> The last three illustrate a more practical perspective. Suppose a universal decree, that math is no longer allowed to be done in ZFC, you could only use ZF, was imposed on mathematicians. This doesn't really change anything - all that mathematicians will do is, if they were perfectly fine with choice before, simply replace instances of "vector space" with "vector space with a basis", or "commutative ring" with "commutative ring with a maximal ideal", because the types of mathematical objects they care about are the ones with these desirable properties
Lol, I would love that. That's the book I want to read. I am weird, maybe, but I find the full-generality of mathematics to be exhausting when I just want to understand how numbers and geometry work. I will never care about the details of infinite sets.
I am reminded by a quote from Jaynes' probability text: that in their opinion, infinite objects are only meaningful when explicitly provided via a limiting process from finite objects. It is not, as far as I can tell, a widespread stance, but it's the one I subscribe to.
(Thanks for the lengthy reply, though. Just, it reminds me of the stuff I already find exhausting.)
There isn't really one "model of math". Plenty of people study alternative foundations of math or various axioms you can attach to ZF, etc. and its great that they do - choice, and lots of other set theoretic/foundational stuff, is very weird. But the reason mathematicians have largely settled on ZFC as a default is that it (and maybe nowadays + an inaccessible cardinal) also reduces some pathology and makes math more convenient.
Let's list some things which are related to the axiom of choice: * The cartesian product of nonempty sets is nonempty (equivalent) * The reals can be partitioned into more parts than there are real numbers (consistent with the negation of choice) * All vector spaces have a basis (equivalent) * All commutative rings have a maximal ideal (equivalent) * All fields are contained in an algebraic closure (implied by choice)
The first two, at least to me, are similar to Banach-Tarski in that they are things I would like to be true and false, respectively, and are not if we do not accept choice. The point here is that the weirdness of Banach-Tarski is as much related to the axiom of choice as it is to generally the fact that (uncountable) infinities are just very weird, and while introducing choice does introduce pathologies like Banach-Tarski, it also reduces some.
The last three illustrate a more practical perspective. Suppose a universal decree, that math is no longer allowed to be done in ZFC, you could only use ZF, was imposed on mathematicians. This doesn't really change anything - all that mathematicians will do is, if they were perfectly fine with choice before, simply replace instances of "vector space" with "vector space with a basis", or "commutative ring" with "commutative ring with a maximal ideal", because the types of mathematical objects they care about are the ones with these desirable properties - they only use the axiom of choice because it ensures the general objects they work with also have those desirable properties. And mathematicians (often even the same ones as before, just wearing a different hat) who _do_ care about choice will continue studying those weird instances of the general object just as before.
As a final point for the convenience of axiom of choice, there are lots of instances where a proof will use choice purely as a matter of convenience. Maybe with some technical set theory or a smarter argument its possible to completely eliminate the requirement of choice, or use a weaker, less-objectionable version of choice. Other times, while a general vector space having a basis requires choice, the vector spaces in your particular application have a basis regardless of your thoughts on the axiom of choice. But of course its much easier to simply assert "vector spaces have a basis" and introduce a (faux) dependence on the axiom of choice. For a concrete example of this last point, see https://mathoverflow.net/a/35772. While about inaccessible cardinals/"universes" rather than the axiom of choice, the principle I want to illustrate is the same. The proof of Fermat's last theorem, if you trace citations back, eventually depends on "universes". But the actual invocations of those theorems are applied to objects where that generality is not required.
(Why not simply only have done the non-general scenario? Because "holds in general with additional axiom, holds in specificity without" is more knowledge than just "holds in specificity")