Is the axiom of choice necessary here?

You use the axiom of choice while constructing the sequence $(x_n \mid n \in \mathbb N)$. To make this more apparent, we need to be a bit more formal in how you obtain such a sequence:

Consider the set $S$ of all finite sequences $\vec{y} = (y_n \mid n \le m)$ such that $y_0 = x_0$ as fixed above and such that for all $n < m$ $y_{n+1} \in X \setminus \{ y_0, \ldots, y_n \}$. Now consider the relation $R$ on $S \times S$ given by $$ (y_0, \ldots, y_m) R (z_0, \ldots, z_l) : \iff l > m \wedge \forall n \le m \colon y_n = z_n, $$

in simpler words: $\vec{y}R\vec{z}$ iff $\vec{z}$ is an end-extension of $\vec{y}$.

Your induction proves that for all $\vec{y} \in S$ there is some $\vec{z} \in S$ such that $\vec{y} R \vec{z}$. The axiom of choice (it suffices to have the axiom of dependent choice) now allows you to pick an infinite sequence $( \vec{y}_n \mid n \in \mathbb N)$ such that for all $n \in \mathbb N$ $$ \vec{y}_n R \vec{y}_{n+1}. $$

If you now let $x_n$ be the $n$-th element of $\vec{y}_n$, the resulting sequence $(x_n \mid n \in \mathbb N)$ is as desired.


Note that this doesn't prove that some form of choice is necessary. It only highlights where you implicitly use the axiom of (dependent) choice. To see that, in general, we need some form of choice here is much harder and (for the moment) you really shouldn't worry about that.


the definition of the sequence is by induction

Well, no, not really - you haven't shown how to define the sequence at all, since the choice of $x_n$ given $x_0, ..., x_{n-1}$ isn't unique. What you can prove by induction is that for each $n$, there is a sequence of $n$-many distinct elements of $X$, but this doesn't give you a way to get an infinite sequence of elements of $X$; this is exactly the sort of thing, in fact, that choice is needed for.


The other answers have correctly identified the issue. Let me highlight the difficulty: it is relatively consistent with the axioms of set theory except for the axiom of choice that there are infinite sets which do not contain a copy of the natural numbers (that is, there are infinite sets $X$ such that there is no injection $f\!:\mathbb N\to X$).

This means that the suggested strategy fails for these sets, but it is even worse, since it is not true that these sets have a proper subset of the same size. Perhaps this feels too abstract, so let's drive the point home:

Suppose $X$ is an infinite closed or open set of reals. We can explicitly find a countably infinite subset of $X$ in this case (without invoking the axiom of choice); this is a decent exercise you may want to attempt. The same is true if $X$ is slightly more complicated, for instance if $X$ is a countable union of closed sets or even a countable union of countable intersections of open sets (this is already challenging).

However, one cannot even prove without using the axiom of choice that if $X$ is a countable intersection of countable unions of closed sets of reals then $X$ has a proper subset of the same size. These are still fairly concrete sets, and already the axiom of choice is needed here.