[FOM] "Mathematician in the street" on AC

[Vaughan Pratt]

After giving more thought to the various responses to my post about 
countable unions, and following up on a suggestion made in private 
correspondence by Andrej Bauer that surjections work better than 
injections when aiming for more constructive results about countability, 
I came up with the following formulation of countable unions as a 
candidate explanation of why "working mathematicians" are surprised to 
learn that any form of choice is involved in the result.  (I dropped in 
on Tim Roughgarden this afternoon, an algorithmic game theorist whose 
office is down the corridor from mine, and his instant reaction was 
surprise that the theorem was not an utterly trivial fact readily proved 
in ZF.)

The following formulation is certainly not the only one, witness my 
previous proposal, but I rather like this one and would be interested to 
see where it ends up in the eventual ranking if and when other 
candidates emerge.

To avoid any misunderstanding let me emphasize that my concern is not 
with the absence of "The countable union of countable sets is countable" 
from ZF, but rather with whether that statement of the proposition is 
what "working mathematicians" like Tim have in mind when they express 
their surprise at its unprovability in ZF.

Since no one has complained about the term "counted set" as the name for 
a pair (X,f) where f: X --> N is an injection, let's stick with that 
nomenclature for injections to N, and adopt "enumeration" as the term 
more appropriate to surjections from N, the approach to countability 
advocated by Andrej.

Writing X+ for X U {X}, and N for the natural numbers as usual, define 
an *enumeration over* X (in contrast to an enumeration *of* X) to be 
*any* function

     f: N --> X+.

This can also be viewed as a partial function N --> X, but the advantage 
of organizing it as a total function to X+ (Andrej wrote 1+X, the 
preferred form in category theory) will become apparent momentarily.

Call im(f) \intersect X the subset of X *enumerated by* f.  The idea is 
that X itself will not in general be countable (to fix the idea take X 
to be the set of reals); rather, the subset enumerated by f, consisting 
of those values other than X itself taken on by f(i) as i ranges over N, 
*is* countable, witnessed by the enumeration of its elements (which may 
contain repetitions).  This captures the intuition of a box enumerating 
some of the elements of X, possibly with repetitions, and possibly with 
pauses represented by X itself as the output when the box temporarily 
(or even permanently) has no member of X to output.  Computer scientists 
like Andrej and Tim who've studied and taught recursively/computably 
enumerable sets for years have this sort of intuition about enumeration 
deeply embedded in their psyches.

Define an enumeration of enumerations over X to be a function

     g': N --> (N --> X+)

Take this to be the "left transpose" of the function

     g: NxN --> X+

defined by g(i,j) = g'(i)(j).  (The right transpose reverses i and j, 
and is equally natural but arguably less canonical.)  This *includes* 
the case where g'(i) is the empty function, meaning the function which 
is X at all values of i, justifying calling g' an "enumeration of 
enumerations" if we identify the constantly X function with the value X.

Now given any surjection h: N --> NxN (e.g Cantor's bijection but any 
surjection will do), gh is an enumeration over X having the obvious 
property that the subset of X that it enumerates is the union over all i 
in N of the subset of X enumerated by g'(i).  Equally obviously (to 
people like Andrej and Tim at least), every countable union of countable 
subsets of X *arises* in this way (after making the requisite choices, 
this being the meaning of "arises" and also the obstacle when attempting 
to prove that statement of the theorem directly in ZF), and is therefore 
countable.

We then have a natural map from surjections N --> NxN to enumerations 
over X constructively witnessing the theorem that the countable union of 
countable sets is countable.  The theorem is completed in a 
non-canonical way by exhibiting any surjection from N to NxN.  Those 
having a preferred such surjection they like to think of as canonical 
can consider the proof itself canonical, the rest can be satisfied that 
at least the map is natural.

If moreover one tries for a technical definition of "natural" in terms 
of naturality in the variable X, any fixed choice of surjection h: N --> 
NxN will presumably not interact with X, in which case gh itself will be 
natural for any fixed choice of h.

On the principle that if anyone is going to be bothered by this it will 
be one's harshest critic, I should begin by asking Arnon whether this 
formulation is sufficiently well-defined by his standards, and if not 
what if anything can be done about its remaining shortcomings.

Vaughan