Fixing the constructive continued-fraction definition of the reals: proofs and refutations
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
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
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
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
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
participants (2)
-
Toby Kenney -
Vaughan Pratt