[FOM] "Mathematician in the street" on AC

[Vaughan Pratt]

Timothy Y. Chow wrote:
> Vaughan Pratt <pratt at cs.stanford.edu> wrote:
>> Define a countable set to be a pair (X,f) consisting of a set X and an 
>> injection f: X --> N.
> 
> This certainly circumvents the use of AC, but I submit that it is somewhat 
> contrary to the mathematical practice of *not* equipping structures with 
> non-canonical stuff that is extraneous to their essence.  You could define 
> a vector space as something that comes equipped with a basis, or a 
> manifold as something that comes equipped with an embedding in R^n, or a 
> group as something that comes equipped with a homomorphism to an 
> automorphism group of something, etc.

Indeed, and Thomas Forster agreed with you on that point.  However there 
is a crucial difference that makes the analogy inapplicable.  As I 
remarked in passing in my previous post (too briefly in hindsight), it 
is a *theorem* that a vector space has a basis.  As far as the 
definition goes, a vector space is equipped with a specific algebraic 
structure, with no existential quantifier in sight in its definition. 
Were it not so I very much doubt whether vector spaces would have become 
so universally accepted.  The absence of existential quantifiers in its 
definition makes a vector space more like a counted set than a countable 
set.

> But experience has shown that there 
> are great conceptual advantages to *not* saddling our mathematical objects 
> with extrinsic structure.  Instead we wait until we need the explicit 
> basis or embedding or representation, and introduce it at that point.

This sounds more like a cultural thing than anything intrinsic to 
mathematics per se.  Our respective points of view may be the biggest 
difference between logicians and algebraists (I made the L-->A 
transition myself rather abruptly around 1980 while struggling with 
completeness of Krister Segerberg's axiomatization of Propositional 
Dynamic Logic and finding myself bogged down by details that the 
algebraic viewpoint neatly eliminated).  Where the logician is 
comfortable merely asserting existence of an entity meeting some 
condition, the algebraist looks for an operation that actually produces 
a specific such entity.  Counted sets should appeal to algebraists as 
much as countable sets do to logicians, witness monoidal categories 
which definitely *don't* say merely that there exists a monoidal 
structure despite the strong temptation to do so, one could never 
complete the definition understandably if they did.

> Specifically, in the case of counted sets, a counted union of counted sets 
> isn't *canonically* counted.

That's a very good point, and one that I'd overlooked.  The weak link I 
see in my proof (you may see others as well though I think I can argue 
against most or all of them) is the choice of injection from N^2 to N. 
The symmetry of N^2 that interchanges (i,j) with (j,i) gives a lower 
bound of 2 on the number of equally natural countings.  (For an upper 
bound of 2 one might try to argue that there's something canonical about 
Cantor's bijection of N^2 with N, but that may be a bit of a stretch.)

So for the sake of a theorem in Z as opposed to ZFC, I guess the theorem 
has to be that a counted union of counted sets is merely countable.  The 
existence of an injection from N^2 to N certainly is in Z (Zermelo, not 
the integers), the problem is to defend any given choice of one.  At the 
very least one must break the symmetry of 2, e.g. by taking 2 = 0<1 
instead of 1+1 and then somehow breaking the symmetry between g and h in 
the product gxh: UxU --> NxN at the other end to match.  The latter is 
easier given that the definition of h as h(x) = f_{g(x)}(x) depended on 
that of g.  Hardly the intuitive notion of "canonical" though.

------------

Let me piggy-back a quick reply to Arnon Avron here, whose objection 
seemed to be that the union (X_0,f_0) U (X_1,f_1) was an undefined 
concept.  That's like objecting that an int i can't be added to a float 
x without writing it as (float)i + x, or that a homomorphism h: G --> G' 
can't be understood as a function U(h): U(G) --> U(G') without writing 
it as U(h).  If it's not clear what coercions suffice to turn my proof 
into a completely formal argument entirely within ZF (in fact Z) we 
should probably take this offline unless there are others stuck on this 
point.

Vaughan