Subject: Choice, inclusions, nonstandard analysis

From: categories <[email-masked]>
Date: Thu, 21 Mar 1996 11:09:41 -0400 (AST)

Date: Thu, 21 Mar 1996 03:33:55 -0800
From: Vaughan Pratt <[email-masked]>

Contents:
	1. Defense of Choice
	2. Toposes with inclusion
	3. Nonstandard analysis without tears.
(Sorry this got so long.)

	From: [email-masked]
	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

---

From: categories <[email-masked]>
Date: Thu, 21 Mar 1996 13:35:34 -0400 (AST)

Date: Thu, 21 Mar 1996 16:53:46 +0000
From: Steve Vickers <[email-masked]>

>if that's too cryptic, happy to explain privately if this worries you.)

There's a sense in which by reasoning non-classically (specifically, with
geometric logic) you can eliminate the need for explicit topology:

  if you define points by a geometric theory, then the topology is implicit
  if you define a map by geometric constructions, then continuity is automatic

>From this point of view, the purpose of explicit topology is to correct the
errors introduced by classical reasoning.

We thus see sophisticated reasoning (classical principles) necessitating
complicated thinking (topology), the reverse of what was intended. You
don't need dogma to see this could be a bad idea, though you do need hard
work to see whether the classical principles really can be dispensed with.

Steve Vickers.

---

From: categories <[email-masked]>
Date: Fri, 22 Mar 1996 11:28:34 -0400 (AST)

Date: Fri, 22 Mar 1996 00:44:30 -0400
From: RJ Wood <[email-masked]>

I would like to comment on Vaughan Pratt's

> 1.  Defense of Choice
...
> examples,...

Write CD(L) for complete distributivity of a complete lattice L.
Write CCD(L) for constructive complete distributivity of L, by which is 
meant that \/:DL--->L has a left adjoint, where DL is the lattice of
down-closed subsets of L, ordered by inclusion.

It is easy to show that CD==>CCD but many times in joint work with
Fawcett, Rosebrugh and Marmolejo I have been led back to the more
interesting
AC<==>(CD<==>CCD)    *

Without choice there is not much that one can prove about CD.
In fact, without choice there is a severe shortage of infinite L
satisfying CD(L). (Recall that AC is equivalent to `for every set X,
CD(PX), where P denotes power set'.) My experience suggests that
all theorems about CD follow from constructively proveable theorems
about CCD after invoking *. Those that my colleagues and I have 
discovered have reasonably ``short'' proofs, if one starts with some
basic knowledge of adjunctions.

Allow me to discharge the facile comment that by *, any theorem that has been
proved constructively about CCD (examples exist) proves that ``Using Choice
lets you prove more theorems'' because that is not the point of this note.

Rather, I think that * and similar results show that some of the
definitions and concepts that seem to arise rather ``naturally'' from
traditional set-based Mathematics are not particularly natural. Stepping
further away from Mathematics, I think that twentieth century Mathematics
has frequently sacrificed useful generalization for excessive abstraction. 

RJ Wood

---

From: categories <[email-masked]>
Date: Fri, 22 Mar 1996 14:33:29 -0400 (AST)

Date: Fri, 22 Mar 1996 09:18:21 -0800
From: Vaughan Pratt <[email-masked]>

Phew, thanks Richard, no fun defending a position alone.

Here's another argument for Choice, no more or less a proof than the
clarity-of-mathematical-thought argument, it seems to me.

"Proof" of AC.  It took mathematics about thirty years longer to
imagine AC false than it did to imagine it true.

This "argument" can be applied in other situations.  Applying it to
Grothendieck universes (aka inaccessible cardinals) would suggest that
they don't exist.  We can imagine their nonexistence (their existence
is independent of ZFC) but so far we haven't been able to imagine their
existence (a proof in ZFC that they don't exist is still on the
cards).

What arguments exist in *support* of the existence of Grothendieck
universes?  I see the "cogito ergo sum" argument, what else?

Vaughan Pratt

---

From: categories <[email-masked]>
Date: Fri, 22 Mar 1996 17:10:10 -0400 (AST)

Date: Fri, 22 Mar 1996 16:01:04 -0500 (EST)
From: [email-masked]

Vaughan Pratt says
  <<What arguments exist in *support* of the existence of Grothendieck
  <<universes?  I see the "cogito ergo sum" argument, what else?>>
    I once asked Joe Shoenfield that -- not quite in those terms -- and his
answer certainly didn't seem to me "cogito ergo sum". That seems to me,
assuming I understand what argument you mean, not radically better than
Anselm's proof of the existence of God: we can imagine the best thing in the
world, and if it is the best it must exist (otherwise one that existed
would be even better), so it exists, QED. Now I don't suppose you mean a
White Knight's sort of argument -- the universe imagined me, therefore it
exists. You mean I imagine Grothendieck's universe, therefore IT exists.
Well, Joe said in effect I can tell you everything that goes to make up the
first Grothendieck universe, except I don't have time to finish telling you.
It's the null set, and the singleton of the null set, and [and on. Not just
countably, of course; we can describe \omega very satisfactorily, and the 
union of an omega-sequence of ordinals, and on. This differs from Anselm's
word game in being a string of constructions. The first Grothendieck
universe is rather large, so it is a fairly formidable kit of constructions.
Pass to a second Grothendieck universe, and you used at least one miracle, to
produce an individual from the first-universe construction. 
      John Isbell