You're right that there's a problem with 'Let f be a choice function on...', but that's the problem the axiom of choice solves. Sure, it's non-constructive; you don't know much about f, just that it exists and f(s) is in s (for all sets s that are subsets of S).

The question is specifically what weird undefinable numbers have to do with anything; why those are specifically a problem.

Let S be the set of all non-finitely defined real numbers.

Let (Sn) be the sequence of sets such that Sn = {s in S : n-1 < s < n}

Am I allowed to say "let s1 be an element of S1"? Or "s2 an element of S2"? (Note that we don't need the axiom of choice to get a choice function for this sequence; I can easily construct one; does that change anything?).