# Extending our language with a new function symbol

Given an arbitray first-order theory (not necessarily a set theory) and definable predicates $P(*)$ and $Q(*,*)$ in the language of that theory, if we adjoin a new function symbol $f$ together with the axiom $$\forall x(P(x) \Rightarrow \exists y(Q(x,y))) \Rightarrow \forall x (P(x) \Rightarrow Q(x,f(x)))$$

is this extension necessarily conservative? Note that we're not requiring that the $y$ satisfying $Q(x,y)$ be unique in the antecedent.

Okay that was my first question. Supposing the answer is 'yes', my second question is this. Suppose our original first-order theory includes an axiom schema like separation, or replacement that runs over the definable predicates of our old language. Does the more general schema running over the definable predicates of the extended language also hold?

Finally, and this is probably a silly question, but supposing that both answers are yes, why doesn't this make the Axiom of Choice redundant?

• Note that taking $P(x)$ to be $x\neq\varnothing$ and $Q(x,y)$ to be $y\in x$ we have that $f$ is a global choice function. Commented Jul 10, 2013 at 10:47
• And once you have global choice, you can define $f$ for any other predicate by using that global choice function. Commented Jul 10, 2013 at 10:52
• @AsafKaragila, so does that mean the answer is 'no'? If so, I find this surprising. Commented Jul 10, 2013 at 11:10
• You should read about Skolem functions. Commented Jul 10, 2013 at 12:26
• Related MO question
– aws
Commented Jul 10, 2013 at 12:36

1. Yes, adjoining such an $f$ together with such an axiom is indeed conservative.