# [FOM] "Mathematician in the street" on AC

Vaughan Pratt pratt at cs.stanford.edu
Wed Aug 19 01:16:04 EDT 2009

```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
> 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
```