FOM: report from expert

[Andrzej Trybulec]

On Tue, 6 Apr 1999 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 

In the Tarski Grothendieck set theory (I prefer this name because Tarski
defined the system in 1938) one can prove the axiom of choice. Is the
axiom of choice a theorem of "ordinary mathematics" ?

Andrzej Trybulec