# Necessity of uniqueness in extension by definition

Wikipedia says that if we can prove $$\forall x_1...\forall x_n \exists! y . \phi(y,x_1,...,x_n)$$, then introducing a function symbol $$f$$ and the axiom $$\forall x_1...\forall x_n.\phi(f(x_1,...,x_n),x_1,...,x_n)$$ gives a conservative extension of the original theory. I'd like to understand the importance of the uniqueness requirement. Specifically,

1. The "0-ary" case: If we've proved $$\exists x.\phi(x)$$ without the uniqueness part, is it safe (i.e. conservative) to introduce a constant symbol $$c$$ and an axiom $$\phi(c)$$? We seem to allow this in natural-language proofs (as in "at least one element satisfies $$\phi$$, so let $$c$$ be one of them").

2. If we start with ZF set theory and allow function symbol extensions without the uniqueness requirement, is the resulting proof system equivalent to ZFC in some sense? (It seems like it would prove the axiom of choice. Is it stronger than ZFC?)

Edit: I came across the conservativity theorem, which suggests that the uniqueness requirement is not necessary. Now I'm wondering:

1. Does the proof of the conservativity theorem require the axiom of choice (in the metatheory)?
2. What's wrong with this argument: By introducing a choice function symbol (as described in the second part of this question), we can prove AC from ZF. By the conservativity theorem, we conclude that AC is a consequence of ZF. This contradicts the independence of AC.
• The uniqueness condition on $\phi$ is required in order to have a function: if for some $n$-uple $x_1,\ldots, x_n$ we have two values $y_1 \ne y_2$ that satisfy the formula, we cannot pick the $y$ that must be the value of $f$. – Mauro ALLEGRANZA Sep 11 at 6:50
• Why can't we just pick one such $y$ arbitrarily? If our metatheory includes the axiom of choice, can't we show that any model $M$ satisfying the existence sentence admits a function $f:M^n \to M$ that interprets the introduced function symbol in a way that satisfies the introduced axiom? – Karl Sep 11 at 7:17

It does allow us to add a $$\operatorname{Choice}$$ function symbol to the language (and the axiom $$\forall x(x\ne\emptyset\implies\operatorname{Choice}(x)\in x)$$), but this doesn't enable the proof of AC that I had in mind, which attempts to define the choice function $$f:S\to\bigcup S$$ as $$f=\{(x,\operatorname{Choice}(x)):x\in S\}$$. The problem is that this last expression invokes replacement with a formula containing the new symbol, whereas the axiom schema only includes formulas in the language of $$\in$$.