FOM: report from expert

[JoeShipman@aol.com]

I am glad to hear that Wiles's proof didn't use Universes and that therefore 
FLT is true.

I am even gladder to hear that number theorists would accept a proof from 
Universes as valid, even though they would try to remove the assumption, 
because it shows a belief in a small large cardinal axiom (or at least in its 
consistency), and indicates that should Harvey establish some good number 
theorems from larger cardinals there is a reasonable chance for those axioms 
to become accepted also, vindicating Godel's philosophical views.

Of course, those views would already have been vindicated if anything of 
significance had been proven from the Universes assumption where the 
assumption had not been shown removable.  But I don't know of any such 
theorems.

Therefore I repeat my earlier query: has any theorem of "ordinary 
mathematics" (defined here as a statement about sets contained in some 
iterated powerset of the integers that does not obviously imply Con(ZF)) ever 
been proven using Grothendieck's Universe assumption in a way that is not 
straightforwardly removable?  If the answer is no, then why does anyone 
bother with Grothendieck Universes?  If they're really as useful for thinking 
about mathematics as McLarty implies but they can ALWAYS be removed for the 
types of theorem they are used to prove (obviously they can't be removed from 
any proof of Con(ZF)), then someone really ought to try to eliminate the 
assumption once and for all with an appropriate metatheorem.

-- Joe Shipman