I think, for the first time, I ran organically into a situation where the Axiom of Choice helped me reason through a mathematical quandary. Shout-out to my math acquaintances to help check my reasoning.
So here's the question: can you choose a random real number? More formally: on what basis do we logically conclude that every real number is a viable candidate for random selection if you are selecting a random real number?
The reason this is even a question is that the definable reals are a subset of the real numbers; not every real number can even be named using a finite description. So the question arises: can you pick a number you can't even name?
And unless I've missed something, I think the Axiom of Choice says "yes." Real numbers can be described with an infinite sequence of digits (before and after the decimal), each digit is chosen from the finite set 0-9, we accept without chasing the evidentiary chain that you can randomly choose one element from a 10-element set, and the Axiom of Choice asserts you can therefore construct a real number's representation (an infinite set) by choosing a random element from every 0-9 option in both directions (two infinite sets).
This works, yeah?
@mark I don't understand what mathematical object you want to prove the existence of.
@robryk This train of thought grew out of the observation "If you pick a random real number, the probability it's rational is zero." Which made me wonder for the first time whether the idea of "pick a random real number" is a well-formed idea in the first place since not all real numbers are even nameable with a finite-string representation ("can you pick, in finite time, something you can't name in finite time?").
@mark it's well formed insofar we've built an abstraction (probability distributions) and declared that this is what picking a random number means.
I think you can make some statements about computability of functions that map between probability distributions, but I don't see how to get around defining some way of picking things axiomatically.
@mark ah; nothing around probability distributions talks about finite time. They're at the same abstraction level as (not necessarily comoutable) functions.
@robryk "choose" -> select with uniform distribution a number from the set of reals.