3
$\begingroup$

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 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.

Improve this question
$\endgroup$
10
  • 2
    $\begingroup$ Your axiom SC sounds like not an axiom in the usual sense, but rather it seems like you want to extend the language to include such functions (ZF alone proves that for any nonempty $X$ there is a map from a singleton to $X$). If so, then this is reminiscent of Hilbert's epsilon or Bourbaki's tau operators: en.wikipedia.org/wiki/Epsilon_calculus $\endgroup$
    – Wojowu
    Commented Mar 3, 2021 at 20:46
  • $\begingroup$ @Wojowu ZF proves that such a map exists, but can we choose a specific one? This axiom is asserting a choice of a specific function, viewed as a set of doubletons, whose domain is the set containing $0$ and whose codomain lies in the set we want to choose from. Unless I'm mistaken, this is reminiscent of the difference between fibrations and cloven fibrations; we know that Cartesian arrows exist in the total category, but to select a specific one we need choice. If we assume that all fibrations can be cloven, we get the axiom of choice. This axiom is meant to be similar to choosing (cont.) $\endgroup$
    – Alec Rhea
    Commented Mar 3, 2021 at 20:50
  • $\begingroup$ @Wojowu specific Cartesian arrows as opposed to simply knowing they exist; instead of just knowing that a map from a singleton to $X$ exists, we have a specific chosen map to work with. $\endgroup$
    – Alec Rhea
    Commented Mar 3, 2021 at 20:51
  • $\begingroup$ "can we choose a specific one?" is a question which to me doesn't make sense on the grounds of first-order logic. How would you formalize that? $\endgroup$
    – Wojowu
    Commented Mar 3, 2021 at 20:52
  • 1
    $\begingroup$ What you want then sounds to me essentially like a global choice function, a class function assigning an element to every nonempty set. Over NBG its existence is equivalent to usual formulations of global choice. I don't think you can formulate it in the language of ZF. $\endgroup$
    – Wojowu
    Commented Mar 3, 2021 at 20:57

1 Answer 1

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
14
  • $\begingroup$ Very cool, thank you. $\endgroup$
    – Alec Rhea
    Commented Mar 3, 2021 at 21:10
  • $\begingroup$ How would you write the axiom SC in the language of ZF (as a schema or otherwise)? $\endgroup$
    – Wojowu
    Commented Mar 3, 2021 at 21:12
  • 2
    $\begingroup$ I see, so at any rate you have to expand the language (by this Skolem function). This was my main concern here (as I expressed in comments to the question). $\endgroup$
    – Wojowu
    Commented Mar 3, 2021 at 21:30
  • 2
    $\begingroup$ @Wojowu: Yes, you have to add something. You can add an axiom instead that states that $V=\rm HOD$ (up to a set, if you must) and then use that to define a choice function. But that's as good as it gets. Add a symbol, or add an axiom. In either case, it's barely a schema. $\endgroup$
    – Asaf Karagila ♦
    Commented Mar 3, 2021 at 22:01
  • 2
    $\begingroup$ As far as I can see, your (SC) amounts to adding to the language of ZF a unary function symbol, say $C$, adding to ZF the axiom schema $\forall x\,(x\neq\varnothing\to C(x)\in x)$, and introducing the notation $f_x(0)$ for $C(x)$. Then you should also extend the separation and collection (or replacement) schemas of ZF to allow formulas containing $C$. $\endgroup$
    – Andreas Blass
    Commented Mar 4, 2021 at 2:52

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .