About the “Axiom of Dependent Choice”

[steenis]

I learned something new today: the “Axiom of Dependent Choice”:

The axiom can be stated as follows: For every nonempty set $X$ and every entire binary relation $R$ on $X$, there exists a sequence $(x_n)_{ n \in \mathbb{N} }$ in $X$ such that $x_nRx_{n+1}$ for all $n \in \mathbb{N}$. (Here, an entire binary relation on $X$ is one where for every $a \in X$, there exists a $b \in X$ such that $aRb$.)

See Wikipedia: https://en.wikipedia.org/wiki/Axiom_of_dependent_choice

I want to ask here: what is your experience with this axiom? Did you ever use the “Axiom of Dependent Choice”, how and why?

 

[andrewkirk]

I have not heard of it, but can see why it would be useful. Sometimes in real analysis one wants to make a sequence in which the next element is different from the current one. Using the relation $\neq$ and the above axiom, one can assert the existence of such a sequence in any set with two or more elements, as the relation is entire if there are more than two elements.

There was a proof that was being discussed on here the other day that needed something like that. Unfortunately I can't remember the context, other than it was real analysis - probably something about sequences. Not knowing about this axiom, I just said we had to assume AC - assuming it needed the full version.

It sounds from the wiki article like this axiom is strictly weaker than AC. It would be nice if it allowed one to recover most of the popular results of real analysis without having to accept the Banach-Tarski conundrum, or the theorem that every set can be well-ordered as a conclusion. I wonder if it is weak enough to prevent either or both of those.

 

[Erland]

I think most mathematicians use the full axiom of choice, or some of its more useful equivalents such as Zorn's lemma, when they need this kind of arguments, even in cases where the axiom of dependent choice would suffice. Because what is important fot most mathematicians is to get job done, not investigate which are the weakest assumptions necessary. It is mainly logicians, set theorists et al who are interested in the latter.