[FOM] "Mathematician in the street" on AC

[Vaughan Pratt]

Aha, the "counted" terminology is just what I wanted, thanks Thomas. 
Too bad it's not in wider use.  What's a citation for the term that no 
Wikipedia editor would complain about, in case it seems worth mentioning 
in the article on countable sets?

There are many analogous situations where everyone is in agreement that 
this sort of distinction makes a difference.  One familiar example is 
the distinction between R^n and an n-dimensional vector space over the 
reals for finite n.  It is a theorem of ZF that a basis exists for the 
latter, whereas the former amounts to the same thing (up to isomorphism) 
but equipped with a specific basis, which determines an inner product 
and hence notions of angle and length.  In consequence one can define 
"n-dimensional Euclidean space" as R^n but not as an n-dimensional 
vector space over R.

An example that gives computability students grief is the distinction 
between a program for computing a partial recursive function and the 
partial recursive function it computes.  The latter is defined as one 
for which a program exists.  The confusion arises when one writes phi_x 
to denote a partial recursive function; the student then has to 
determine from context exactly who has access to the index x: the 
program, the student, the instructor, an oracle...  If the student is 
still struggling with this when confronted with the recursion theorem, 
that every partial recursive function can be implemented in a way that 
gives it access to its own index, the theorem may seem either vacuously 
true, meaningless, false, or (the intended impression) miraculous.

Yet another example is the category of sets and functions as usually 
understood.  This is cartesian closed, and bountifully so, namely in a 
proper class of ways, but no one would want to appeal to its being so 
closed in practice without first fixing a specific tensor product 
(invariably cartesian product) and right adjoint A=>B thereof 
(invariably the set of functions from A to B).  More generally one 
assumes coherence conditions that avoid the sort of craziness that 
results from relying on uncorrelated existentials.

If "counted" were to become a generally recognized notion, the natural 
theorem in ZF would be "Every counted union of counted sets is counted." 
  It is natural in the sense that it surely formalizes the intuitions of 
those who consider it pretty much as obvious as the countability of N^2.

The version that is independent of ZF would be the less obvious variant, 
"Every counted union of countable sets is countable" when defining 
countable union as an omega-ary operation, and "Every countable union of 
countable sets is countable" when defining countable union as a unary 
operation mapping P^w(P^w(X)) to PX (where P^w(X) denotes the set of 
countable subsets of X, and with the theorem being nonvacuous in this 
last case only for uncountable X since P^w(X) = P(X) when X is countable).

Unfortunately when the only thing that's at stake is dependence on 
something even weaker than AC, junior faculty just coming up for tenure 
aren't likely to take that sort of subtlety terribly seriously.

Part of the problem here is that AC itself is too abstract to be 
concretely meaningful to most "working mathematicians," and therefore 
not something they feel comfortable passing value judgments on. 
Accepting AC as true has something of the flavor of Pascal's Wager: if 
AC is true then so are the theorems that appeal to it, but if AC is 
neither true nor false then no harm has been done.  (In making his wager 
Pascal seems not to have reckoned with the possibility of an Antigod who 
would consign him to eternal torment for worshipping God, the 
counterpart of AC being false.  Goedel showed that AC can't be false, 
but who convinced Pascal that there is no Antigod?)

If I wanted to motivate someone to draw the distinction between a 
countable set and a counted set, I would instead point out to them that 
the former notion when applied to countably infinite sets entails 
quantifying over uncountably many functions.  I would then ask them 
whether they were comfortable with the notion of countability depending 
on quantifying over a domain that not only was uncountable but that 
contained insane functions that, relative to each other, were wildly 
intractable, going all the way up the arithmetic hierarchy and far 
beyond.  When put that concretely they might think twice about it.

But I would also ask them whether they thought Erdos would judge their 
non-ZF proof (of the countability of countable unions of countable sets) 
as "straight from The Book."  This is not to imply that The Book must 
outlaw every non-theorem of ZF ("every vector space is free" being a 
great candidate), only those which can be moved into ZF by a better 
choice of definition of some concept without losing their basic import.

Vaughan Pratt

Thomas Forster wrote:
> Dear Vaughan,
 >   Thank you for this nice exposition.  The notion you are using is
> the one that Conway coined the phrase *counted set* for.  However, i 
> think you are being far too charitable in your description of normal 
> mathematical practice.  I think you are crediting these good people 
> with using the notion of counted set *consistently* (in which case, 
> as you observe, no AC is needed).  Sadly what i think is going on is 
> that the mathematician-in-the-trailer-park is engaged in a fallacy of 
> equivocation between the two notions.  Worse, they do not take kindly 
> to having this equivocation pointed out to them.