[FOM] finite choice question

Andrej Bauer Andrej.Bauer at andrej.com
Thu Nov 17 15:56:15 EST 2005

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

More information about the FOM mailing list