As my retort to that common mentioned, he is wrong.

That is still random. You are arbitrarily picking an encoding, (English) in this case. Why not a Russian programming language or Chinese? How did you *select* your encoding out of the set of all encodings?

The act of assigning order to an unordered set is arbitrary. ABC order is a made up concept. It's not numerical, it's an arbitrary language and an arbitrary order that's a by product of human culture. Thus invoking this is at it's essence invoking the axiom of choice. You are arbitrarily selecting an algorithm.

Gödel worried about this, and one of the lemmas leading up to their First Incompleteness theorem is that the encoding doesn't matter, as long as it's a bijection on valid algorithms. (Numbers which code for invalid algorithms, perhaps due to syntax errors, can be ignored.) Gödel also was the one who showed that such encodings are possible and useful in the first place, so the problem of arbitrary encodings started and ended with him.

You can phrase things like Gödel did. For any encoding of algorithms into natural numbers which is bijective (ignoring invalid syntax), enumerate the algorithms as 0, 1, 2, 3, ... using the bijection, and then run them in parallel by taking steps [0, 0, 1, 0, 1, 2, 0, 1, 2, 3, ...] The user provides an encoding, without invoking the Axiom of Choice.

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 .