While reviewing some categorical versions of the axiom of choice, it occurred to me that none of the formulations I'm aware of actually reflect how I use choice in practice: pronounce that we 'choose an element $x$ of $X$' or something like this.


That is, while I understand that 'every surjection in ${\bf Set}$ splits' and 'every collection of nonempty sets has a choice function' etc. are ways to formalize choice that can be mildly contorted to give the way I used it above (surject onto a singleton and split, consider a collection containing one set, etc.), none of them straight up axiomatize my intuitive usage of choice. To this end:



> 
> Define **simple choice** (SC) to be the axiom asserting that every nonempty set $X$ comes equipped with a **simple choice function** $$f\_X:1\to X,$$ where $1$ is the ordinal (and not some random singleton, to make things more concrete).
> 
> 
> 


Using SC, when we say 'choose an element $x$ of $X$' we really mean 'look at $f\_X(0)$', instead of the above more involved interpretations. For any nonempty collection of sets $Y$, I believe we can define a choice function $c\_Y:Y\to\bigcup Y$ in the classical sense with $c\_Y(X)\in X$ for all $X\in Y$ by defining $$c\_Y(X)=f\_X(0).$$


Further, while the classical versions introduce auxiliary contortions that are relatively harmless when working with sets, we suddenly have to use things like [Scott's trick](https://ncatlab.org/nlab/show/Scott%27s+trick) to get good behavior when working with the globalized versions of choice and proper classes -- the globalized version of SC seems to work in a more straightforward manner with proper classes.


Working in $MK$, let's call global simple choice (GSC) the axiom asserting that every nonempty class $X$ comes equipped with a simple choice function $f\_X:1\to X$. I believe this implies global choice in the same manner that it implies regular choice above, but if we have a proper class and want to select an element of it we don't need Scott's trick to intersect with some stage of the cumulative hierarchy anymore.


I'm certain that I'm not the first one to cook up something like this, so my questions are



> 
> What is wrong with this version of choice? Is it actually equivalent to the standard formulation? If it is equivalent, is this version of it less appealing for some reason that isn't occurring to me? Are there existing references to it somewhere?
> 
> 
> 


Any assistance is appreciated.



A simple form of choice
Nothing is wrong with this version of choice. In $\sf ZF$, and the theories extending it, it is indeed equivalent to Global Choice, exactly by using Scott's trick. You just smooth it out by putting this into the language.


The difference will come if you start allowing proper class of atoms (non-sets). In that case, it is consistent that there is a proper class of atoms, but every set of atoms is finite. If we had this "simple global choice", which chooses from every class, rather than every set, we could have used it to choose atoms and inject the class of ordinals into the atoms (so in particular, there are sets of atoms of any given cardinality).




---


As a side note, do pay attention to the fact that classes are not objects in $\sf ZF$, so you cannot write this as a sentence (and barely as a schema) if you're working in $\sf ZF$. But if you're moving to second-order theories like $\sf KM$ or $\sf NBG$, then that's not a problem anymore.


