[FOM] The Gold Standard/correction

[Timothy Y. Chow]

Harvey Friedman <friedman at math.ohio-state.edu> wrote:
> This assessment is based on the premise that Grothendieck universes are 
> to be properly viewed as a superfluous aberration. If not, then probably 
> NBG + AxC would be the preferred vehicle, under the no coding rule.

This discussion reminds me of something that I again vaguely recall having 
been discussed on FOM before, but this time I've actually gone to the 
trouble of trying to search the archive and have not found anything.  I 
refer to a sci.math.research article by Vidhyanath Rao.

http://groups.google.com/group/sci.math.research/msg/a9279fa4411aaab3

This seems to be another example of core mathematics that is not obviously 
formalizable in (a conservative extension of) ZFC.  Unless there have been 
new developments since Nath Rao posted this?

Tim