>>11175139It is whenever "the set S at hand is non-empty" formulated constructively, i.e. by demonstrating a value s0 is in S. Because then, the choice function can be taken to take any such non-emphy set and resign its value (the one that's used to demonstrate that it's non-empty).
However, if "is non-empty" is not witnessed but simply demonstrated non-constructively (by showing that not being able to take a value would be absurd by a means other than showing a particular value), then claiming that there's a choice function of each set is also non-constructive.
Example: I give you the set {4, 6, 11} and ask me to choose an element from it. You may say "I choose from it 6".
Now I give you a well ordered set of 70 elements. You may say "I choose from it 'the smallest' w.r.t. your ordering".
Now ai give you N, the set of natural numbers. You may say "I choose from it the number 36".
Okay, but now I say I give you a set of cardinality of the power set of of the powerset of N, but I won't tell you which set it is (i.e. I won't give you any information about what sort of elements I've packaged into in this large set) and I won't tell you the bijection that witnesses that it has said cardinality.
You are now in the situation that you know nothing about this set except how big it is. Due to your lack of knowledge, you can't choose and present me with any of it's elements.
If you take the existential quantifier in logic to capture the knowledge of some object (not it's blank existence in the real of possible objects), then you can't accept AoC. It breaks the constructive semantics one may or may not want to adopt for ones logic (syntatic framework and derivation calculus)
