Suppose that $X$ is a set and $f$ a map defined from $X$ onto $X$. Is the axiom of choice required to define
$$S = \{x_n : n \in \mathbb{Z}\}$$
where $x_0 \in X$ is given and $x_n = f^n(x_0)$?
If not what is a definition of $S$ in $ZF$?
The origin of my question is this question.
Defining $ S' = \{x_n \, : \, n\geq 0\} $ does not need any choice. However, your instincts are correct that defining the sequence for negative values of $ n $ uses a form of choice, as there is no specific element in the fiber $ f^{-1}[x_n] $ to select. However, you do not need the full axiom of choice. Indeed, you can use the axiom of dependent choice to define this set.