Does choosing a counting function require the Axiom of Choice?

Question

Say one is asked to prove something about set $X$, and part of the given conditions is that $X$ is countable. Your proof starts with

"Let $f: X \mapsto \Bbb{N}$ be a counting function for $X$ and ..."

and the proof proceed to use $f$ to demonstrate that which was to be proven.

Now if $X$ were finite, one could start with "Let $f: X \mapsto \{ 1, 2, \ldots |X|\}$," this requires just the axiom of finite choice and everybody is OK with that.

If I needed to deal with a collection of countable sets $X_i : i\in I$ where $I$ is infinite, then starting with "$\forall i \in I$ let $f_i: X_i \mapsto \Bbb{N} $ be a counting function for $X_i$ and ..." then I have relied on the Axiom of Choice.

Here, though, I need to choose just one counting function -- but in general (not knowing anything about $X$ other than that it is countable) choosing that counting function appears to require an infinite number of choices.

My question is, has such a proof assumed the Axiom of Choice, or not.

For some couintable sets, for example the rationals, it is possible to algorithmically specify a particular counting function, so for such sets this question does not arise. But perhaps there are countable sets for which one cannot specify algorithmically specify a particular counting function, in which case my question applies. If there are no such sets, that is itself an interesting theorem.

Answer 1

No, you do not need the axiom of choice there. The point is that $X$ is countable iff it has a counting function. You are only making one choice - you are choosing an element from $\{$counting functions on $X\}$, which you know (by hypothesis) to be non-empty.

Answer 2

No, you are wrong. If $X$ is finite, the fact that there is an enumeration of $X$ as $\{x_1,\ldots,x_n\}$ is not due to the axiom of choice for finite sets being a theorem. It is by the definition of finiteness.

Similarly, the definition of $X$ being a countable set, means there is an injection from $X$ into $\Bbb N$. Using existential instantiation we get an enumerating function $f\colon X\to\Bbb N$.