[FOM] analysis with hyperreals vs. surreals?

[Ben Crowell]

Steven Obua wrote:

>Could you point out where in Conway's book this comparison of surreals
>and hyperreals happens?
In the 1976 edition, it's on p. 44, at the end of ch. 4.

>In the mechanical proof-assistant Isabelle both the hyperreals and
>partizan games (the stuff out of which surreals are made) have been
>formalized, and I would like  to formalize the connection between them,
>if there is any. Unfortunately I don't know the connection, can someone
>provide links?

The construction used to build the surreals can also be used to
construct R by stopping the machine at a certain point, but I don't
know if the same idea works for *R. The surreal approach and the
hyperreal approach seem more similar to each other than they do to
smooth infinitesimal analysis, which uses nonaristotelian logic, and
has models without any invertible infinitesimals. One big difference
between the hyperreals and the surreals is that the hyperreals have a
transfer principle that applies to first-order logic, and can even be
extended beyond first-order logic to statements about internal sets
and functions.

It seems like it ought to be possible to map the hyperreals
homomorphically into some subset of the surreals, but it's not
obvious to me how to do it. The axiomatic treatment of the hyperreals
merely assumes the existence of at least one infinite number H, which
could be mapped to some infinite surreal. But it's not obvious to me
what you'd do after that, because the hyperreals aren't explicitly
constructed from H in the same way that, say, the complex numbers are
explicitly constructed from i.