[FOM] FOM Digest, Vol 59, Issue 18

[David Ross]

S. S. Kutateladze wrote:

> Since nonstandard analysis is conservative over the "standard"
analysis and the "great"
> conjecture is stated in standard terms, any nonstandard proof of the
conjecture will
> be immediately  translated into the standard language (there is a
> formal algorithm  by Nelson to this end).

This does not work for all proofs done using nonstandard analysis, in
particular any that use in an essential way the interplay between
internal and external entities.  For example, there is no such
translation of Hirshfeld's proof of Ramsey's Theorem, or the van den
Dries/Wilkie proof of Gromov's Theorem.

> The power nonstandard
> analysis lies far from the fact that nonstandard analysis allows one
to use
> infinitesimals in inventing new proofs of standard theorems.

The fact that NSA has been used to discover and prove new standard
theorems is certainly evidence of its utility, aside from the
foundational achievement of resurrecting infinitesimal arguments.  The
fact that some of the theorems for which it provided the first proofs
were not as strong as they might have been, is not an indictment of the
methodology.

David Ross