FOM: report from expert

[Martin Schlottmann]

JoeShipman at aol.com wrote:
> 
[...]
> 
> 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

Such a metatheorem would require a coherent
axiomatization of category theory. There has
been a discussion of this question on the
fom list some months ago, but nobody was willing
or able to provide an axiom system which included
not only just the algebraic properties of topoi
(maybe with some additional structures) but also
a sufficient set of assumptions of existence.

-- 
Martin Schlottmann <martin_schlottmann at math.ualberta.ca>
Sessional Lecturer
Department of Mathematical Sciences, CAB 583
University of Alberta, Edmonton AB T6G 2G1, Canada