Is there any theorem that can only be proven using the axiom of choice and that is actually used in real-world applications?

Question

I don't have a strong background in mathematics but I am interested in it from a philosophical perspective and I was wondering: is there any theorem or mathematical tool that is used in real-world applications and that can only be proven or justified by assuming the axiom of choice to be true?

Answer 1

That depends on what you mean.

Everything we do is finite. Given approximations with $100$ or $1{,}000$, or $10^{10^{10^{10}}}$ digits, you're not going to notice any difference between real analysis and discrete analysis.

But working with infinite objects can give us a smooth understanding of how "better approximations give better results", and then we can decide what is good enough.

And this applies not only for things like engineering or programming, but also to quantum mechanics. If you want to apply things to the real world, you need to contend with the fact that we have finite lives, with finite machines, finite understanding, and finite capacity. So once you're applying it, you need to forget "almost all the information", and the key point is that we can do this without a problem because we know that this information is very very very small and insignificant.

Okay. Big words. What now? Well. Now you have to decide. You can adopt an ultrafinitistic approach, reject the existence of $2^{100^{2^{100}}}!$, and never ever in your life use the axiom of choice for anything. And you won't feel any different. Or, you can use infinite objects to approximate and give you a better understanding of finite approximations.

So let's assume you chose the latter, took the red pill, and you're diving into the rabbit hole of infinite objects. Great. Now we're going to use the axiom of choice, right?

Well, again, not really. If all you care is approximating things in real life, then all you care about is things which are continuous over separable objects. The real numbers, finite dimensional vector spaces, maybe $\ell_2$. And even then, you really just care about behaviour on a countable dense subset. That's fine, but that means that for the most part, you'll never truly need the axiom of choice. Let me list some examples.

1. $f\colon\Bbb{A\to R}$ is continuous at a point $a$, where $A\subseteq\Bbb R^n$ for some $n\geq 1$. Well, to define this properly, we need to choose a definition: $\varepsilon$-$\delta$, or using sequences? Turns out that in general this would necessitate a fragment of the axiom of choice. But if we $A=\Bbb R^n$ and $f$ to be continuous everywhere? Not anymore.

2. The Hahn–Banach theorem, famously implying the Banach–Tarski paradox, and thus the existence of non-measurable sets. But if your vector space is separable, then again, you don't need the axiom of choice at all to prove it.

3. The Baire Category theorem. Very important theorem, very useful theorem, and it lets us understand, for example, what does it mean to say that "most continuous functions are not differentiable at any point". Also famously, its general statement is equivalent to Dependent Choice, which is a strong version of countable choice. But, again, if your space is separable, you don't need any choice to prove it.

And this list continues on and on. Okay, so let's hit a wall.

4. Lebesgue measure, which is the formal basis for probability, as well as integration (well, if we discount Riemann, that is). Surely that's not going to work without the axiom of choice. And that's true, if the real numbers are a countable union of countable sets, which they consistently are without choice, then you cannot develop measure theory, because we want singletons to be null, and the measure to be countably additive.

   ...except that we can still work with Borel codes, and for the most part, we'll be just fine.

Okay, okay. So I made the point. The axiom of choice is entirely unnecessary. We can just ignore it altogether for real life purposes. Yay.

But hold on, would it be nice if actually using all the aforementioned machinery was actually simple? And since we're already using "make believe infinite objects" to approximate real world stuff, why not make it easier, especially if the outcome is the same?

And so, yes, we use the axiom of choice all the time. It's unnecessary, it's adds a philosophical layer which some people will call into question, but it is just makes our tools simpler to work with. For this reason I posit that research into the axiom of choice is philosophically and technically important (and of course I'd say that, I'm working on this sort of research myself). It lets us understand where our theorems no longer apply without additional assumptions (e.g., separability) and how much we are losing explicitness of the objects we care about when we appeal to the axiom in our proofs.