Return to Question

Deep Choice: $\forall X \ [\forall a,b \in X \, ( a \neq \emptyset \land (a \neq b \to a \cap b = \emptyset)) \to \\ \exists Y \exists f \,(f: X \rightarrowtail Y \land \forall x \in X \,( f(x) \in \operatorname {tc}(x)))]$

In English: for every family $X$ of pairwise disjoint nonempty sets, there is an injective function that sends each element $x$ of $X$ to an element of the transitive closure of $x$.

Denote this principle $``\sf Dp C\!"$

Is the following true?

$(\sf ZF + DpC) \to AC$

Deep Choice: $\forall X \ [\forall a,b \in X \, ( a \neq \emptyset \land (a \neq b \to a \cap b = \emptyset)) \to \\ \exists Y \exists f \,(f: X \rightarrowtail Y \land \forall x \in X \,( f(x) \in \operatorname {tc}(x)))]$

In English: for every family $X$ of pairwise disjoint nonempty sets, there is an injective function that sends each element $x$ of $X$ to an element of the transitive closure of $x$.

Denote this principle “$\mathsf{DpC}$”.

Is the following true?

$(\mathsf{ZF} + \mathsf{DpC}) \to \mathsf{AC}$.

Deep Choice: $\forall X \ [\forall a,b \in X \, ( a \neq \emptyset \land a \cap b = \emptyset) \to \\ \exists Y \exists f \,(f: X \rightarrowtail Y \land \forall x \in X \,( f(x) \in \operatorname {tc}(x)))]$

In English: for every family $X$ of pairwise disjoint nonempty sets, there is an injective function that sends each element $x$ of $X$ to an element of the transitive closure of $x$.

Denote this principle $``\sf Dp C\!"$

Is the following true?

$(\sf ZF + DpC) \to AC$

Deep Choice: $\forall X \ [\forall a,b \in X \, ( a \neq \emptyset \land (a \neq b \to a \cap b = \emptyset)) \to \\ \exists Y \exists f \,(f: X \rightarrowtail Y \land \forall x \in X \,( f(x) \in \operatorname {tc}(x)))]$

In English: for every family $X$ of pairwise disjoint nonempty sets, there is an injective function that sends each element $x$ of $X$ to an element of the transitive closure of $x$.

Denote this principle $``\sf Dp C\!"$

Is the following true?

$(\sf ZF + DpC) \to AC$

Deep Choice: $\forall X \exists Y \exists f \,(f: X \to Y \land \forall x \in X: x \neq \emptyset \to f(x) \in \operatorname {tc}(x))$

In English: for every set $X$ there is a function that sends each nonempty element $x$ of $X$ to an element of the transitive closure of $x$. Denote this principle $``\sf Dp C\!"$

Is the following true?

$(\sf ZF + DpC) \to AC$

Deep Choice: $\forall X \ [\forall a,b \in X \, ( a \neq \emptyset \land a \cap b = \emptyset) \to \\ \exists Y \exists f \,(f: X \rightarrowtail Y \land \forall x \in X \,( f(x) \in \operatorname {tc}(x)))]$

In English: for every family $X$ of pairwise disjoint nonempty sets, there is an injective function that sends each element $x$ of $X$ to an element of the transitive closure of $x$. 

Denote this principle $``\sf Dp C\!"$

Is the following true?

$(\sf ZF + DpC) \to AC$