[lheck]

True. It's always good to see someone thinking about math concepts in critical ways to understand them. But this post doesn't really have a place here on hacker news as it's just born of faulty premises and of misunderstanding what the Axiom of Choice states.

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.

[quchen]

Thanks for pointing out that the f must be a function part is particularly difficult. Is this only a problem for infinite sets (of sets to pick from)? 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)?

[lheck]

> Is this only a problem for infinite sets (of sets to pick from)?

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.