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

["Toby Kenney" <tkenney@mathstat.dal.ca>]

The proof I gave is not quite ideal - I showed that if the objects 1-4 you
list all exist, then they are isomorphic. In theory, it would still be
possible for object 3, say, not to exist. I think the following is a
better proof:

Let X be an object with morphisms 0 : 1 ----> X, s,t : X ----> X such that
ts=t. We want to construct the map N^2 ----> X. We have a map
f : N ----> X, given by considering X with just 0 and t. For every n in N,
we can also form a map g_n : N ----> X by g_n(0)=t^n(0), and g_n(succ)=s.
Now we can form the map h : N^2 ----> X by h(a,b)=g_a(b). I think this
must be the unique map preserving everything necessary.

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.
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 > ...

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).

On the matter of it being disconcerting finding infinite sups, the
definition doesn´t mention any form of partial order, so it shouldn´t
really be any more surprising than finding (Kuratowski) finite sups.

Sorry this email is mostly just intuition, rather than firm fact.
Hopefully some wiser people than I will be able to put more substance to
it.

Toby

> Toby Kenney wrote:
>> Vaughan Pratt wrote in part:
>>> I could well imagine 1 and 2 turning out to be isomorphic, but I feel I
>>> would get a lot from seeing the proof of whichever way that goes.
>
> Thanks very much, Toby.  I didn't (and still don't) have any intuition
> into what objects and morphisms are present in the free topos with NNO,
> but your proof will help me fill in the gaps in this neighborhood of it.
>
> On the one hand there are lots of objects one can talk about in language
> analogous to that characterizing the NNO, on the other there are also
> lots of morphisms one can talk about that identify those objects (up to
> isomorphism), and I'm still at the very early stage of learning how to
> walk along that ridge line without falling off one side or the other.
>
> Joyal and Moerdijk, Algebraic Set Theory, show how to construct
> sup-semilattices with sups up to a specified size S.   Obviously not
> every topos with NNO supports every S, but presumably S = K
> (Kuratowski-finite) is always present.  Your proof if correct shows that
> ts = t is too strong.  What if I relax it to ts <= t and proceed as in
> J&M to construct the initial such object?  Can you still construct your
> isomorphism, or do we end up with a weaker relationship?  If the latter
> then we should have t(0) >= t(s(0)) = t(1) >= t(2) >= ... >= x for any
> natural number x.  Obviously t(0) is minimal among all terms having at
> least one t, which should make t(0) the ordinal w.
>
> The one disconcerting thing here is that initiality has made t(0) an
> infinite sup even though I assumed only finite sups.  I don't know
> whether this means that the methods of J&M can't construct this initial
> algebra, or that in every topos with NNO one can construct the requisite
> sup-semilattices with countable sups.  I suppose it must be the latter.
>
> (I'm a complete novice here, as I've said before, so I hope people will
> be patient with my appalling ignorance of topos-theoretic techniques.)
>
> Vaughan
>
>