[FOM] "Mathematician in the street" on AC

[Arnon Avron]

Quoting "Vaughan Pratt" <pratt at cs.stanford.edu>:

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

No, Vaughan. This was only a side point. My main point was
clealy repeated at the end of my posting. It was that you
yourself said in your original message that N^2 is countable
(not that (N^2,f) is countable for some f you choose) and
you talked about the countable set of pairs (x_i,f_i),
and this is not a countable set according the definition
you gave in your first posting on the subject.

To repeat: twice in your own posting you refer to countability
as a *property of a set*, and (at least so it seemed to me)
you were using the ordinary definition: that a set X is
countable iff there exists an injection from X to  N.

As for the question itself: of course you can formulate a constructive 
version of the theorem that is indeed  provable in ZF. It would be 
something like:

 If X and F are functions defined on N
 such that for every i:N, F(i) is an injection from
 X(i) to N (or a surjection of N on X(i), if so
 you now prefer) than the union of {X(i)|i:N} is countable.

(Indeed, in most cases in which the theorem about the countability
of the countable union of countable sets is applied in practice,
We have such X and F available, so we do not have to use AC).

But for formulating and proving the above version
we do not have to redefine the notion of
a countable set which *every mathematician* takes as a
property of a set (not of an order pair of that set and a function
from it to N...) - and this includes you (as I have shown in my
previous message).

As for the question why some mathematiciams do not always notice
when AC is used in a proof -  the answer is that the language
mathematicians use in proofs is not always precise enough,
and sometimes causes mistakes. In particular: mathematicians
tend to replace the use of existential statements
by the introduction of skolem functions. This is such a common
procedure that they do not even notice that they are
using AC when they do so. Thus a "proof" of the theorem
under discussion usually goes like this: "Let X_i be countable
for every i:N. This means that for each i there is an injective
function f_i:X_i->N..." and then they use the f_i's, not noticing
that they are relying  here on the existence of a skolem function f with
domain N such that f(i) is some injection from X_i to N
(writing f_i rather than f(i) also helps to hide that!).

Here it might be good to recall that AC was implicitly used in this way by
mathematicians long before it was formulated and its
role was realized - and some of these mathematicians
have even strongly rejected AC (being unaware at
the beginning that they had been using the principle
to which they objected...)

Arnon




----- End forwarded message -----