Formulating the axiom of choice with a new function symbol without also getting global choice

Question

Is there a way to formulate the axiom of choice by adding a single "choice-like" function symbol to set theory without also adding the axiom of global choice?

Bourbaki's $\tau$ or variations thereof can be defined as taking sets, sets or proper classes, or propositions with a designated free variable as arguments. If $\tau$ takes a set as an argument and returns a set, then it is a unary function in the theory of sets.

I'm pretty sure that adding any version of $\tau$, even one that is restricted to taking sets as arguments, gives you a theory with the axiom of global choice. In this Wikipedia article, $\tau$ is described as picking an arbitrary element from every nonempty set; proper classes and propositions are not mentioned. I'm assuming that the various flavors of $\tau$ are basically equivalent.

---

Here's my attempt to add a function symbol that sends every set to the graph of its choice function. I'm pretty sure that doing so gives you the axiom of global choice.

Since doing the obvious thing didn't work, I'm wondering whether what I'm trying to do is even possible.

I've seen formulations of the axiom of choice that use indexed families of sets of choice functions.

Here's the choice function formulation given on Wikipedia expressed using slightly different syntax. For every nonempty set $X$, there exists a choice function $f$.

$$ \forall X \supsetneq \emptyset \mathop.\;\; \exists f : X \to \cup X \mathop.\;\; \forall A \in X \mathop. \;\; f(A) \in A $$

Choice functions are unary functions and as such have a natural encoding as sets.

$$ f \;\text{as a set} \;\; \text{is equal to} \;\; \{ (x, f(x)) \mathop| x \in X \} $$

It, seems like, in principle, we could add a new function symbol $\sigma$ that just sends every nonempty set to the graph of a choice function. $\sigma$ is supposed to be analogous to a Skolem function for the axiom of choice. I'm pretty sure that this step strengthens the axiom because the newly minted $\sigma$ can be used to define $\tau$.

$$ \sigma(\emptyset) \;\; \text{is arbitrary} $$ $$ \sigma(X) = \;\; \text{$f$ as a set where $f$ is the choice function for $X$} $$

$\sigma$ can now be treated as a function symbol in a theory of sets. It isn't expressible as a function because its domain and codomain are proper classes, but it can be a function symbol in the same way that $\in$ is a relation symbol.

We can define Bourbaki's $\tau$ in terms of $\sigma$ in the following way.

$$ \tau(X) \;\;\text{can be defined as}\;\; \sigma({X})(X) $$

Answer 1

No. Once you add a symbol, and you require that it chooses an element from each set, you've effectively added global choice.

The reason why global choice is stronger than the axiom of choice is that for each family of sets there exists a choice function, but we cannot amalgamate these choice functions over all sets uniformly (unless, of course, we can choose one for each set, but then we already appeal to global choice).

Now, the problem with adding a symbol to the language is that it is interpreted in the structure. So it is now a fixed choice function which we can always refer to. And that's just global choice.

If it's any consolation, every model of ZFC can be extended to a model of ZFC+Global choice without adding sets, if we instead add a new symbol for the choice function. This can be done via class forcing.