> So the statement "let x be an element of y" is already problematic?

Hm, good point. No, that's not the problem because that's just the same as saying "let x be an undefinable number". The problematic statement is (I think -- I need to think about this some more) "let f be a choice function on (infinite) sets of undefinable numbers". If x=f(S) that is not the same as "let x be an undefinable number" unless S is the set of ALL undefinable numbers, which it need not be.

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?).

> I can easily construct one; does that change anything?)

I don't think so. The way you have constructed the Sn's allows you to re-use a choice function for one set for all the other sets. But I don't think this is possible in general.

This is the thing that makes it hard. If you don't impose some sort of structure on the Sn's then I think you will have a very hard time constructing a choice function for them. That's the whole point. If you want a choice function for such sets in general you have to just assume that one exists without being able to actually exhibit one. Your assumption may be mathematically valid (because AoC is consistent with ZF), but I submit that a reasonable person might find it a little hinky.