I’ve been thinking recently about different versions of Global Choice, which are equivalent in the presence of Powerset but not equivalent in its absence. As part of this I realized that this gives the answer to how different formulations of what I’ve variously seen called Class Choice/Class Collection/Class Bounding relate in the absence of Global Choice.

Let me describe two different formulations. The first I will call Class Collection. This schema asserts that if $\varphi(x,Y,A)$ is any formula with a (set or class) parameter $A$ then if for each $x$ there is a $Y$ so that $\varphi(x,Y,A)$ then there is a single class $C$ so that for each $x$ there is an index $i$ so that $\varphi(x,(C)_i,A)$, where $(C)_i = \{ y : (i,y) \in C \}$ is the $i$-th slice of $C$. In words: we can collect witnesses that $\varphi$ holds for each $x$ into a single coded hyperclass.

The second formulation, I will call it Class Choice, is a little stronger. Rather than just asserting that we can collect witnesses into a single coded hyperclass, it asserts that the index for the witness for $x$ is $x$ itself. More formally, an instance of Class Choice asserts that if for each set $x$ there is a class $Y$ so that $\varphi(x,Y,A)$ then there is a single code $C$ for a hyperclass so that for each $x$ we have $\varphi(x,(C)_x,A)$.

And we can get fragments of Class Collection or Class Choice by limiting which formulae are allowed. Of particular interest to me are Elementary Class Collection and Elementary Class Choice, which limit the formulae allowed to those whose quantifiers are all only over sets.

Previously, it was a little mysterious to me just how the two schemata related. Obviously, Class Choice implies Class Collection, but it wasn’t quite clear what was needed to get the reversal. But it turns out that a version of Global Choice which I’ve been calling Coded Hyperclass Choice is exactly what bridges the gap. Let me state the results which give the connection, then I’ll explain what Coded Hyperclass Choice is, and then give the proofs. At the end I’ll say where Coded Hyperclass Choice fits among the other variants of Global Choice

Proposition 1 Work over the base theory $\mathsf{GB}^-$. Let $\varphi(x,Y,A)$ be a formula with a parameter $A$. Then the instance of Class Collection for $\varphi$ plus Coded Hyperclass Choice plus Comprehension for properties elementary in $\varphi$ implies the instance of Class Choice for $\varphi(x,Y,A)$.

Proposition 2 Work over the base theory $\mathsf{GB}^-$. Then Elementary Class Choice implies Coded Hyperclass Choice.

Corollary Let $k \ge 0$. Then, over $\mathsf{GB}^-$, we have that $\Pi^1_k$-Class Choice is equivalent to $\Pi^1_k$-Class Collection plus Coded Hyperclass Choice.

The base theory $\mathsf{GB}^-$ is Gödel–Bernays set theory without Powerset and without Global Choice.

Definition (Over $\mathsf{GB}^-$) Coded Hyperclass Choice asserts that coded hyperclasses (of nonempty classes) admit choice functions. That is, if $C$ is a class of pairs then there is a class function $F$ so that for each $x \in \mathrm{dom}\ C$ we have $(x,F(x)) \in C$.

Proof of Proposition 1: Assume that for each $x$ there is $Y$ so that $\varphi(x,Y,A)$ holds. We want to find a class $C$ so that $\varphi(x,(C)_x,A)$ holds for each $x$. We know, by the instance of Class Collection for $\varphi(x,Y,A)$, that there is a class $D$ so that for each $x$ there is $i$ so that $\varphi(x,(D)_i,A)$. Now let $E$ be the class defined as $E = \{ (x,i) : \varphi(x,(D)_i,A) \}$. This is a class because its definition is $\Delta^1_0$ in $\varphi$, and we have assumed exactly the corresponding fragment of Comprehension. Apply Coded Hyperclass Choice to $E$ to get a class function $F$ so that $(x,F(x)) \in E$ for all sets $x$. We can now define the desired $C$, namely as $C = \{ (x,y) : (F(x),y) \in D \}$. ∎

Proof of Proposition 2: Fix a code $C$ for a hyperclass of nonempty classes, i.e.\ $C$ is a class of pairs. We want to find a function $F$ so that $(x,F(x)) \in C$ for all $x \in \mathrm{dom}\ C$. Fix an arbitrary $x$. Note that if $x \in \mathrm{dom}\ C$ then there is a singleton class $Y = \{y\}$ so that $(x,y) \in C$. We don’t need any fragment of choice to make this conclusion, beyond that afforded by first-order logic, as this is just finite choice. (We would need a form of choice to pick such $Y$ for all $x$ simultaneously, but that’s getting ahead of ourselves.) So by Elementary Class Choice there is a code, which I suggestively call $F$, for a hyperclass so that for each $x$ if $x \in \mathrm{dom}\ C$ then $(F)_x$ is such a $Y$ for $x$. Now observe that $F$ is in fact a function, since $(F)_x$ is always a singleton for $x \in \mathrm{dom}\ F$. And by construction we have $(x,F(x)) \in C$ for each $x \in \mathrm{dom}\ C$, as desired. ∎

Proof of Corollary: This follows from the two propositions by using the facts that $\Pi^1_k$-Class Collection implies that the class of essentially $\Pi^1_k$ formulae is closed under quantification by sets and that $\Pi^1_k$-Class Collection implies $\Pi^1_k$-Comprehension. ∎

So the gap between Class Choice and Class Collection is exactly filled by Coded Hyperclass Choice. Let’s see where it fits in with the global choice principles. If our base theory includes Powerset, then we have many equivalent ways to formulate Global Choice. But absent Powerset they separate. Observe that the existence of global well-order immediately implies Coded Hyperclass Choice: to get a choice function for a coded hyperclass just use the global well-order to pick the least member of each slice. And Coded Hyperclass Choice implies the existence of a global choice function, by considering the coded hyperclass $\{ (x,y) : y \in x \wedge x \ne \emptyset \}$.

It cannot be that Coded Hyperclass Choice is equivalent to both the existence of a global well-order and the existence of a global choice function, as the latter is strictly weaker than the former over $\mathsf{GB}^-$. Does it sit strictly between them?

Question Work over the base theory $\mathsf{GB}^-$. Does Coded Hyperclass Choice imply the existence of a global well-order? Does the existence of a global choice function imply Coded Hyperclass Choice?