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

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

[Vaughan Pratt]

Prof. Peter Johnstone wrote:
> On Wed, 11 Feb 2009, Vaughan Pratt wrote:
>
>> Prof. Peter Johnstone wrote:
>>>  Whoa! This simply can't work. Whatever the final coalgebra for N x (-)
>>>  looks like, it must (thanks to Lambek) be isomorphic to N x itself,
>>>  and therefore (since equality for N is decidable) must have lots of
>>>  complemented subobjects {0} x itself, {1} x itself, ... The point of
>>>  the continuity theorem for functions R --> R is that there are toposes
>>>  in which R has *no* nontrivial complemented subobjects [...]
>>>  The only way to get round it (apart from using glue)
>>>  is to replace N by some "nonstandard natural number object" having no
>>>  nontrivial complemented subobjects -- but where you get that from, I
>>>  don't know.
>>
>> You're assuming product distributes over sums, which would be true for
>> ordinary product but I specified lexicographic product, with the left
>> argument as the "high order digit" (converse of the usual convention for
>> ordinal product in ordinal arithmetic).
>
> For goodness' sake, Vaughan! How many times do I have to tell you that
> I'm talking about *the underlying object* of the final coalgebra, and
> not its order structure or its topology? If the underlying object of
> the lexicographic product is the ordinary (cartesian) product -- and
> if it's not, then I don't know what it is -- then it distributes over
> sums because that's what products do in a topos.

Peter, if you don't mind my answering a question with a question, did
either of us mention underlying objects before?  (I could have
overlooked an earlier message.)

When you speak out of the blue about "the underlying object of the final
coalgebra," what exactly is underlying what?  I feel like I've abruptly
stepped through a mirror into some strange part of topos theory that
will be covered in Volume 3 of the Elephant.

One notion of underlying object that makes sense for me in the context
so far is the set E(1,X) of elements of an object X in a topos E.  With
this notion I have a prayer of making sense of your claim in the context
of the following four objects of a topos E with NNO N (and whatever else
if anything is needed to ensure that objects 2-4 exist in E).

1.  N^2.

2.  The initial object among all objects X with an element 0: 1 --> X
and maps s,t: X --> X satisfying st = ts.

3.  As for 2 with ts = t in place of st = ts.

4.  As for 3 with st = s in place of ts = t.

If I've grasped this slippery topos concept, all four objects X of E
have, as their underlying set E(1,X), the set of all pairs (m,n) of
natural numbers (up to isomorphism of course).  In 2 the elements take
the form of terms (s^m||t^n)(0) meaning m s's and n t's applied in any
order to 0.  In 3 the elements take the form of maps s^m(t^n(0)) meaning
n applications of t (coarse tuning) followed by m applications of s
(fine tuning), while in 4 they take the form of maps t^m(s^n(0)) (3 with
s and t interchanged).

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.

I presume that 3 and 4 are isomorphic on the ground that s and t can be
mapped to any two endomorphisms whence there must exist an isomorphism
exchanging s and t.  I imagine I would get less out of a rigorous proof
of that unless there's a bug in the previous sentence.  If there's no
bug then this would seem to constitute a subtle difference from algebra,
where the signature labels the operations in a way that prevents such an
interchange and puts 3 and 4 in distinct albeit equivalent varieties.

Whether or not 1 and 2 are isomorphic, they are in some sense both
representations of the ordinary product of N with itself.

Where I have greater difficulty is imagining an isomorphism between 2
and 3 merely on the ground that they have the same underlying object.
I'm really not following your logic here.  2 implements product
concurrently whereas 3 and 4 implement it sequentially.  How could they
be isomorphic in every topos?  (I can see that they'd have to be
isomorphic in Set, and presumably certain other toposes which however I
have no idea how to characterize.)  I regard 3 and 4 as equivalent
definitions of the ordinal w^2 (w = \omega) in a topos.

What are the necessary subobjects of 3, and which of those are
necessarily complemented?  I can think of the singletons {(m,n)}, the
set of successor elements (since s: X --> X is a monic), and the
*uniform* tails s^m: X --> X of the successor elements, but not the set
of limit ordinals in w^2 since t: X --> X is not a monic, and hence not
anything involving t.  Are there other subobjects of 3, and can you
characterize them all in some neat way?

If as you seem to be implying, 1-4 are isomorphic, then I would have to
agree with your "for goodness' sake" (yes it was really stupid of me not
to see that) and resign myself to the absence (thus far) of any
alternative to apartness for representing the reals.

If however you agree with me that they can't be isomorphic (via
something more reliable than my proof by agitated gesticulation born of
summary dismissal) then we can move on with the rest of my envisaged
program to define the continuum [0,x) in a topos without appealing to
apartness.  This too may or may not have bugs, whence the "proofs and
refutations" qualification in the new subject line.  (If this were darts
there'd be a sequential scoreboard, concurrently with beer.)

Vaughan

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

[Vaughan Pratt]

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

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

[Toby Kenney]

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

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

[Vaughan Pratt]

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

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

[Toby Kenney]

Vaughan Pratt wrote in part:
...
>
> One notion of underlying object that makes sense for me in the context
> so far is the set E(1,X) of elements of an object X in a topos E.  With
> this notion I have a prayer of making sense of your claim in the contex=
t
> of the following four objects of a topos E with NNO N (and whatever els=
e
> if anything is needed to ensure that objects 2-4 exist in E).
>
> 1.  N^2.
>
> 2.  The initial object among all objects X with an element 0: 1 --> X
> and maps s,t: X --> X satisfying st =3D ts.
>
> 3.  As for 2 with ts =3D t in place of st =3D ts.
>
> 4.  As for 3 with st =3D s in place of ts =3D t.
>
...
>
> 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.
>
> I presume that 3 and 4 are isomorphic on the ground that s and t can be
> mapped to any two endomorphisms whence there must exist an isomorphism
> exchanging s and t.  I imagine I would get less out of a rigorous proof
> of that unless there's a bug in the previous sentence.  If there's no
> bug then this would seem to constitute a subtle difference from algebra=
,
> where the signature labels the operations in a way that prevents such a=
n
> interchange and puts 3 and 4 in distinct albeit equivalent varieties.
>
> Whether or not 1 and 2 are isomorphic, they are in some sense both
> representations of the ordinary product of N with itself.
>
> Where I have greater difficulty is imagining an isomorphism between 2
> and 3 merely on the ground that they have the same underlying object.
> I'm really not following your logic here.  2 implements product
> concurrently whereas 3 and 4 implement it sequentially.  How could they
> be isomorphic in every topos?  (I can see that they'd have to be
> isomorphic in Set, and presumably certain other toposes which however I
> have no idea how to characterize.)  I regard 3 and 4 as equivalent
> definitions of the ordinal w^2 (w =3D \omega) in a topos.
>

I=B4m pretty sure the objects (1)-(4) are isomorphic. Here=B4s a sketch o=
f the
proof:

Let X be the object (3), i.e. the initial object with a morphism 0:1---->=
X
and morphisms s:X---->X, t:X---->X with st=3Ds. Let Y be the object (2),
i.e. the initial object with a morphism 0:1---->Y and morphisms u:Y---->Y=
,
v:Y---->Y.

(1)&(2):
We clearly have maps 0 x 0: 1----> N^2, succ x 1_N and 1_N x succ :
N^2---->N^2, inducing the map Y---->N^2. For an element a of Y, we can
form maps f_{t,a}: N---->Y by 0 ]----> a, succ ]----> t, and f_{s,a} by
0 ]---->a, succ ]----> s. We can now form a map N x N ----> Y by
f(a,b)=3Df_{t,{f_{s,0}(a)}}(b). We can check that these maps form an
isomorphism.

(2)&(3):

Lemma: X is a monoid

We construct the addition X x X---->X by its exponential transpose
X---->X^X. This is the map induced by 1_X:1---->X^X, s^X:X^X---->X^X, and
t^X:X^X---->X^X.

We think of this monoid structure as ordinary ordinal addition.
We now construct morphisms s=B4 and t=B4 X---->X, given by s=B4(x)=3Dx + =
1 and
t=B4(x)=3D\omega + x. It is clear that s=B4 and t=B4 commute. This induce=
s a
morphism Y---->X.

On Y, we can create the projection map p:Y---->N as Y is isomorphic to N =
x
N. We also have the inclusion i : N ----> N x N given by a ]----> (a,0).
Now ipu and v satisfy ipuv=3Dipu (ipu is the map \_ + \omega. This induce=
s a
map X ----> Y, which will be the inverse of the map Y ----> X.

I will check the details later to make sure. But I would be very surprise=
d
if there were any problems.

Toby