Can $\sf AC_\omega$ and $\sf DC$ be generalized? When one come across axiom of choice, one reads about weaker forms like countable choice $\sf AC_\omega$ and dependent choice $\sf DC$.

Are there known uses of restrictions to higher cardinals like $\sf AC_{\omega_1}$ for example, or more generally $\sf AC_{\omega_\alpha}$ or a restriction to a stage of the cumulative hierarchy $\sf AC_{V_\alpha}$?


Along the same lines, are there higher forms of $\sf DC$ that use longer sequences, for example $\sf DC_{\omega_1}$ that uses $(x_n)_{n \in \omega_1}$ instead of $(x_n)_{n \in \mathbb N}$, so we may generally have $\sf DC_{\omega_\alpha}$.


What is the comparison in consistency strength between the two lines? For example how $\sf DC$ compare with the $\sf AC_{\omega_\alpha}$'s.

 A: Yes, there are general variants of both $\sf DC$ and $\sf AC_\omega$.

*

*Since $\sf AC$ is about choice functions from a family, we can give it three parameters. I follow the convention1 that $\sf AC_X^Y(Z)$ means "Every family of subsets of $\sf Z$ which is in bijection with $\sf X$, and every member is in bijection with $\sf Y$ admits a choice function". When we omit one of the parameters, we replace it with a universal quantification. So $\sf AC^{\rm fin}(\Bbb R)$ would be the axiom of choice for arbitrarily families of finite subset of $\Bbb R$, for example; and $\sf AC_{WO}$ is the axiom of choice for arbitrarily families that can be well-ordered.


*$\sf DC$, in contrast, talks about iterations of a function, and sequences, so it is inherently well-ordered. So when we write $\sf DC_\kappa$ it only makes sense that $\kappa$ is an $\aleph$ number. We can still restrict to a set with $\sf DC_\kappa(X)$,2 and while the formulations using relations and sequences is a bit awkward, we have a simpler formulation in terms of trees: $\sf DC_\kappa(X)$ means that every $\kappa$-closed tree on $X$ has a branch of length $\kappa$. Again, removing $X$ means a universal quantification, and we can write $\sf DC_{<\kappa}$ for $\forall\lambda<\kappa\,\sf DC_\lambda$.
Now, $\sf AC_{WO}$ implies $\sf DC$, but not $\sf DC_{\omega_1}$. And $\sf DC_\kappa$ does not imply $\sf AC_{WO}$ for any $\kappa$. If you also look closely, you will see that $X$ can be well-ordered if and only if $\mathcal P(X)\setminus\{\varnothing\}$ admits a choice function. So $\mathsf{AC}_{V_\alpha}$ implies that for all $\beta<\alpha$, $V_\beta$ can be well-ordered. It is not equivalent, of course, since $\sf AC_\omega$ can fail for the first time in an arbitrarily high rank.
It is worth pointing out that $\sf AC_X$ does not come up very often. One of the reasons is that we don't really understand sets that cannot be well-ordered, so it's hard to work with them. We can prove a few small things, e.g. that $\sf AC_X$ holds when every surjection onto $X$ admits an inverse, but not a whole lot more.
One of the reasons is that we never really had good tools for preserving $\sf AC_X$ for an arbitrary set $X$. Although in one of my recent papers I provide a crude preservation theorem for symmetric extensions that allows us to prove $\sf AC_X$ holds for some sets $X$ which cannot be well-ordered.
As for the consistency strength, all these are of course equivalent, since they all follow from $\sf ZFC$, which is equiconsistent with $\sf ZF$. You can look at Jech's "Axiom of Choice" book, where Chapter 8 is dedicated for these principles; and in the Howard–Rubin dictionary of choice principles as well.

Footnotes.

*

*Some people use the opposite notation for superscript and subscripts, i.e. $\sf AC^{WO}$ for what I'd write $\sf AC_{WO}$. This is confusing, yes. Other people use something like $X$-$\sf AC$.


*Here too there is a discrepancy in notation, some people use $\sf DC_X$ to denote $\sf DC(X)$, and $\kappa$-$\sf DC$ to denote $\sf DC_\kappa$. Again, confusing.
