Notation arb(x)

Suppose we have extended $ZF$ by adding to $ZF$ an unary function symbol $arb$ (an arbitrary element of a set) and a corresponding axiom "For every non-empty set $S$, $arb(S)$ is in $S$". Will be the resulting theory a conservative extension of $ZF$?

-
It seems to me that the answer is an obvious yes, given a proof there are only finitely many instances of $arb$ in the formulas and you can just replace each instance with the "mini-proof" that $S\neq\varnothing$ therefore we can fix some $s\in S$. This happens finitely many times so we're good without appealing to the axiom of choice. –  Asaf Karagila Jan 20 '13 at 14:05
@Asaf Surely not. Using replacement, I can (uniformly!) construct a choice function for every family of non-empty sets, so in particular this theory proves the axiom of choice! –  Zhen Lin Jan 20 '13 at 15:21
@Zhen Lin, oh yeah. It seems like you can easily get global choice from this simply take $\lbrace(x,arb(x))\mid x\neq\varnothing\rbrace$. I was thinking in terms of a "dynamic oracle" so to speak... :-) –  Asaf Karagila Jan 20 '13 at 15:37
It depends how the remaining axioms of ZF are altered (or not). For example, do we broaden the scheme of replacement to apply to formulas of set theory which contain the symbol "$arb$"? If so, then as Zhen Lin says the resulting theory proves the axiom of choice: given a collection of sets $\mathcal{A}=\lbrace A_i: i\in I\rbrace$, applying replacement to the formula "$x=arb(S)$" as $S$ ranges over the elements of $\mathcal{A}$ yields a choice function. If we don't do this - that is, if we have replacement and separation only for sentences of the language of set theory without "$arb$" - then we do in fact get a conservative extension: given any model $\mathcal{M}$ of ZF, let $arb$ pick any element from each element of $\mathcal{M}$ (I guess I'm using Choice in the ambient universe to do this, but if all we care about is not proving any new theorems, then this can be gotten rid of by Shoenfield absoluteness); the resulting extension is a model of ZF with $arb$.
There are only finitely many explicit instances of $arb$ in any proof; but there may be one "mass-instance" of $arb$ being applied to every member of a set of sets, via Replacement. The second step of your algorithm involves replacing each actual instance of $arb$ by a specific choice, which does work if there are only finitely many $arb$s, but fails if we have a mass instance of $arb$. (Wow, that didn't come out nearly as clearly as it sounded in my head. :p ) –  Noah S Jan 20 '13 at 16:31
Hm, I think what Noah is saying is that even inside one sentence, we may end up evaluating $\textrm{arb}(x)$ for infinitely many $x$. (For example, $\forall x . (\exists y \in x) \to \textrm{arb}(x) \in x$.) –  Zhen Lin Jan 20 '13 at 20:41