FOM: report from expert
JoeShipman@aol.com
JoeShipman at aol.com
Tue Apr 6 21:03:31 EDT 1999
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
More information about the FOM
mailing list