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,
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").
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:
- Does the proof of the conservativity theorem require the axiom of choice (in the metatheory)?
- 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.