1
$\begingroup$

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?

$\endgroup$
10
  • 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 ♦
    Commented Jul 10, 2013 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 ♦
    Commented Jul 10, 2013 at 10:52
  • $\begingroup$ @AsafKaragila, so does that mean the answer is 'no'? If so, I find this surprising. $\endgroup$
    – goblin GONE
    Commented Jul 10, 2013 at 11:10
  • 1
    $\begingroup$ You should read about Skolem functions. $\endgroup$
    – Asaf Karagila ♦
    Commented Jul 10, 2013 at 12:26
  • 3
    $\begingroup$ Related MO question $\endgroup$
    – aws
    Commented Jul 10, 2013 at 12:36

1 Answer 1

Reset to default
1
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .