[FOM] Countable choice

[Andrej Bauer]

Thomas Forster wrote:
> I have a feeling that there is a literature on the idea that
> countable choice is not just a weak form of full choice, but
> is somehow a fundamentally different principle: there might
> be good reasons for adopting AC_\omega that aren't special
> cases of arguments for adopting AC.   Can anyone give me
> any pointers to it..?

In Bishop-style constructive mathematics Countable Choice (and Dependent
Choice) are accepted. I don't have Troelstra and van Dalen's
"Constructivity of mathematics" with me right now, but I would expect to
see there a discussion about why constructive mathematics finds AC_omega
acceptable (in volume 1). Another place to look might be Beeson's book,
which I also do not have with me right now.

In general, constructive mathematicians like to discuss acceptance and
rejection of various choice principles. For them this is not a skeleton
in the closet.

There is (at least one) computational interpretation of the axiom of
choice which tells us that AC_omega is ok because natural numbers have
canonical forms. Namely, the choice principle AC(X,Y), which says that,
for any relation R on X x Y,

  (forall x : X, exists y : Y, R(x,y)) ->
    exists f : X -> Y, forall x : X, R(x,f x)

is validated by a construction which takes an _intensional_ operation p
of type X -> Y (which takes x and computes y such that R(x,y)), and
returns an _extensional_ choice function f : X -> Y. How can we turn an
intensional p to an extensional f? One possibility is to precompose p
with a function that computes canonical forms. In particular, we would
expect this to be the case for natural numbers, X = N: before applying p
to a number, we put the number in canonical form (a numeral).

Similarly, Brouwerian intuitionisim accepts AC(N^N, X) where N^N is the
space of all sequences of numbers. This view can be accepted if we think
that every sequence can be put in canonical form, i.e., that there is
nothing more to a sequence other than the progression of its values

   a_0, a_1, a_2, ...

(In Brouwerian intuitionism there are further stipulations involving
what we can learn about such sequences. These lead to a continuity
principle.)

In contrast, Russian constructivism does not accept AC(N^N, X) because
there a sequence is given by a Turing machine that computes it. There is
no canonical choice of such Turing machines, which is proved by an easy
diagonalization.

I think even classically we can appreciate the distinction between
having and not having canonical forms as basis for acceptance of AC.

Best regards,

Andrej