Is Global Choice conservative over Zermelo with Choice? To be explicit, by Zermelo set theory with Choice, ZC, I mean the theory with the same language and axioms as ZFC except not Foundation (also called Regularity) and with the axiom scheme of Separation instead of Replacement.  By Global Choice I mean adding a new function symbol $F$ and an axiom:$\forall v[v\neq\emptyset \rightarrow F(v)\in v]$, and extending the Separation scheme to include formulas using $F$.
It is known that the axiom of Global Choice gives a conservative extension of Zermelo Frankel set theory with Choice (ZFC).  The proof I know is by  Haim Gaifman in his "Local and Global Choice Functions" (Israel J. of Math v. 22 nos. 3-4, 1975, pp. 257--265.  And there is one I have not worked through which uses forcing by Ulrich Felgner "Comparison of the axioms of local and universal choice" Fund. Math. 71, 1971, pp. 43-62.  Both seem to require the idea of the rank of a set.  Maybe one can be adapted to work for ZC, but I do not see it.
Or is there some other proof? Or a disproof?
 A: The known proofs of conservativity of ZF + GC (Global Choice) over ZFC make significant use of replacement, and as far as I know the problem of conservativity of Z + GC over ZC is wide open. 
Let me add that I have discussed the problem with a number of experts over the past two decades, and also posed it on FOM in 2006 in this posting.
A: Global Choice is not conservative over ZC. We'll build a model of ZC which satisfies a sentence disprovable by Global Choice. Warning: it is hideous, and I've been struggling to come up with a clean way to present it.
We work in ZF + GCH below $\aleph_{\omega}$ + existence of countable sets $(X_n)_{n<\omega}$ such that there is a surjection $f: \mathcal{P}(\bigcup_{n<\omega} X_n) \rightarrow \omega_2.$ This holds in a symmetric extension of $L$, see Asaf Karagila's Iterated failures of choice, section 4.
The model we construct will satisfy ZC + GCH and that every infinite set has cardinality some $\aleph_n,$ yet will code $(X_n)_{n<\omega}$ and $f$ by definable classes. Note that we are identifying $\aleph_n$ with the canonical prewellordering of $\mathcal{P}^n(\omega)$ of length $\omega_n$ since the von Neumann construction of the $\aleph$'s doesn't work in ZC.
Let $X = \bigcup_{n<\omega} X_n.$ There will be Quine atoms $a_x$ for each $x \in X$ and $a_Y$ for each $Y \subset X.$
Let $B = \{V_{\omega}\} \cup \{\{a_x: x \in X_n\}: n<\omega\}\cup \{\{a_Y\}: Y \subset X\}.$
Consider this model:
$$M_1=\bigcup_{n<\omega}\bigcup_{S \in [B]^{<\omega}} \mathcal{P}^n(\bigcup S).$$
Then $M_1 \models ZC + GCH + \forall S \exists n (|S| \le \aleph_n).$
Let $P = \{(n, a_x): x \in X_n\} \cup \{(a_x,a_Y): x \in Y \subset X\} \cup \{(a_Y, f(Y)): Y \subset X\}.$ We will build an extension of $M_1$ in which $P$ is a definable predicate. For each $p \in P,$ let $b_p = \{p, b_p\}.$
Let $C = B \cup \{\{b_p\}: p \in P\}.$
Let $M = \bigcup_{n<\omega}\bigcup_{S \in [C]^{<\omega}} \mathcal{P}^n(\bigcup S).$
Then $M \models ZC + \varphi,$ where $\varphi$ is the conjunction CH $\wedge$ $``$the class $\{p: \exists b (b=\{b, p\})\}$ codes a countable sequence of countable sets of atoms $X_n,$ a class of atoms which each relate to a different subclass of $\bigcup_{n<\omega} X_n,$ and a surjection from the latter class onto $\aleph_2."$
Finally, we see that Global Choice proves $\neg \varphi,$ since from a global choice function, we can choose enumerations of each $X_n,$ enumerate $\bigcup_{n<\omega} X_n,$ and thus define a surjection from $\mathcal{P}(\omega)$ onto $\omega_2,$ violating CH.
Also note that we can adjust the construction of $M$ so that it satisfies Foundation by several applications of the trick used here: Is $\in$-induction provable in first order Zermelo set theory?
