[FOM] 622: Adventures in Formalization 6

[John Baldwin]

On Wed, Oct 28, 2015 at 7:59 AM, Freek Wiedijk <freek at cs.ru.nl> wrote:

> Dear Hendrik,
>
> >So one unifirmly defined system defines everything from
> >reals and ordinals, even providing a meaning for dividing
> >omega minus one by pi.
>
> I think the Conway numbers don't work well with
> exponentiation?  You cannot take the omega-logarithm in a
> way that omega-exponentiation gives you back your original
> number?
>
>
>
This is incorrect. Ehrlich and Van den Dries showed the exponential ordered
field of surreal numbers is an elementary extension of the
 exponential ordered field of real numbers.

Fundamenta Mathematica 2001 Fields of Surreal numbers and exponentiation
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20151028/23a0db26/attachment.html>