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) $$