[FOM] 622: Adventures in Formalization 6

[Freek Wiedijk]

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?

>Anyone know whether the addition he defines matches the
>usual one on ordinals?

The Conway addition is commutative.

Freek