FOM: Formal power series are Archimedean

[Martin Davis]

At 11:11 AM 11/12/97 -0800, Vaughan R. Pratt wrote:
>
>>Non-Archimedean extensions of the reals R were well known long before
>>Robinson. His key contribution was such an extension R* for which the same
>>sentences that are true of R are true of R*.
>
>What's not Archimedean about formal power series?  There is always a
>scaling factor for any nonzero formal power series that will increase
>it beyond any given limit.

Every ordered field of which the reals are a subfield is non-Archimedian.
The very existence of infinitesimal elements defeats the Archimedian property.

>What sentence true of R fails for formal power series over the reals?
>

The language Robinson worked with includes constant symbols for every
function from R to R. Among the sentences are:

sin(x+y)=sinxcosy + cosxsiny
identities involving Bessel functions
and many many others

Martin