Why does this formulation of Choice not follow from the Comprehension Schema?

Question

I have been thinking about the following formulation of the Axiom of Choice.:

For any relation $R$, there is a function $H$, which is a subset of $R$, and such that $\operatorname{dmn}H=\operatorname{dmn}R$.

At first, it seemed surprising to me that this did not follow from Comprehension (i.e., from the schema $\forall x_1, x_2, ..., x_n \forall C\exists B \forall x ( x \in B \Leftrightarrow x \in C \land \phi )$, where $B$ does not occur free in $\phi$).

I thought that for any relation, it seems that we should be able to define a subset of it with the same domain meeting a "functional condition". But when I tried to do this, I couldn't. However, I felt like I was getting close when I let $B$ be free in $\phi$, i.e., when I let myself say that $w$ is in $R$ and also anything in $H$ meets such and such conditions, where $H$ is the set (function) whose existence I'm trying to prove.

But my understanding is that Choice does not even follow from Naive Comprehension. So, I wondered if someone could explain the following precisely.

1. Why does the above formulation of Choice does not follow from regular Comprehension?
2. Why does it not even follow from Naive Comprehension (assuming that it does not)?

Answer 1

You can use comprehension to prove that every relation has a subset which is function with the same domain. The proof is just not very enlightening.

Let $R$ be a relation, and let $f$ be a choice function on the family $\{\{y\mid\langle x,y\rangle\in R\}\mid x\in\operatorname{dom}(R)\}$. We define $F\subseteq R$ to be $\{\langle x,y\rangle\in R\mid\langle x,y\rangle\in f\}$. Here the comprehension axiom was defined for the formula $u\in v$, with $u$ being a free variable ($\langle x,y\rangle$ in our case) and $v$ being a parameter ($f$ in our case).

Yes, this proof is not very illuminating at all. And there's a good reason too. There is absolutely no reason to expect that the function you seek is at all definable by a property, as a subset of $R$.

Formally speaking, we know that if $\sf ZF$ is consistent, then it does not prove the axiom of choice. It means that the separation schema (or bounded comprehension, if you prefer that name) does not prove the axiom of choice.

From naive comprehension we can prove contradiction, and therefore we can prove anything. In particular any version of the axiom of choice, and also $0=1$. So it does not matter that much what we can prove from that inconsistent axiom.

Answer 2

Somewhat intuitivelyish speaking (there exists formal proof for that axiom of choice can't be proved from the other axioms, but I'm not the one to provide such a proof):

The axiom of choice does not a priori assume a predicate to use for the comprehensions. Think of it more that the axiom of choice provides such a predicate (or function) to use.

In order to restrict a relation to a function you must have a way to for each $x$ select which of the values $y$ such that $xRy$ to have. If you explicitely have such a way (for example choosing the unique smallest of $y$) you can use axiom of comprehension to restrict it to a function.