[FOM] 622: Adventures in Formalization 6

Freek Wiedijk freek at cs.ru.nl
Wed Oct 28 08:59:00 EDT 2015

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

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

The Conway addition is commutative.


More information about the FOM mailing list