Contents:
1. Defense of Choice
2. Toposes with inclusion
3. Nonstandard analysis without tears.
(Sorry this got so long.)
From: peterj(a)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
