[FOM] Adequacy of FOL+ZFC as foundation

[joeshipman@aol.com]

On an earlier thread, I mentioned two ways that first-order logic with 
the ZFC axioms is problematic as a foundation:

1) Grothendieck Universes are necessary for the convenient development 
of some modern number-theoretic results

2) NF is not consistent with ZFC so far as we know.

McLarty's paper on Wiles's theorem suggests that a metatheorem is 
possible which would eliminate the need for Grothendieck Universes, 
although he does not state one. (I can state one, that you don't need 
Grothendieck's axiom of a proper class of inaccessibles -- a single 
inaccessible limit of inaccessibles suffices for any application to 
number theory or indeed for any "Absolute" statements.)

No one responded to my request for examples of mathematics done in NF 
as a base theory that were not obviously reinterpretable as arguments 
from ZFC.

Therefore my two examples do not appear to lead to statements which are 
generally regarded as having been proven, but which cannot be seen to 
be theorems of ZFC.

Can anyone suggest another example that might show the inadequacy of 
FOL+ZFC?  I would like to exclude statements that require large 
cardinals, because I can regard them as simply being ZFC theorems about 
the statement following from a large cardinal.

-- JS