[FOM] Is there a "naturally occurring" theorem provable in EFA but not in predicative arithmetic?

[Rupert McCallum]

My friend Norman Wildberger thinks there is a part of mathematical
reasoning which is self-evident and doesn't need to be analyzed by the
axiomatic method. I want to cast doubt on this belief of his by giving
him an example of a "naturally occurring" theorem, of the kind
mainstream mathematicians would be interested in, which can be proved
in EFA but not in predicative arithmetic as developed in Edward
Nelson's book "Predicative Arithmetic". Of course one example is
"exponentiation is total", but that is not the sort of theorem which
would be of interest to a mainstream mathematician.


 
____________________________________________________________________________________
Access over 1 million songs - Yahoo! Music Unlimited 
(http://music.yahoo.com/unlimited)