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?

  • 2
    $\begingroup$ 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. $\endgroup$ – Asaf Karagila Jul 10 '13 at 10:47
  • $\begingroup$ And once you have global choice, you can define $f$ for any other predicate by using that global choice function. $\endgroup$ – Asaf Karagila Jul 10 '13 at 10:52
  • $\begingroup$ @AsafKaragila, so does that mean the answer is 'no'? If so, I find this surprising. $\endgroup$ – goblin Jul 10 '13 at 11:10
  • 1
    $\begingroup$ You should read about Skolem functions. $\endgroup$ – Asaf Karagila Jul 10 '13 at 12:26
  • 3
    $\begingroup$ Related MO question $\endgroup$ – aws Jul 10 '13 at 12:36

The paradox is resolved here (thank you for the link, aws). In brief:

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

  2. No, otherwise the axiom of choice would be provable in any set theory in which the axiom of union and the axiom schema of separation hold. So in particular, ZF would prove choice.

  3. Since this question is predicated on the assumption that the answers to the previous two questions are 'yes', we may disregard it.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.