Contents: 1. Defense of Choice 2. Toposes with inclusion 3. Nonstandard analysis without tears. (Sorry this got so long.) From: peterj@maths.su.oz.au Vaughan Pratt seems to be challenging the rest of us to find something wrong with his ordinal-based definition of Set, and no-one else has taken up the challenge; so I'll have to break my vow and point out its obvious shortcoming. Peter's points are sufficiently well taken as to deserve both careful reflection and measured response. I apologize for the one-liner on Monday referring to Peter's Sunday message in the middle of a postscript advertising my LL'96 paper, which violated both of these. Cryptic responses only clog everything up. Peter argues that Choice should be avoided in constructions, on the following ground. I suppose only a minority of mathematicians are unhappy about AC to the extent of actually rejecting any construction that can't be done without it. But I think a very large majority would be unhappy about calling upon God to construct things for them (such as the real numbers) for which they know there is a perfectly good man-made construction. Such people are going to be in a near- permanent state of unhappiness if they are condemned to do mathematics inside Vaughan's category. =================== 1. Defense of Choice Before I address the distinction Peter draws here between natural chaos and mathematical artifact, I'd like to put in a word for Choice, which Peter isn't exactly leaping to defend. Using Choice is like wearing eyeglasses. The wearer barely sees them but sees the world more clearly. The *observer* of the wearer on the other hand sees the glasses directly as the wearer's baggage or ornament, and is only indirectly aware of the wearer's improved vision. Using Choice lets you prove more theorems, but they also shorten existing proofs, sometimes significantly. There is no shortage of examples, but just to point to the case under discussion, if you organize a category-with-epsilon-trees along the lines I was suggesting, the construction of epsilon reduces to the equation \epsilon = <. At a fraction of a line, this is significantly shorter than the published constructions, which seem to require a lot more. Long proofs cloud our mathematical vision. A shorter proof shows us the same result but by a path that makes its truth clearer. The proof as the means is a sine qua non, but that does not make it the end, the truth is the end (wearing my Platonist hat for now). The counterpart to the observer of the wearer of eyeglasses is that movie critic of the foundations world, the axiom system critic who worries about excess baggage, ornamentation, and/or legislation. Why interfere with the natural course of things when with just a little accommodation of nature by longer proofs we can leave her unfettered by legislation? Unfortunately all known ways of building a house seem to entail some disturbance of nature, and this commendable environmental concern is in impractical conflict with the requirement that your house have a picture window with a clear view of mathematical truth. Quantum mechanics and Choice are in much the same boat. Neither makes as direct contact with the truth as F=Ma or x+y=y+x, but both are better understood as sharpening vision, providing respectively the physicist and the mathematician with eyeglasses. In time they may come to feel like absolute truth, but this is a slow process. Arguing against Choice, understood internally, applies nonmonotonic logic to restrict what can be deduced. It is fundamentalist in its rejection of sophisticated reasoning supporting clear thinking. (Sorry if that's too cryptic, happy to explain privately if this worries you.) ============= 2. Toposes with inclusion Such people are going to be in a near- permanent state of unhappiness if they are condemned to do mathematics inside Vaughan's category. At first I had interpreted this to mean that mathematicians would be unhappy working with reals that had bits of the membership relation dangling off them. This seemed no objection at all; of course the user doesn't want construction materials on his nice stuff. The builder has to clean up after construction, or the user isn't obliged to pay the bill in full. But even if the builder doesn't do it, the user can always spend a bit extra to do it himself, and the upshot is the same. But a day or so later, after rereading even if [AC] does [hold], you don't have the ability to point to a particular object of it and say "This is the set of real numbers" (still less to point to a particular morphism and say "This is the addition operation on real numbers"); you have to rely on God's (or "the randomizer's", as Vaughan seems to call him) ability to do it for you. it occurred to me that perhaps Peter was interpreting my construction as meaning quite literally that I was proposing to name reals with ordinals. This certainly would make the users permanently unhappy. My interest in this stuff is ultimately as a user, and I would be unhappiest of all because such a user-unfriendly system would have been my fault, and because it would have been a complete waste of effort. I suppose I could just ask Peter which he meant (or was it something else again?). However both are plausible concerns, and I can think of equally good and more or less independent responses to them, which I'll give now. For the first, I'll define what I'll call for the moment an itopos, for topos-with-inclusion, along with a forgetful functor from itoposes to toposes. (This might be better done for categories in general; here I'm only concerned about clarifying one topos.) For the second I'll point to a particular object of my category and say "This is a monoid embedding the monoid of nonnegative reals as its bounded sequences, the rest being nonstandard reals", and point to a particular morphism and say "This is the addition operation on this monoid, whose restriction to the standard nonnegative reals is standard addition"). This will do double duty as a constructive refutation of Peter's objection and as an interesting (to me), short, and I believe new construction of the reals that bypasses *all* the many intermediate constructions in the standard constructions, *and* produces the nonstandard reals more simply than previous constructions (that I'm aware of) as a potentially useful spinoff. A topos with inclusions is no big deal (though it might be if worked out more carefully than here). Its point is to make explicit the identity of the elements of sets, in part because it is useful in its own right in some situations, in part because it clarifies what is being erased when we claim to erase construction details. The identities of a topos are those of a category, defined by a map i:O->M. An *itopos*, or topos with inclusions, extends the notion of identity to a preorder on the objects as a subcategory of the topos. An *extensional* itopos makes this a partial order. This entails an extension not so much of the signature of a topos itself as just an increase in the arity of identity, as a function from objects to morphisms, from one to ordered two, i.e. not just the diagonal but the "upper triangle" of the homfunctor when a partial order, plus squares on the diagonal when a preorder. The inclusions need to be coordinated with the topos structure, not done here (a good thing too if this is all old hat, which seems rather likely given that it is a rather obvious notion). The strict inclusions for the itopos OSet (for Ordinal Set) that I constructed the other day were already described then as the nonidentity maps from i to j that are the left inclusion of i into i+(j-i). In other words just ignore the excess of j over i and map bijectively and monotonely to what remains of j. Application. In an itopos one can define the usual Boolean operations on sets in the (large) distributive lattice of inclusions (omit the downward remainders), knowing that the intersection of two sets contains the very elements that show up in common in those two sets, not mere stand-ins for them. Cleaning up. There is an evident forgetful functor from OSet to Set, obtained by decrementing the arity of identity to leave only the diagonal identities, those in Set(X,X). The practical impact of forgetting the nondiagonal identities is that functors between toposes need preserve only the retained identities. If you find a need to preserve epsilon structure, it means you should be working in the itopos. This addresses Mike Barr's point, which he mentioned as confirming with Makkai, about most applications ignoring the epsilon structure. Erasing the off-diagonal identities makes it official. =============== 3. Nonstandard analysis without tears Definition. The nonstandard nonnegative reals form the set \omega^\omega of sequences of natural numbers, modulo the following two equational universal Horn clauses whose variables range over sequences, with addition understood as pointwise. 1. 2(a/2) = a 2. a + c = b + c -> a = b The function 2a doubles every element of sequence a: (3,2,..) |-> (6,4,...) The function a/2 shifts the sequence right, setting the leading digit, indexed by 0, to 0. (3,2,...) |-> (0,3,2,...). Think of halving a binary numeral by shifting. End of construction. It can easily be seen that the clauses will not identify an unbounded sequence with a bounded one. The standard nonnegative reals are extracted from this monoid as the (equivalence classes of) bounded sequences. The real denoted by the sequence a_i is sum(a_i / 2^i),i<\omega, in other words ordinary binary notation. Example. The ultimately constant sequences (1,0,0,0,...) and (0,1,1,1,...) denote the respective reals 1.00... and 0.111... in binary notation. These are identified by the following computation: 1.111... = 0.222... by 1 1.000... = 0.111... by 2, with c = 0.111... A little work shows that every bounded real is identified by clauses 1 and 2 with a sequence all of whose elements but the leading "digit" are 0 or 1, and which if ultimately constant ends in 0's. This of course is the standard binary representation for real fractions, but with a single digit in "radix" \omega for the integer part. It should be clear that pointwise addition is ordinary real addition for such reals, with infinite carries propagating in finite time as in the example. This construction makes these standard and nonstandard nonnegative reals a monoid. The same technique that extends the natural numbers to the integers extends these nonnegative reals to the standard and nonstandard reals, of which the standard reals then form a ring (define multiplication as all endomorphisms of the monoid, made a binary operation by associating each endomorphism with where it sends 1) and a field as usual, the standard field of reals. Every real in this monoid being bounded away from zero, the whole monoid without the nonstandard reals cannot form a field, though the above definition of the ring satisfies the ring axioms by construction. But we can easily extend it to a field by the same means by which the integers are made the field of rationals: define an ireal (possibly infinite or infinitesimal real) to be a pair a/b of nonstandard reals, modulo the implication ad = bc -> a/b = c/d. This produces with very little fuss a field suitable for nonstandard analysis without tears. These constructions can all be carried out as operations on objects of the category Set, as a topos obtained by my construction from OSet. All terms used in the construction are made explicitly available in the construction I gave, as part of its signature as a bicomplete topos. No trace of the randomness in the choice of well-ordering of \omega^\omega participates in the construction, which should be understood as merely proving existence and properties of the topos thereby constructed, with the proof erased when done. Here is an indication of how this construction could go, at least for the nonstandard reals. Start with two copies of \omega^\omega, for respectively a and b in clause 2 of the definition. Make \omega^\omega copies of \omega^\omega, one for each c. From the copy for c, delete all sequences pointwise less than c. Send maps a+c, b+c from a,b to c respectively. Now make one more copy of \omega^\omega and send maps x-c from c to it. (Note that monus never "underflows", because we deleted those elements.) The colimit of this diagram implements 2. 1 is an easy coequalizer. That's it. For the promised addition morphism, very roughly speaking, start from +:\omega^2->\omega, form +^\omega, and apply to this morphism the same operations that were applied above to the objects, all of which are functorial. Getting from here to the ireals is a matter of constructing the "integers" then the "rationals" with any standard approach, starting with \omega^\omega instead of \omega. This construction was described as an infinite diagram for conceptual simplicity. It can be made finitary with first order logic or adjunctions, however you prefer to look at it. Hopefully all operations needed for this conversion are already in the signature provided for Set; if not the signature needs more oomph. Vaughan Pratt