[myWindoonn]

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.