But the entire point of the axiom of choice is to say "that's fine; you're still allowed to use 'unconstructed' choice functions in your proofs".
Would the OP reject the statement "let x be an element of the set of numbers that cannot be defined with finitely many symbols"; such a statement does not depend on the AoC, but I think the OP complains about making even a single choice.
This is where the axiom of choice is interesting; many people feel that it seems intuitively reasonable, but the implications are counterintuitive (e.g. banach-tarski)
You can assume there exists a number between 3 and 4 though, no problems there.
As for the integer example, the integers are all easily (finitely) constructed (successors to 0 and their additive opposites), so it isn't a consistent concept to say "This is an unconstructable integer." Sets, on the other hand, are not necessarily always constructable, unless you only take the constructivist axioms.
It's different because there's nothing that says such a choice function _cannot_ exist (short of an axiom that says explicitly so).
No, the argument is that if you cannot describe the choice then you have a problem. My argument does not assume anything about the choice function, it's merely an informal observation about its output.
If so, your problem is not with the axiom of choice.
Edit: "Not being able to describe the choice a choice function makes" and "not being able to construct it" are really the same thing.
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.
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 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.