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