FOM: "The unreasonable effectiveness of mathematics"

[Martin Davis]

At 07:26 PM 1/25/98 -0800, Solomon Feferman wrote:

>As I explained in an earlier posting, that reported the result of work
>showing that a certain formal system of variable types conservative over
>Peano Arithmetic serves apparently to formalize all (thus far accepted)
>scientifically applicable mathematics (18 Nov, 23:51).  So the
>indispensability of that mathematics to science can't be counted as an
>argument for the real numbers somehow being embedded in the world.

I've thought about this. It seems to me is that what this very interesting
conservative extension result really shows is that the kind of analysis
useful in science (I assume this means things like ODE, PDE, elemntary
functional analysis, conformal mapping, coplex variable thoery, and such)
will not suffice to prove any statements of number theory not already
derivable in PA. This, despite G\"odel's proof that there are arithmetic
sentences undecidable in PA that become decidable when higher type objects
are permitted. But I don't see what this implies about statements of
analysis itself (as for example those useful for science), provable in this
system. Statements about "real numbers" provable in this system still
mention and use real numbers.

Am I missing something?

Martin