Unsurprisingly, I'm biased in the direction of the Computer Science flavor of mathematics, which leads me to say: Of course the Axiom of Choice is useful. Why wouldn't an axiom that allows you to wave your hand and produce infinite amounts of information that you have no mechanism to produce any of be useful? Of course it's useful to invoke infinite amounts of information from thin air. Indeed, uncountably infinite amounts of information, or any aleph-X you please amounts of information.

I agree and understand that it's not a matter of "right" or "wrong", but I do find myself looking a bit askance at "proofs" of statements in which a mathematician writes the equivalent of a few kilobytes of proof statements (in a suitable encoding), which has to be paired with an infinite number of unknowable bits, which the mathematician is not only incapable of providing in practice but often incapable of providing even in theory, to be "true". Mathematicians often claim to find the axiom aesthetic; I find it to be quite the contrary. When you look at proofs from an information-theoretic point of view, the Axiom of Choice is literally an infinitely-sized wart on the side of any proof that uses it.

This isn't necessarily true; you can also limit which sets are valid sets in a way that guarantees that choosing an element from these sets is well defined. For example, the Axiom of Constructibility basically limits which sets exist, in a way that allows you to always use the Axiom of Choice because your sets have a specific fine grained structure you can use to well-order them.

For example, if I were to require "all sets are finite", then the Axiom of Choice is trivial. The Axiom of Constructibility still allows infinite sets (and even uncountable sets), but it's still limited enough that the Axiom of Choice holds.

You can almost think of it as requiring all sets to have source code, and then just alphabetizing the source code in order to pick a set.

Yes, it's true that you can use the Axiom of Choice in ways that don't invoke infinite information, and yes, those would be OK with me from an aesthetic point of view. (Again let me emphasize my complaint here is not that it is "invalid" but that I find it very unaesthetic, contra many conventional mathematicians.) But things like the Banach-Tarski paradox definitely require infinite amounts of information (uncountable infinite in this case, I believe) with, as far as I know, no mechanism for producing it. As far as I know, it's just an existence proof.

When discussing hypothetical FTL technologies, I often like to say that it's no great surprise that if you allow one impossibility (negative mass) it's no surprise that you get another (FTL). Similarly, if you allow an uncountably infinite amount of information to be magicked into your proof, it's no surprising that you may get a confusing result like the Banach-Tarski paradox. From my perspective, the confusing step isn't when you have two spheres where you used to have one, the confusing step is when you made uncountably-infinitely-precise cuts with no ability to produce the cuts in question. I'm not confused by the end result, I'm confused at that step. So to speak. I'm not literally confused, obviously, only my sense of aesthetics is.

My take on this is that the axiom of choice allows you to produce infinite amounts of information, if and only if you start with infinite amounts of input.

Think about how much information is involved in presenting an infinite collection of sets! When I say even something as simple as "Let x be a real number" I'm already invoking infinitely many bits of information. Things have already gotten weird, you just haven't noticed because we've hidden it.

The axiom of choice is saying something like, okay, we somehow have this infinite pile of information sitting around; now we're allowed to interact with it. And if you don't like that, your problem might be with the infinite amount of information we started with. (Or it might not; yes-choice and no-choice are both totally valid positions.)

But in practice it doesn't matter that much because you never actually do start with infinite amounts of information, and so you don't need an infinite-amounts-of-information processor. But if we have finite amounts of information that we're pretending are infinite to simplify things, we can also process the finite amounts of information and pretend we're processing infinite information.

Confused about this. Isn't the comp-sci perspective to use the effective topos and computable partial functions? In that case, LEM fails and so must AOC; instead, we have Markov's Principle.

I mean a computer science perspective on the Axiom of Choice itself.

While I am naturally much more sympathetic to intuitionistic/constructible mathematics than the general math community is, I won't go so far as to insist it is the only one true math, since I don't think there is such a thing. I just think that from an information theoretic perspective, calling the instantiation of infinite unknowable amounts of information into a proof "aesthetic" is, well, not a term I'd use. I find Axiom of Choice generally gross.

Is the existence of basis in every vector space really useful? I think in analysis, people mostly work with Schauder basis rather than Hamel basis. I am not aware of any important result that uses the existence of Hamel basis in an infinite-dimensional vector space. This is not a criticism about your comment, but an honest question.

I am not a fan of the axiom of choice, and open-minded about truth values beyond true and false. So I'm really curious about the progress of constructive mathematics, regarding proving known results with non-ZNF axioms, and maybe establishing some more "intuitively satisfying" (whatever that may mean) results where ZNF gives subjectively bogus results like Banach-Tarski?

A lot of people blame Banach-Tarski on the axiom of choice. I disagree. I think it's in essence just a variant of the Hilbert hotel, with the axiom of choice merely serving as part of the machinery for this manifestation. In other words, it's just a counterintuitive but true consequence of the nature of infinity. As such, I think any mathematical system that acknowledges infinity, is going to have such counterintuitive results.

Why does AoC implying LEM mean you can't use LEM in constructive maths?

EDIT: misread

Constructive mathematics by it's nature does not use LEM. The idea is that proof of existance must be done by construction of the object in question. LEM implies DNE, which means existance can be shown by showing non-existance is not the case.

EDIT: Apologies, misunderstood.

I said that if you don't want to use LEM in constructive maths you must also give up AOC, since AOC -> LEM.

Oh right. Also hi siraben didn't notice it was you.

Hello! Nice to see another IRCer :)