The axiom of choices is about picking elements of infinitely many sets at once.
In the example we are talking about a single set. The deduction "the set is non-empty => we can pick an element" is much more basic than AC.
In the example we are talking about a single set. The deduction "the set is non-empty => we can pick an element" is much more basic than AC.
The actual HARD PART about the axiom of choice is that the thing f that picks from the collection of sets to its elements that has to exist must be a function. The axiom of choice does not have any reference to f being "described using any finite collection of symbols", or "computable". f must not be computable or graspable or describable, these are not constraints put onto f by the Axiom of Choice. But it must be a function!
Why is "being a function" a constraint for f at all? Not everything that goes from set A to set B is a function. Functions have to be able to be described in terms of sets, and not every collection of items is a set. The notion that every collection is a set is called naive set theory, and it does not work (see Russel's paradox). This is the hard part about the axiom of choice.
So if someone invokes some argument over complex concepts about computability, or being stateable, that's not even true of stuff outside of the Axiom of Choice and definitely not why specifically the AoC is hard.
I've edited this a lot, but it might still depend on the AoC if you can construct such a function in general, my ideas didn't work (e.g. two complex infinite sets per set are already hard)
> Is it trivial to construct a function that picks a single element from an arbitrary set that’s not ordered numbers (say, the real endomorphisms)?
With no constraints on the function this is the AoC.
On the other hand, it's always refreshing to see someone pushing us to think in this constructs.
Logic is hard!