Re: What does it take to identify the field and the continuum of reals?

[Martin Escardo <m.escardo@cs.bham.ac.uk>]

Vaughan Pratt writes:
 > I would bounce this question back to Martin: what did he mean by "th=
e
 > Dedekind reals" in his attribution to Freyd?

I meant (and still mean): the underlying object of the final coalgebra
is what topos theorists know as "the object of Dedekind reals" (in an
elementary topos with nno).

In more detail [Freyd & Johnstone, in Johnstone's Elephant, pages
1028-1032]: given a topos with nno, consider the category of
(internal) posets in the topos. In this category, define a
functor. Consider its final coalgebra. Theorem: (1) It exists. (2)
Moreover, the underlying object of the algebra is the Dedekind unit
interval under its natural order. (3) The structure map performs
average (x,y) |-> (x+y)/2 (for full details, see the reference).

Answering the question quoted below, you get all the ingredients you
are looking for: a *set* of numbers (as the underlying set of the
underlying poset of the final coalgebra), its *order* (as the
underlying object of the final coalgebra), and (part of) its
*algebraic* structure (as the structure map of the final
coalgebra). Of course, here "set" means an object of a topos,
e.g. that of classical sets. You get only part of the *algebraic*
structure, but topos logic is strong enough to allow you to fully recov=
er=20
it after you have the final coalgebra in your hands.=20

The Escardo-Simpson approach is similar, but takes a different route
and makes weaker assumptions - I won't repeat the story, which can
be found in the paper whose reference was already given by Alex
Simpson.

Martin Escardo