[FOM] Countable choice

[Kenny Easwaran]

As I recall, in the literature working with the Axiom of Determinacy,
at least some form of countable choice is generally assumed as well.
I seem to recall that AD actually proves some form of countable
choice, but I don't remember if that's actually true.  At any rate,
many of the claims that are said to follow from Determinacy require
countable choice as well.  So that literature may have some more
that's of use.

Kenny

On Wed, Jun 11, 2008 at 1:19 AM, Andrej Bauer <Andrej.Bauer at andrej.com> wrote:
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>