FOM: why formal power series do not work

[Vaughan R. Pratt]

>From: kanovei at wminf2.math.uni-wuppertal.de
>Try to define 2^z for the z being x^{-1}. 

I only claimed to have produced an ordered field (which is necessarily
Archimedean, whence my disagreement with Martin's diagnosis).  2^z is
not a field operation.

On the other hand Robinson's construction is robust with respect to
such extensions beyond the rational operations.  So the "bug" I was
presuming must exist in my construction seems to be more a question of
scope of "theory of the reals" than a bug in what I claimed.  If you
are just talking about "the" first-order theory of the reals in the
sense of the rational operations (and Martin said nothing to suggest
otherwise), then I (still) don't see any problem with my proposal.

The crucial point here would seem to be that Robinson's technique works
for richer languages with elementary functions like sin, exp, and log.
I.e. I agree with Vladimir's diagnosis.

This is a point I would probably never have gleaned just from the
literature if I had not gone through this exercise.

What Conway's numbers do that the power series I suggested don't is in
effect to extend the exponents of x in the power series transfinitely
in both directions, and so on recursively, giving much stronger closure
properties on his number system that assure definedness of many more
functions than just the rationals.  (One way to make this connection is
to realize that Conway's "short" numbers are just finite binary
notation, and that those beyond day \omega bring in bit positions at
\omega and -\omega and beyond, creating a disconnect of the same
general kind as encountered with formal power series.)

As a metacomment it seems to me valuable to progress more gently via
systems of intermediate strength, the better to appreciate exactly what
is sufficient and what is necessary about the various constructions
catering to the various languages.  That formal power series equip
ordered fields with infinitesimals in an easy way seems like an
excellent such intermediate system, especially given that it is quite
elementary.

It also gives additional perspective on Jon Barwise's request for a
canonical system.  If you specify the language in advance, it makes
sense to ask what the prospects are for finding a canonical system; the
richer the language presumably the poorer the prospects.  But if you
leave it open-ended, the prospects are zero and his request becomes
unreasonable.

Vaughan