[FOM] "Mathematician in the street" on AC
Vaughan Pratt
pratt at cs.stanford.edu
Thu Aug 20 00:43:34 EDT 2009
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
More information about the FOM
mailing list