In some circumstances I've been using a form of choice over the first uncountable ordinal knowing a priori that only a countable number of choices were going to be made (without any a priori upper bound). I would like to know whether I was using the classical dependent choice or something stronger and in case how much stronger.
I think the argument that I have in mind is better explained with an example and the best that I know is a proof of Ekeland's variation principle.
Such principle establishes the existence of `almost mininizers' of a function on a non-compact, but complete, metric space. Let me give a - somehow suboptimal - formulation of the result:
Theorem Let $(X,d)$ be a complete metric space and $f:X\to[0,+\infty)$ lower semicontinuous (one can assume $f$ to be continuous if he wishes). Let $\epsilon>0$. Then there exists a point $x\in X$ such that $f(x)\leq\inf f+\epsilon$ and satisfying $$ f(y)\geq f(x)-\epsilon d(x,y)\qquad\forall y\in X. $$
Thus if we could choose $\epsilon=0$ the theorem would provide the existence of a minimum for $f$, so that the requirement $\epsilon>0$ might be seen as a sort of almost minimization (also known as quasi-minimization in some contexts).
Here is a possible proof of the theorem: Let $\Omega$ be the first uncountable ordinal and let's recursively define a map $\Omega\ni \alpha\to x_\alpha\in X$ as follows. $x_0\in X$ is taken arbitrarily such that $f(x_0)<\inf f+\epsilon$. If $x_\alpha$ has already been defined, we define $x_{\alpha+1}$ as follows: if $x_{\alpha}$ satisfies the conclusion of the theorem, we put $x_{\alpha+1}:=x_{\alpha}$. Otherwise the set of $y$'s such that $$ f(y)< f(x_{\alpha})-\epsilon d(x_{\alpha},y) $$ is not empty: let $x_{\alpha+1}$ be any of these $y$'s. Thus in particular we have $$ \epsilon d(x_\alpha,x_{\alpha+1})<f(x_{\alpha})-f(x_{\alpha+1}).\qquad (1) $$ If $\alpha\in\Omega$ is a limit ordinal we define $$ x_\alpha:=\lim_{\beta\uparrow\alpha}x_\beta. $$ We need to show that this is a good definition, i.e. that the limit exists. Let's examine the case $\alpha=\omega$ at first. Adding up (1) over $\alpha\in\mathbb N$ we see that $$ \epsilon\sum_{n\in\mathbb N} d(x_n,x_{n+1})\leq f(x_0)<\infty $$ and this forces the sequence $(x_n)$ to be Cauchy, so that (since $(X,d)$ is assumed to be complete) $x_\omega$ is well defined. For general limit ordinals $\alpha$ the argument is the same: one has to observe that (1) and transfinite induction show that for $\beta\leq \beta'<\alpha$ it holds $$ \epsilon d(x_\beta,x_{\beta'})<f(x_{\beta})-f(x_{\beta'}) $$ so that one can conclude that the limit of $x_\beta$ exists arguing as before and, for instance, using the fact that any countable ordinal is the limit of an increasing sequence of smaller ordinals.
Hence $x_\alpha$ is now defined for every $\alpha<\Omega$. Let us now look at the map $\alpha\to f(x_\alpha)$. By construction this map is non-increasing: this is trivial for successor ordinals, for limit ones we use the (semi)continuity of $f$. But any monotone map from $\Omega$ to $\mathbb R$ must be eventually constant: in our notation this follows by noticing that the open sets $(f(x_{\alpha}),f(x_{\alpha+1}))$ are all disjoint and thus only a countable number of them can be non-empty.
Hence $\alpha\to f(x_\alpha)$ must be eventually constant and in particular for some $\alpha$ we must have $f(x_\alpha)=f(x_{\alpha+1})$. However, by construction this means that $x_\alpha$ satisfies the conclusion of the theorem, because otherwise (1) forces $f(x_{\alpha+1})<f(x_\alpha)$. Thus the proof is achieved.
Notice that albeit the $x_\alpha$'s are defined over all $\Omega$, in fact only a countable number of choices have been made, because the function $\alpha\to f(x_\alpha)$ is eventually constant.
I would like to know:
a) is this argument using the standard axiom of dependent choice, a different form of countable dependent choice or some uncountable version of it?
b) is the `choice axiom' used in the proof compatible with the measurability of all the subsets of the reals?
Perhaps I should mention that Ekeland's proof of the above theorem relies on the standard dependent choice. The idea is that instead of randomly picking $x_{n+1}$, one chooses one which makes a `sufficiently big step', here is Ekeland's proof:
Pick $x_0\in X$ as above and for given $x_n$ define the closed set $S_n\subset X$ as $$ S_n:=\{y\ : \ f(y)\leq f(x_n)-\epsilon d(x_n,y)\}. $$ Then pick $x_{n+1}\in S_n$ such that $$ f(x_n)-f(x_{n+1})\geq\frac12\big(f(x_n)-\inf_{y\in S_n}f(y)\big)\qquad (2) $$ Then the same arguments previously used ensure that $(x_n)$ is a Cauchy sequence while from the requirement (2) it is easy to see that the limit point fulfills the requirements.
The 'problem' that I have with this argument is that it is `more complicated' (of course this is highly debatable) because it needs the idea of forcing the choice as in (2), rather than simply saying 'if I'm not arrived, I move on'. Beside this particular case, I've found myself using the argument involving ordinals even in situations where I would not know what is the analogue of (2), in particular because there appears to be no function to be almost-minimized. Thus I would like to understand which form of choice I'm using and its relation with other axioms typically related with countable forms of choice.