After studying the axiom of dependent choice, I tried to think of a possible generalization of the axiom that would work in a similar way on infinite uncountable sets: by replacing the binary relation with a general set membership relation over ordinal-indexed elements, I finally obtained the axiom below.
Remark: in order to make the axiom easier to read, I use the notation $(\underbrace{y_0, y_1, \dots}_{\alpha})$ to denote a map of elements indexed over an ordinal $\alpha$.
Generalized Axiom of Dependent Choice: given a set $X$, an element $x_0\in X$, a limit ordinal $\beta$, and a set $R$ containing elements of $X$ indexed over any $\alpha\in\beta$, suppose that the following two relations hold:
$
(a)\quad \forall \alpha\in\beta\,:\,(\underbrace{y_0, y_1, \dots}_{\alpha})\in R\,\,\Rightarrow\,\,\exists z\in X : (\underbrace{y_0, y_1, \dots, z}_{\alpha+1})\in R
$
$(b)\quad$ if $\sigma$ is a sequence of elements of $X$ indexed by a limit ordinal $\gamma\in\beta$ such that each initial segment of $\sigma$ is an element of $R$, then $\sigma$ is an element of $R$.
Then there exists a function $f\,:\,\beta\,\mapsto\,X$ s.t. $f(0)=x_0$ and
$$
\forall\alpha\in\beta\,:\,(\underbrace{f(0), f(1), \dots}_{\alpha})\in R
$$
Do you think this is a valid and sound generalization? I found simple proofs of the following facts:
if $\beta=\omega$ (i.e. the first infinite ordinal), then the generalized version is equivalent to the axiom of dependent choice with fixed first element.
the generalized axiom of dependent choice implies the axiom of choice on the ordinals (although it is not clear if they are also equivalent)
although inherently non-constructive, the generalized axiom hints to a 'method' for building the function $f\,:\,\beta\,\mapsto\,X$: choose $x_0$ as the first element, then randomly select the following elements $x_1, x_2,\dots$ in such a way that the sequence $(x_0,x_1,x_2,\dots)$ is still in $R$. This seems to be an intuitive process
if we replace the condition $\cdots\Rightarrow\,\,\exists z\in X\cdots$ with the condition $\cdots\Rightarrow\,\,\exists ! z\in X\cdots$ (where the existing element $z\in X$ is also unique) then the function $f\,:\,\beta\,\mapsto\,X$ is provably unique. Although the changed version may seem to be provable in ZF, it is not a consequence of the axiom schema of replacement, nor it is definable via transfinite recursion - in other words, I suspect it is independent of ZF.
I would like to receive some feedback from other logicians: does this look like a valid generalization? Do you think it may be worth of a publication, and in case, in which journal?
Please share your thoughts about this, thank you in advance and have a great day!
Kind regards,
Gianluca Calcagni