[FOM] 622: Adventures in Formalization 6

[Hendrik Boom]

On Tue, Oct 27, 2015 at 02:55:07PM -0700, Mitchell Spector wrote:
> With regard to the discussion as to whether the set of natural
> numbers should be a subset of the set of real numbers, or whether
> it's good enough to have an isomorphism that lets us identify
> natural numbers with certain real numbers:
> 
> It may worth pointing out that Conway's surreal numbers provide a
> systematic approach which includes both the natural numbers and the
> real numbers, and which makes N a subset of R.

And those Conway numbers also contain the ordinals, and the 
nonnegative integers are a subset of those, too.  So one unifirmly 
defined system defines everything from reals and ordinals, even 
providing a meaning for dividing omega minus one by pi.

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

-- hendrik