[FOM] shipman's challenge: the best defense

[joeshipman@aol.com]

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"?

Or do you think that all such renderings of the statement in the 
language of set theory fail to formalize "the set of real numbers is 
uncountable" sufficiently faithfully for a ZFC-proof of the 
set-theoretic sentence to settle the question of whether the real 
numbers are uncountable?

If the latter, do you think that any other formal system could 
accomplish what ZFC doesn't here?

-- JS


-----Original Message-----
From: Gabriel Stolzenberg <gstolzen at math.bu.edu>


   Having said this, I invite Joe to think about the "adequacy" of
a formalization of the informal statement, "The set of real numbers
is uncountable."  The claim that it is a "faithful representation"
of the informal statement might well make a mathematician (e.g., me)
uncomfortable.  I believe this is a familiar point.

________________________________________________________________________
More new features than ever.  Check out the new AOL Mail ! - 
http://webmail.aol.com