[FOM] finite choice question

[Andrej Bauer]

On a related note, I wondered once about the following forms of "finite"
countable choice. Let N = {0,1,2,...} be the natural numbers and
f:N-->N. Consider the choice principle AC(N,f): for every relation R on
N x N,

   (forall n in N. exists m < f(n). R(n, m)) ==>
      (exists c : N --> N. forall n in N. R(n, c(n))

So this is like countable choice, except that the totality of relation R
is majorized by f.

When does AC(N,f) entail AC(N,g)? In particular, do we have, for a fixed
k > 2, any of the implications:

   AC(N,lambda n.2) ==> AC(N,lambda n.k) ==> AC(N,lambda n.n)

No choice is allowed in the base theory, of course. Choice has been
beaten to death. Someone probably has worked this out.

Andrej Bauer