[openasocket]

I think you're misunderstanding the axiom of choice, focusing too much on the literal word "choice". Sure, that ABC order is arbitrary, but so are most mathematical constructions! How did I "select" that encoding? By defining it! By your definition of the axiom of choice, literally defining any set at all (besides the null set and the set of natural numbers, which are defined in their own axioms) would require invoking the axiom of choice.

You only need the axiom of choice if you need to pick an element out of a set WITHOUT SPECIFYING which one you are picking. And sometimes not even then. For instance, if you want to prove all elements in a set have a certain property, often you will see proofs take the form "pick an element of that set, assume it doesn't have this property, then by X, Y, and Z we have a contradiction, thus all elements have that property". That doesn't involve the axiom of choice at all, even though a straight reading of that statement makes it sounds like we are making a choice. In truth that proof is saying we can do this with every single element of that set, so you aren't really making a "choice". You only need the axiom of choice when you are, say, stating the existence of a function without defining what that function is. For an example of an actual invocation of the axiom of choice, check out the proof sketch in the wikipedia article on Zorn's Lemma: https://en.wikipedia.org/wiki/Zorn%27s_lemma .