Re: Fixing the constructive continued-fraction definition of the reals: proofs and refutations

[Vaughan Pratt <pratt@cs.stanford.edu>]

Toby Kenney wrote:
> I think the following is a better proof:

Toby, thanks for that.  Peter J. suggested a proof in a separate email
to me, let me absorb and compare them.

> Your suggestion of relaxing the condition to ts <= t seems to require
> changing from ordinary objects to partially-ordered objects. I think the
> initial one should be just the free monoid on two generators, with some
> partial order. You probably want to insist that s and t be inflationary.

Quite right, I forgot to specify that s and t were monotone (which
implies inflationary), and I also left out that 0 is the empty sup. 
(According to J&M in "Algebraic Set Theory" 1995, specifying 
inflationary rather than monotone for the class as a whole gives the 
hereditarily transitive sets, i.e. the von Neumann ordinals.  Monotone 
gives a larger class and a weaker notion of ordinal which nonetheless is 
inflationary as a consequence of monotonicity and initiality.)

> If you´re considering partially-ordered objects, then this won´t be
> isomorphic to N^2. I´m not sure whether there will be any isomorphism in
> the topos, even without requiring it to preserve order. You could
> alternatively consider a condition like t=sts. I´m not really sure what
> you mean by your claim that t is the ordinal w - I think the object you
> describe isn´t even totally ordered - how can you compare t^2(s(0)) and
> t^2(0)? If you take a condition like t=sts to make it totally ordered, you
> still have a decreasing chain t > ts > ts^2 > ...

The conditions I forgot to mention, 0 <= x and t monotone, should give 
t^2(0) <= t^2(s(0)).

> It looks like this should be something like the interval in N x Z,
> lexicographically ordered, going from (0,0) (so without the pairs (0,-n)).
> If this is still an attempt to construct the reals, then I don´t see any
> sensible way to describe addition on an infinite lexicographic product of
> copies of Z (the integers).

If both coordinates still have complemented subobjects, in particular if 
{0} x w and w x {0} are both complemented subobjects, then I should 
throw in the towel, consistent with Peter's advice.  Are they?  If w x 
{0} is not a complemented subobject then we're moving in the right 
direction: the next step is to define a suitable final coalgebra.

Vaughan