As others have noted, this has little to do with the Axiom of Choice per se. The Axiom of Choice is not needed to prove that one can make a choice from a single

As others have noted, this has little to do with the Axiom of Choice per se. The Axiom of Choice is not needed to prove that one can make a choice from a single inhabited set, where this boils down to the tautology "If a set has at least one element, then it has at least one element". The Axiom of Choice is only needed for making infinitely many choices at once. (There IS a sense in which what is going on here is the distinction between what category theorists call "internal" and "external" Choice, but I'll not get into that for now since I think the following is more important to point out first.) The result/paradox here has more to do with Tarski's indefinability theorem, under which no suitable formal language is able to define the concept of definability in that same language. See also https://mathoverflow.net/a/44129/3902 https://mathoverflow.net/a/44129/3902 for more discussion on what goes wrong in attempting to formally prove that "undefinable" numbers exist by this common but naive argument from uncountability. The gist of the above MathOverflow link and of Tarski's indefinability theorem is that we must keep in mind that Cantor's famed diagonal argument for uncountability is a constructive argument. Given any function from N to 2^N, it defines an explicit element of 2^N not in the range of that function. So there would be something paradoxical in concluding that this explicitly defined value is not definable.