[FOM] reply to shipman: countably uncomfortable

[Gabriel Stolzenberg]

   This is in reply to Joe Shipman's reply of Jan 10 to my message,
"shipman's challenge: the best defense" of Jan 8.  In it, he asks,

> Would you regard any of the standard renderings of "the set of
> real numbers is uncountable" in the language of set theory as
> sufficiently faithful that a formal machine-checkable ZFC-proof
> of it has a claim to be considered as "a proof that the set of
> real numbers is uncountable"?

   1. I was referring to the uncomfortable feeling a mathematician
may get when she realizes that the system in which we prove that
the reals are uncountable is countable.  Yes, we all know the
things that can be said to reassure her but I can't think of any
that would be likely to work.

   2. What does it mean for something to have "a claim to be
considered as something"?

   3.  Also, when you talk about a "rendering" in the language of set
theory, it sounds as if you think that the expression has a meaning
independent of set theory---with respect to which the rendering may
or may not be "sufficiently faithful"---and I can't imagine what that
would be.  As I read you, in this particular context, "faithful" is,
alas, only a junk term.  (This could change but, if it did in the way
I have in mind, we wouldn't be having this discussion.)  And I see no
way to do better.

   Gabriel Stolzenberg