Subject: Re: Set membership <-> function composition

From: categories <[email-masked]>
Date: Tue, 12 Mar 1996 08:29:35 -0400 (AST)

Date: Mon, 11 Mar 1996 17:07:55 -0400 (AST)
From: Michael Barr <[email-masked]>

 Let me introduce my response by saying that although I was more-or-less
 familiar with Lawvere's thoughts on the subject, I had never thought too
 much about them until some years ago, more than 5, less than 10, when
 I found myself teaching a course in set theory.  For the first time,
 I came to realize what a complex horror set membership really is.
 In every other type of mathematics I had ever studied, the objects
 were some kind of sets with some kind of structure and the arrows were
 the functions (or at worst equivalence classes of such) that preserved
 them.  Mostly, the structure was given by operations, or at least
 partial operations, although Top was something of an exception, but
 even there, continuous maps are those that preserve ultrafilter
 convergence.
 
 But of course, Sets are an exception.  Here are sets defined in terms of
 these elaborate epsilon trees and this structure is invariably ignored.
 It seemed to me intuitively, confirmed by Makkai, that the ONLY arrows
 between sets that actually preserved all that structure were inclusions
 of subsets.  So that obvious category is just a poset.  But of course
 the truth is that that epsilon structure is invariably ignored.  So
 why is it taken as the basis of mathematics.  Much better to simply
 define sets as the objects of a category and then an element is just
 a global section, or rather an equivalence class thereof.  
 
 My whole experience with category theory convinces me that membership and
 the closely related idea of equality is an intrinsically obscure notion
 Or rather, not that it itself is obscure, but it obscures anything
 it touches.  Like, the idea of embedding Z into Q by taking the eqivalence
 classes of fractions and then removing those that include a fraction
 of the form n/1 and replacing them by the corresponding integer.  Yes,
 it can be done and we certainly want to say that Z is a subring of Q,
 but it is such a mess and so unnecessary.
 
 Some would say, but not I, that you should just work in your favorite
 topos.  I take a platonic view that there really are sets, but membership
 and equality are not the simple concepts we think they are.  In particular,
 I would like to say that a fraction is a pair of integers m/n, n > 0 and
 that m/n = p/q when mq = np.
 
 I don't know about pointers to the literature. 
 
 Cheers, Mike

---

From: categories <[email-masked]>
Date: Tue, 12 Mar 1996 14:45:55 -0400 (AST)

Date: Tue, 12 Mar 1996 10:27:25 -0500 (EST)
From: [email-masked]

  On Mike Barr's comments. The bulk of them are right enough, though maybe it
is not quite fair to complain that something designed as foundation for every-
thing is awkward to work with. Like complaining that the tax code is full of
qualifications and exceptions. But, what stirred me to respond is recognition
of an old friend in
<<I would like to say that a fraction is a pair of integers m/n, n > 0 and
<<that m/n = p/q when mq = np.>>
   So would Saunders MacLane, sorry, Mac Lane. He gives the axioms in his 1948
invited address published as 'Duality for groups' in BullAMS 1950. The
community has not taken up Saunders' axioms, can't think why. 
     John Isbell

---

From: categories <[email-masked]>
Date: Wed, 13 Mar 1996 10:48:59 -0400 (AST)

Date: Tue, 12 Mar 1996 17:11:35 -0500
From: Robert A. G. Seely <[email-masked]>

Michael Barr's reply to this question was not entirely complete (IMHO), as
he forgot to mention that he wrote a short paper some time (3 yrs) ago
dealing with matters related to this.  Those interested might want to
download his paper, which can be obtained by ftp from triples.math.mcgill.ca
in the directory pub/barr (look for variable.sets.*.Z, where * = dvi, tex,
or ps).

= rags =

---

From: categories <[email-masked]>
Date: Wed, 13 Mar 1996 12:49:06 -0400 (AST)

Date: Wed, 13 Mar 1996 10:29:57 -0500
From: Peter Freyd <[email-masked]>

One may argue that formal set theory relates to topos theory in the
way that untyped lambda calculus relates to the typed theory. If you
think it's difficult to get a model of set theory out of a topos try
to get a model of untyped lambda calculus out of a model for the typed
theory.

The semantics of core mathematics -- unlike the semantics of a
programming language -- has never presented much of a problem. The
perversity of formal set theory as a foundational language for
mathematics has not been much in evidence for the simple reason that
no mathematician has ever actually used it for his semantics. 

I am not saying here that the continuum hypothesis is perverse, or
even questions about much larger cardinals. (For one thing they can be
stated easily in a topos setting.) I am saying that formal set theory
allows entirely perverse questions that have nothing to do with the
semantics of mathematics.

The actual elements used for a mathematical construction are never of
interest. Imagine your reaction to an interruption at the beginning of
a lecture on number theory, "Which construction of the natural numbers
do you have in mind? Russell's or Van Neumann's?" My favorite example
of the sort of perverse question one can ask if one were to take
formal set theory seriously is "Does any simple group appear as a zero
of the Riemann Zeta function?"

---

From: categories <[email-masked]>
Date: Wed, 13 Mar 1996 16:28:38 -0400 (AST)

Date: Wed, 13 Mar 1996 19:30:06 GMT
From: Ralph Loader <[email-masked]>

Hi,

>interest. Imagine your reaction to an interruption at the beginning of

It's perfectly feasible to imagine that in say, descriptive set theory,
properties of certain structures could be shown by showing (1) they have a
certain cardinality, (2) sets of such cardinality have epsilon trees with a
certain property and (3) using epsilon induction over such epsilon trees to
prove something about our original structures.  [I don't know of any such
instances; I'm not a descriptive set theorist.]

Alternatively, what about Godel's constructible universe.  This seems to be
a mathematical construction, and the actual element relation seems to be
not only of interest, but essential to the construction.

>of the Riemann Zeta function?"

This is an interesting example.  You state a question in mathematical
English, and then criticise ZF for being able to express this question,
while category theory cannot.  One wonders what other questions stated in
mathematical English---some of them perhaps perfectly sensible---can be
stated in the language of ZF, but not in the language of category theory.
I'd much rather that my formalisation of mathematics could state
nonsensical things (consistency strength isn't an issue here), than to be
living in the fear that my formalisation may be inadequate to express some
sensible arguments.

Two examples that I think are relevant to this debate.

Category theorists are keen on statements to the effect that structures are
defined by their universal properties.  A typical book on topos theory may
define an elementary topos as a category with finite limits and power
objects.  It then goes on to show that any topos has internal-homs.  How?
By defining the function space as a certain set of sets of ordered pairs...

Let Nat(x) be the statement "x is a triple (omega,S,0) to which the Peano
axioms apply". ZF |- "there exists x such that Nat(x)".  This is sufficient
to do arithmetic; after proving this single existential statement, one need
never give a particular construction of the natural numbers again.  Indeed,
if one is really worried about these things, note that ZF+"Nat(omega)"
(where omega is a new constant symbol) is conservative over ZF and then
work in the latter theory, without ever fixing on a particular
interpretation of ZF+"Nat(omega)" into ZF.

Both category theory and set theory are amenable to working with
mathematical structures by either explicit constructions or by uniquely
characterising properites.  In both category theory and set theory, we
prove the existence of structures with certain uniquely characterising
properties via explicit construction.

Ralph.

---

From: categories <[email-masked]>
Date: Wed, 13 Mar 1996 16:54:29 -0400 (AST)

Date: Wed, 13 Mar 1996 15:45:47 -0500
From: Michael Barr <[email-masked]>

- 
- Date: Wed, 13 Mar 1996 10:29:57 -0500
- From: Peter Freyd <[email-masked]>
- 
.................................
- 
- The actual elements used for a mathematical construction are never of
- interest. Imagine your reaction to an interruption at the beginning of
- a lecture on number theory, "Which construction of the natural numbers
- do you have in mind? Russell's or Van Neumann's?" My favorite example
- of the sort of perverse question one can ask if one were to take
- formal set theory seriously is "Does any simple group appear as a zero
- of the Riemann Zeta function?"
- 
- 
My point exactly.  The elements don't matter, so why should
elementhood be taken as the fundamental relation of all
of mathematics?  Equality doesn't matter either, but
equivalence relations do.

---

From: categories <[email-masked]>
Date: Wed, 13 Mar 1996 17:12:59 -0400 (AST)

Date: Wed, 13 Mar 1996 15:54:44 -0500
From: Michael Barr <[email-masked]>

- 
- Date: Wed, 13 Mar 1996 19:30:06 GMT
- From: Ralph Loader <[email-masked]>
- 
............................
- 
- Category theorists are keen on statements to the effect that structures are
- defined by their universal properties.  A typical book on topos theory may
- define an elementary topos as a category with finite limits and power
- objects.  It then goes on to show that any topos has internal-homs.  How?
- By defining the function space as a certain set of sets of ordered pairs...

................................
- 
- Ralph.
- 
- 
Nonsense.  How can a set of sets of ordered pairs be an object of a
topos.  In fact, there is at least one book that defines a topos as
a category with finite limits and power objects and constructs the
internal homs as a limit of two arrows between two power objects.
The construction is hidden inside a cotriple, but that is what it
amounts to.

---

From: categories <[email-masked]>
Date: Thu, 14 Mar 1996 10:24:35 -0400 (AST)

Date: Wed, 13 Mar 1996 13:40:25 -0800
From: james dolan <[email-masked]>

-This is an interesting example.  You state a question in mathematical
-English, and then criticise ZF for being able to express this question,
-while category theory cannot.

i at least am curious just what is this mathematical question you
claim to have in mind which zf can express but which category theory
can not.  obviously it wasn't "Does any simple group appear as a zero
of the Riemann Zeta function?" since that is mere gibberish and not a
mathematical question at all.  zf was being criticized for being
unable to not express this non-question, and category theory was being
praised for having the option to express "it" (should someone actually
bother to give it a real meaning) or not.

whatever was the real point that you were trying to argue might still
be interesting to hear but it's hard to even know what that point
might have been in light of the apparent misunderstanding you've
exhibited here.

---

From: categories <[email-masked]>
Date: Thu, 14 Mar 1996 10:25:21 -0400 (AST)

Date: Wed, 13 Mar 1996 13:45:19 -0800
From: Vaughan Pratt <[email-masked]>

	The semantics of core mathematics -- unlike the semantics of a
	programming language -- has never presented much of a problem.

It would be interesting to hear a few mathematicians who *don't* work
much in foundations comment on this.

===

Item A.

	The perversity of formal set theory as a foundational language
	for mathematics has not been much in evidence for the simple
	reason that no mathematician has ever actually used it for his
	semantics.

Isn't this a bit strong?  An awful lot of mathematicians are under the
impression that their definitions are grounded in set theory.  This has
the enormous advantage for them that, if pressed as to whether their
own mathematics is consistent, they can claim

(a) that the definitions could be expanded all the way out to whatever
fragment of ZF they're assuming if the auditors insist, and

(b) that if their local framework is inconsistent, then the part of ZF
they used (and a fortiori the whole of ZF) is itself inconsistent.  "If
I go down, I'm taking you with me" sort of thing, just like if we ever
find a polytime recognizer for an NP-complete set.

Being well-calibrated on the structure of ZF and which bits are at
greater risk makes it a *lot* easier to organize one's mathematics to
minimize the risk of consistency.  Pretending there never was any risk
of inconsistency in the first place is *very* well contradicted by the
historical record, particularly in calculus.

Today we have trustworthy infinitesimals, of a very elegant kind,
thanks to nonstandard arithmetic.  While one might *wish* that these
had been discovered by categorical means, the actuality is that their
discovery used very heavy doses of formal set theory.  Whether we can
do it today with less heavy doses is beside the historical point.
Formal set theory evolved in response to consistency concerns, and
today it engenders for many of us a strong sense of safety, implicit in
our trust of our own tools, and explicit in actual products such as
infinitesimals we can trust.

===
Item B.

	My favorite example

Item A argues that many of us *do* take formal set theory seriously.
In this item I will argue that doing so does not force one into this
sort of situation.

Now there's nothing inconsistent about going inside a definition and
asking implementation-specific questions.  People do this all the time,
in fact one might argue that mathematicians do it every one or two
sentences.

In any such visit to the inside of a definition, people seem to treat
the occasion as though a tacit NDA (nondisclosure agreement) applied.
Perhaps it shouldn't be so tacit.

MATH NDA.  When you step inside a definition, you agree to bring in
only permitted imports.  You agree furthermore that when you leave, you
will take out only permitted exports.

The usual definitions of "simple group" and "zero of the Riemann Zeta
function" permit neither importing nor exporting the other concept.
Your example enters both definitions at the one time, imports the other
concept in each case, and exits each definition with illicit
information, racking up a total of four NDA violations in a single
exchange.

Even if mathematicians don't stick this NDA to their doors, they know
instinctively to use it, independently of whether their math is
implemented with sets or categories.  Violations of the NDA will get
you funny looks.

===
A+B

Now here's a *very* important point, it's why I separated the above two
issues out as two items.

Item B, the NDA protocol, does not conflict with Item A, the reliance
on the consistency of ZF that many put their trust in.

There is no more conflict here than there is between NDA's in business
and the laws of physics.  All an NDA does is *restrict* what things can
be done, it does not break or even bend any law.

If you don't stick to the NDA's, you may get funny looks, but
consistency is not put at risk.  If you add an unexplored axiom to ZFC
you put consistency at serious risk *and* you get funny looks.  All
very analogous to violating business NDA's and breaking laws of
physics.

===

Back to my original question.

CAT is grounded in Set when you take the homfunctor to go to Set, as is
standardly done.  But the very notion of set is defined by membership;
a set is determined by the truth values of membership of candidate
elements of it.

A choice to be made early on is whether the candidate elements of a
given set themselves must form a set, the point of view encouraged by
toposes where the very question of membership is a private business
discussed only in power objects (a power breakfast comes to mind).  The
alternative is to allow the candidates to form a proper class, as in
ZF, which will blithely tell *every* individual except 1 and 2 that
they are not members of {1,2}, without any consideration of their
feelings.

The first choice does seem saner to me.  However a lot of people think
globally about membership and equality, and it seems like a lot of
religious mumbo-jumbo to them not to be allowed to even *ask* whether
two things are not equal when they don't live in the same
neighborhood.

So when I write about sets, can I safely adopt a "Boolean" style and
say that the question "x \in {1,2,3}" (equivalently, "x=1 or x=2 or
x=3") has only two answers, yes or no?  Or should I do the mumbo-jumbo
thing and clarify the ground-rules by explaining how the existence of
neighborhoods creates at least one more possible answer?  Or should I
pretend there's no problem and think mumbo-jumbo even when I know my
audience is thinking Boolean?

I *hate* that third alternative, it seems so dishonest.  But maybe
dishonesty is the best policy in this situation...

Vaughan Pratt

---

From: categories <[email-masked]>
Date: Thu, 14 Mar 1996 10:26:15 -0400 (AST)

Date: Wed, 13 Mar 1996 16:53:30 -0500
From: Peter Freyd <[email-masked]>

  Ralph Loader writes:

  It's perfectly feasible to imagine that in say, descriptive set
  theory, properties of certain structures could be shown by showing
  (1) they have a certain cardinality, (2) sets of such cardinality
  have epsilon trees with a certain property and (3) using epsilon
  induction over such epsilon trees to prove something about our
  original structures.  [I don't know of any such instances; I'm not a
  descriptive set theorist.]
  
There are all sorts of near-by examples but they're not
counterexamples to my assertion. The fact that any structure of a
certain type is isomorphic to one with further special properties is a
standard first-step. The most usual further property is the existence
of a well-ordering.  But there's no such example, nor will there ever
be, in which one must use some property of the elements of every
possible structure of the given type in order to prove a property of
the structure. That's a tautology if the "property of the structure" in
question is an isomorphism-invariant.

  Alternatively, what about Godel's constructible universe.  This
  seems to be a mathematical construction, and the actual element
  relation seems to be not only of interest, but essential to the
  construction.

I must agree that when making constructions in mathematical subjects
in which the elements are the essence then one will use elements.

About my example of the philosopher who asked the number theorist (I
actually witnessed this) whether he was proving theorems about Russell's
or Van Neumann's numbers led Ralph to reply:

  You state a question in mathematical English, and then criticize ZF
  for being able to express this question, while category theory
  cannot. One wonders what other questions stated in mathematical
  English---some of them perhaps perfectly sensible---can be stated in
  the language of ZF, but not in the language of category theory. 

In fact there are topos-theoretic analogues for Russell and Van
Neumann, but not even a philosopher would be tempted to ask the
analogue question. Besides the R and VN numbers one could ask the
analogue question about the Lawvere and the Church numbers (in
category theory, not in set theory). But one wouldn't.

Anyway, I do have a counterexample to my own assertion. I think JH
Conway gave us some examples of mathematical constructions in which
the elements are the essence, to wit, his games and his numbers. Conway
games can be described as the result of replacing the single epsilon
of ZF with a pair of epsilons (for left and right "moves"). If one
restricts attention to "impartial" games (any move legal for one player
would have been legal for the other) then the two epsilons can be 
conflated and the subject conflates to ZF.

---

From: categories <[email-masked]>
Date: Thu, 14 Mar 1996 10:26:55 -0400 (AST)

Date: Thu, 14 Mar 1996 09:38:34 +1100 (EST)
From: [email-masked]

Peter Freyd's old question "Does any simple group appear as a zero
of the Riemann Zeta funxtion?" reminds me of the pleasing fact that
it contains what philosophers would call a "category mistake".
Pleasing because it's precisely the sort of mistake you can't make
if you're working in a category.

Peter Johnstone

---

From: categories <[email-masked]>
Date: Thu, 14 Mar 1996 10:27:35 -0400 (AST)

Date: Thu, 14 Mar 1996 01:25:06 -0800
From: Vaughan Pratt <[email-masked]>

My original problem was what to do about the absolutely ghastly
argument I complained about, showing that membership could be figured
out in Set.  I now have a solution, only a couple of whose 70 lines are
needed to describe membership.  The rest explicitly, arithmetically,
and (except for infinite products) completely describes all the
adjunctions of (a lightweight version of) the bicomplete topos Set.

For starters, you need to accept Mike Barr's intuition that "the
elements don't matter."  If it bothers you that {2,4,17} is not "in" my
version of Set, you aren't looking at it from Mike's perspective.

It's tempting to make Set even lighter weight than I do here by
constructing it as Skel(Set).  But while this is technically feasible,
it makes the definition of limits and colimits on infinite sets
obscure, and also loses a property I'll mention below in connection
with a nice observation of John Isbell.

Instead I retrace what I imagine is a familiar path for set theorists,
but from the categorical perspective.  I take the objects to be simply
the ordinals, each defined as the set of ordinals less than it, and the
maps to be all functions (in the usual sense) between ordinals.  (So
for all cardinals alpha, this Set has only alpha many sets of
cardinality less than alpha, which is what I mean by lightweight.)

This may well have been already proposed before, since it is so simple
and solves my problem so directly.  But if so then why didn't someone
bring it up as an answer to my question?

The ordinals being a transitive class, membership i \in j coincides
with (global) strict inclusion i \subset j, which as will be seen below
is definable as the left "local" inclusion of i into i+(j-i).  This is
ten times shorter than the method I complained about (Goldblatt 12.4)
for calculating membership in Set!

Here are some features of this version of Set.  I'll abbreviate \omega
to \w, \eta to \i, \epsilon to \e.

* The full subcategory consisting of the finite sets is skeletal.

* Since every set is well-ordered, by definition, Choice holds.

* Since i+j=k is uniquely solvable in j for i<=k (this can be seen
informally by deleting the first i elements of k and taking j to be the
order type of the residue), it follows that monus (nonnegative minus)
can be defined, denoted k-i.  (Note that i+j=k is not uniquely solvable
in i, witness i+\w=\w which has all finite ordinals as solutions while
i+\w=\w+1 has no solutions.)  We also have ordinal ("integer") division
i/j and remainder i%j, see below.

* The *global* inclusion (assumed proper) of i into j is definable,
namely as the "local" inclusion of i into i+(j-i) (meaning the first
half of the unit of the adjunction defining +, at (i,j-i)), just when
this is not the identity on i.  (For j <= i, j-i = 0, making the local
inclusion the identity.)  The global inclusions make Set an irreflexive
poset, identical to membership except that we do not normally speak of
membership of x in y as a map, only as the truth of the binary relation
of membership at the object pair (x,y).  If for some crazy reason we
want to represent the membership relation by maps in Set, the global
inclusion maps are the obvious choice.

* The isomorphism 1=>x = x is the identity 1_x, and similarly for the
isos \rho: x*1 = x, \lambda: 1*x = x, and \alpha: (x*y)*z = x*(y*z)
making Set a strict cartesian closed category.  I wrote = rather than
tilde to avoid a repeat of yesterday's screwup with caret, but in fact
these are equalities in the strongest sense: they make \rho, \lambda,
and \alpha all identity natural transformations.

Isbell's argument in CTWM VII.1 shows that we can't *always* make
\lambda,\rho,\alpha identities, even in a CCC like Skel(Set).  In the
present context Isbell's argument yields more, namely that any
construction we use to further reduce Set from the ordinals to a
skeletal category *must* weaken these identities to isos.

What saves the day for ordinals is that when x,y,z are countably
infinite, x*y and (x*y)*z get to be different infinite ordinals.
Isbell's argument gives really nice insight into why set theorists find
ordinals work better than cardinals: as cardinals, countable x*y and
(x*y)*z have to be the *same* countable cardinal, ordinals create
useful elbow room.  (Without this category perspective, I don't know how
to make a convincing case for ordinal arithmetic over cardinal, anyone
know a noncategorical way?)

* The inclusion of the rationals into the reals (as Dedekind cuts) is
definable, but only as a local inclusion, not a global one, nor a
monotone one with respect to the well-ordering of the reals.  Set well
orders the reals "randomly," and we get to probe around in the
resulting well-ordering after the "big coin toss" and sniff out some
(all?) aspects of its crazy choices.  (Use the global inclusion of 1
into the reals to locate the "least" real "0", which can now be
compared with the "real" additive identity of the reals, 0.0.)  But
because it depends on the coin toss it is not mathematics, just
unrepeatable noise.

*  But this isn't to say that every uncountable ordinal looks random.
The least uncountable ordinal \w_1 *is* ordered predictably and
repeatably, and that order *is* genuinely mathematical (to believers in
\w_1 anyway).

There's presumably a lot more to say about Set defined this way, but
this is way overlength already, so let me push on to describe the
category Set itself.  The description talks about 0 and successor early
on; these can be understood either externally starting from an already
constructed Set (less demanding pedagogically) or internally as a
purely categorical definition of Set (in terms of constants 0,1,+
denoting initial and final objects and a coproduct), which will
inevitably seem circular just like ZF seems circular.

====================Light Set---V.R. Pratt--3/13/96===========

I'll start from the class of von Neumann ordinals, each the set of all
ordinals less than it (sorry, Mike), and define all small sums and
products, (co)equalizers, and the classified subobjects.  I'll follow
the standard ordinal conventions for binary sum and product, which make
1+\w = \w < \w+1 and 2*\w = \w < \w*2.

We need some auxiliary operations on ordinals.

        i/j  =  the least k satisfying i < j*(k+1)
        i%j  =  i - j*(i/j)     (i modulo j)

Exercises.  i <= j*(i/j), i%j < j.

Binary sums (for illustration).  To form i+j, form j' by adding i to
the *elements* of j (recursively), and take i+j to be i union j', with
the evident inclusions.  (This is not commutative in general, as noted
earlier.)

This generalizes to all small sums as follows.  Given a family n_i of
ordinals indexed by i<I (I=2 for binary sums), take their sum to be the
least ordinal s such that there exists a family f_i of monotone
injections f_i:n_i->s such that i<j<I, h<n_i, k<n_j -> f_i(h)<f_j(k).
For the rest of the adjunction defining this sum, take the unit
\i_<n_i> to be <f_i> and the counit \e_k to be \n.n%k (*not* \n.n%I).

Binary products (for illustration).  Form i*j as the sum of j copies of
i, with the evident projections.  (Not commutative in general.)

Infinite products are a well-known problem for ordinal arithmetic,
starting with \w copies of 2.  The problem is to well-order the
continuum.  Choice says only that a well-ordering exists, we can't
determine one by the constructive methods that work on everything else
in this note.  We just do our best.

Given a family n_i of ordinals indexed by i<I, take their product to be
the least ordinal p such that there exists a jointly monic family f_i
of monotone surjections f_i:p->n_i (the projections) such that for all
x<y<p, if there exists a largest j such that f_j(x) != f_j(y), then
f_j(x) < f_j(y).  The projections form the counit while the unit is the
linear function \n.an where a=1+sum(n_i,i+1<I) (the brick's diagonal).

The incompleteness of this specification arises when such a largest j
does not exist.  Note that care is taken not to contradict the
definition for finite products, which *does* completely specify the
adjunction for product.

Exponential ij.  Defined as the product of j copies of i (inheriting
the infinite product problem when j is infinite).  The unit of the
defining adjunction (-j right adjoint to j*-, not -*j) has for its
morphisms linear (!) functions an+b where a = sum((ji)k,0<=k<j), b =
sum(ki(ji)k,0<=k<j).  The counit (evaluation map) at i is the function
\n.((n/j)/i(n%j))%i.  This works by (i) projecting out the function
part of n as n/j and the argument part as n%j (ii) evaluating by
"shifting" and "masking" to pick out "digit" n%j in radix i.  Theorem:
this function is the evaluation map.  (So this weird-looking function
is not an "implementation hack" at all, it's the unique function for
the job.)

Subobject classifier:   Given f:i->2, the associated subobject is the
least j such that there exists a monotone injection g:j->i such that
fg = 1!.  Theorem: such a g:j->i exists and is unique, and is the
pullback of 1:1->2 along f.

The equalizer of f:i->j and g:i->j is the subobject of i corresponding
to the predicate on i "f(x)=g(x)".  Theorem: this exists and is
unique.

The coequalizer object k of f:i->j and g:i->j is the subobject of j
whose characteristic function p:j->2 is the predicate "is the least
representative in its block".  The coequalizer h:j->k maps each element
of j to the least representative of its block.  Theorem: h exists and
is unique.

Vaughan Pratt

---

From: categories <[email-masked]>
Date: Thu, 14 Mar 1996 10:28:21 -0400 (AST)

Date: Thu, 14 Mar 1996 11:43:20 +0000
From: Steve Vickers <[email-masked]>

>living in the fear that my formalisation may be inadequate to express some

I for one _do_ live in fear (not really ... more a sort of smug
schadenfreude) that set theoretic formalisation is inadequate to express
some sensible arguments.

The nonsensical things in set theory seem to arise from a basic nonsensical
postulate: that there is a single fundamental relation "element of" on the
mathematical universe that is sufficient to determine the nature of every
mathematical object. It's a tour de force of modern mathematics that so
much has been accomplished using this postulate, but its essential
unreasonableness should not be forgotten and it is therefore complacent to
assume that it is adequate to express all sensible arguments.

Let me give some examples.

1) The "element of" relation is absolutely _un_fundamental - this is part
of the force of Freyd's example about simple groups. What are the elements
of a real number? If you consider the real number to be a Dedekind section,
then it is a pair of subsets of the rationals, Q, and hence its elements
are whatever you think the elements of an ordered pair are. Or,
equivalently, it can be represented as a subset of Qx2 (or Q x any
doubleton {L,R}). Or, equivalently, a subset of QxQ, with (q,r) in x iff
|q-x| < r (i.e. the real is identified with its neighbourhood filter of
rational open balls). All these enable a real to be described as a set, but
they give it completely different elements. In reality there is no single
universal "element of" relation that describes the nature of everything,
including the reals; instead, the reals are described by various relations
with other specific objects.

2) Topology: Normally one thinks of open sets as being sets of points, but
localic topology views points as being sets of opens (e.g. reals as
neighbourhood filters above). There is obviously a fundamental relation of
points being "in" opens, and localic arguments can be expressed quite
reasonably using it. Set theoretic expression using "element of" completely
obscures this. In other words, set theory prevents you from adequately
expressing reasonable arguments.

3) Generic objects: Suppose we agree on a particular set theoretic
representation, e.g. reals as Dedekind sections. What then is a _generic_
real, such as the x in f(x) = x^2? Set theory has to treat this as a mere
hole where a specific real could be put, but it is quite reasonable to
treat it as a real in its own right (so long as you don't use - e.g. -
excluded middle to demand specific properties of it) and that's exactly
what people do. What are its elements? One can still make sense of the idea
that it is determined by its elements (using "generalized elements" and
Kripke-Joyal semantics), but in doing so one must go far beyond classical
set theory.

4) What about theories such as that of accessible categories, that, for set
theoretic reasons, have to be liberally sprinkled with infinite cardinals?
Doesn't this make you think that perhaps set theory is somehow obscuring
simple ideas?

To my mind, the evidence suggests that despite its undoubted successes, set
theory is not right for mathematical foundations, and we should be looking
for its replacement. It is easy to be bemused by the fact that all our
mathematical upbringing presumes set theoretical foundations, but we should
try to recognize its limitations and failures.

Steve Vickers.

---

From: categories <[email-masked]>
Date: Thu, 14 Mar 1996 10:29:21 -0400 (AST)

Date: Thu, 14 Mar 1996 12:24:37 GMT
From: Ralph Loader <[email-masked]>

>equivalence relations do.

Really?  Try telling that to people who produce computer verified
correctness proofs for communication protocols.  I'm sure they'll be
pleased to know that their proofs should undergo a very significant
increase in size and obscurity to satisfy what appears to be little more
than aesthetic prejudice.

Equality matters in some contexts, it doesn't matter in others.  In some
logics equality is definable rather than explicit, in which case this point
doesn't appear to make much sense.  Trying to be perscriptive about
this---or any other---foundational point seems to me about as useful as
(and just as perverse as) perscriptive linguistics.

Given the known relationships between e.g. topos theory, higher order
logics and various set-theories, is arguing about which is the correct /
best / most relevant foundations of mathematics really that different from
arguing about whether the Russell naturals or the von Neumann naturals are
the correct / best / most relevant natural numbers?  [Of course, this is
fairly independant from questions such as how to present the natural
numbers]

Ralph (who is quite pleased to be talking to someone who isn't a dogmatic
platonist the-universe-is-a-model-of-ZF type).

P.S. any sarcasm isn't intended to be personal.

---

From: categories <[email-masked]>
Date: Thu, 14 Mar 1996 10:30:05 -0400 (AST)

Date: Thu, 14 Mar 1996 12:55:58 GMT
From: Ralph Loader <[email-masked]>

>The construction is hidden inside a cotriple, but that is what it

<sigh/smirk> My desire for a little irony got the better of my pedantic
instincts.  I'm well aware that the phrase "representative of a subobject
of the power-object of a product" would have be more precise than the
morally equivalent set-theoretic terminology.  It doesn't effect the point
that I was trying to make; that whether one defines certain things by
explicit construction or via an axiomatisation is fairly independent of
whether one prefers to work in a logical, categorical or set-theoretic
foundation.  Neither is this effected by the availability of alternative
constructions.

Of course, for some people, it would be a perfectly sensible point of view
that topos theory is interesting precisely because of results to the effect
that a couple of elementary constructs are sufficient to justify the fairly
general use of set-theoretic notation, such as refering to a `set of sets
of ordered pairs'.

Ralph.

---

From: categories <[email-masked]>
Date: Thu, 14 Mar 1996 10:53:13 -0400 (AST)

Date: Thu, 14 Mar 1996 09:28:40 -0500
From: Robert A. G. Seely <[email-masked]>

 >> [ cuts ]
 >> [One] example that I think [is] relevant to this debate.
 >> 

This might be a little disingenuous - 

Of course, in any topos there will be a monic X=>Y --> P(XxY) , so via the
"internal language" X=>Y may be seen as a certain set of sets of ordered
pairs.  But the point is that via the "internal language" you can (and
indeed you may) argue about the structure of a topos in a very "set-like"
manner.  But of course you are not obliged to do so.  So in a very real
sense, your (first) example illustrates that your fear is unfounded.
(Indeed, one can imagine a topos theorist pondering the matter of simple
groups being zeros of the Riemann zeta function in suitable toposes; the
point of Peter Freyd's observation was (I think) that a topos theorist
without any taste is less likely to stumble upon this question than a set
theorist without taste, who might well do so... due to the emphasis upon
different fundamental notions in the two approaches.)

= rags =

---

From: categories <[email-masked]>
Date: Thu, 14 Mar 1996 17:09:16 -0400 (AST)

Date: Thu, 14 Mar 1996 10:08:42 -0500 (EST)
From: Colin Mclarty <[email-masked]>

	Several contributors to this thread share Loader's confusion on a 
couple of points.

	For one, constructibility in set theory does have an isomorphism
invariant meaning, as Mitchell showed in JPAA about 1975. Trivial changes
make the definition work in any topos with natural number object. In fact,
a good bit of work in set theory today is on finding isomorphism invariant
consequences of V=L or related axioms (constructibility relative to some
set). Elementhood is not essential.

	And Peter Freyd's question 

	"Does any simple group appear as a zero of the Riemann Zeta
		function?" 

is not absolute nonsense in ZF or in category theory--it is only 
misleading as it makes a question of (arbitrarily definable) codings look 
like a question of complex analysis. 

	In ZF the answer is: It depends which coding of groups and numbers
you use--it is easy to make up codings where the answer is yes and just as
easy to make them up where the answer is no.

	For what it is worth, the codings in common use all make the
answer "no", since they make every group an ordered 3 or 4 tuple while
they make a complex number an ordered pair of infinite sets. This is
trivia. 

	Now suppose we found some good relation representing groups as
complex numbers, which was manageable to work with and for which we could
show that some simple groups correspond to points which would falsify the
Riemann hypothesis. 

	Then mathematicians might well start asking whether some zero of
the zeta function "is" a simple group--just as we now ask whether some
given real number "is" rational (a question whose strict answer on most ZF
codings is always "no"). And this question would be just as well expressed
in category theory as in ZF.

best regards, Colin

---

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

Date: Thu, 14 Mar 1996 10:40:33 -0500
From: Peter Freyd <[email-masked]>

Vaughan writes:

  An awful lot of mathematicians are under the impression that their
  definitions are grounded in set theory.

Note, please, that I was writing about _core_ mathematics. There's an
aperture problem here. What do we take as the universe of
"mathematicians"?  If we stick to those parts of mathematics as
described by the US National Science Foundation as "core mathematics"
then I will stand by my statement. A semantics is unneeded. 

I must agree, of course, that there have been proofs in core
mathematics that have used structures for which the semantics became
questionable. Because of their technical nature (that is, because
they were needed in proofs, not theorems) consistency arguments -- in
lieu of clear semantics -- were acceptable. There's a reasonably clear
historical argument in favor of ZF for purposes of such arguments.

(One example: In what John Thompson described as his best work he
proved that certain finite groups -- such as the Monster -- appear as
the Galois groups of number fields; in his proof he used the existence
of infinitely many automorphisms of the complex numbers. Whether or
not your semantics allows more than two automorphisms of the complex
numbers, there's no question that the consistency of ZFC implies that
the groups in question do appear as the Galois groups of number
fields.)

---

From: categories <[email-masked]>
Date: Thu, 14 Mar 1996 18:43:11 -0400 (AST)

Date: Thu, 14 Mar 1996 13:30:24 -0800
From: Vaughan Pratt <[email-masked]>

	From: Peter Freyd <[email-masked]>
	If we stick to those parts of mathematics as
	described by the US National Science Foundation as "core mathematics"
	then I will stand by my statement. A semantics is unneeded. 

Without looking, I'm certain that they include calculus.  I'm not sure
what is meant by "calculus doesn't need a semantics."  My impression
was that the evolution of analysis was a beautiful interplay of
definition and theorem that went on for centuries, from Newton (if not
even earlier) right into the end of this century!

Do you see a clear distinction between "definition" and "semantics"?

Vaughan Pratt

---

From: categories <[email-masked]>
Date: Fri, 15 Mar 1996 09:35:19 -0400 (AST)

Date: Thu, 14 Mar 1996 16:41:51 -0800
From: Vaughan Pratt <[email-masked]>

	1) The "element of" relation is absolutely _un_fundamental -
	this is part of the force of Freyd's example about simple
	groups. What are the elements of a real number?

Yes, when you need to kick a set theorist, the real number line is a
particularly sensitive part.  Excellent kick.  Ouch.

	In reality there is no single
	universal "element of" relation that describes the nature of
	everything, including the reals; instead, the reals are
	described by various relations with other specific objects.

I'm with you 100% philosophically on this.  We move and rest, and need
vocabulary for both activities.  Sets are great for lolling around in
(I wonder how Cantor was at sports in school), but terrible for zipping
perfectly smoothly along the real line.

Categories give a much smoother ride than sets because they're *built*
to.  But they also have stationary parts, that show up in two places.

(i)    The objects.  This is where one rests between morphisms.  Having
your objects form a set is a Good Thing, it fits their punctual style:
"Be there on the dot" says the set.

(ii)   Homsets.  Sets are dual to their elements.  This seems to be
because when dealing with powersets you have a higher probability of
meeting the contravariant power set functor herself than one of her
covariant brothers.  (Not a theorem, just a feeling.)  Homsets are no
exception.  When you pass from moving along one morphism at a time in a
category to contemplating the morphisms lying there in profusion in the
homsets, you dualize your viewpoint and see a morphism as merely a
punctual dot of a homset.  This explains the paradox of the very
unpunctual morphisms able to make themselves the punctual members of a
homset, we just view them dually "from the other direction" (not one
parallel to the morphisms though).

I agree that it is a type error to try to understand a smooth line as
made of points when it is just trying to do its job and get you from
point A to point B uninterrupted (poor gap, I interrupted it).
Interruptions are incompatible with smooth travel.  But travel with no
rest at all is pretty grim and hard to sustain when you're trying to
get some real work done, whence line *segments* rather than entire
lines for category theory.  Hell is having to move forever along the
real line!

But it is equally a type error to try to turn your rest stops into
motion.  You *need* to rest from time to time.  For one thing it gives
your maintenance department a turn at doing stuff, maintenance has to
shut down when you're on the move, on-the-fly maintenance is *much*
harder.  And if you're the type of person that has opponents, it's all
in the game to give them a turn.

But if I'm with you 100% philosophically on this example, I'm only with
you about 50% mathematically.  It seems to me that set theory supports
the go part of stop-and-go traffic *pretty* well.  Not perfectly, as we
agree.  But when you consider how much of the continuum set theory *is*
able to comprehend, I'm not terribly sold on the inadequacy of sets for
modeling go almost as well as stop.

	2) Topology: Normally one thinks of open sets as being sets of
	points, but localic topology views points as being sets of
	opens (e.g. reals as neighbourhood filters above). There is
	obviously a fundamental relation of points being "in" opens,
	and localic arguments can be expressed quite reasonably using
	it. Set theoretic expression using "element of" completely
	obscures this. In other words, set theory prevents you from
	adequately expressing reasonable arguments.

I'm with you <10% on this one.  I can't tell what limitation of Set
you're talking about here, but unlike your philosophically excellent 1)
it doesn't seem to match up to any of the well-known limitations.

It sounds like you're saying that set theory doesn't let you talk about
the converse of the membership relation.  That's certainly not the
case.  Or maybe you mean that Set\op is not a concrete category.
What's wrong with its concrete representation as CABA?  If that seems
too complicated, how about its coconcrete representation as the
category of sets and their *converse* functions (binary relations whose
converse is a function)?

Maybe you're saying that  Hom:Set\op*Set -> Set  is outside set
theory.  That too is implausible.

None of these issues hold the sort of terrors for set theorists that
the continuum does.  At least not a terror that has them terribly
bothered mathematically the way the continuum problem does.

	3) Generic objects:

0%, needle wrapped around the post.  You seem to be saying that set
theorists are scratching their heads over what a variable is while the
category theorists have it all sorted out.  News to set theorists.  You
can't kick a set theorist in the variables, they're very well protected
there.

	4) What about theories such as that of accessible categories,
	that, for set theoretic reasons, have to be liberally sprinkled
	with infinite cardinals?  Doesn't this make you think that
	perhaps set theory is somehow obscuring simple ideas?

I don't know how to define "accessible category" without bringing
cardinals into the picture, but maybe I'm the last one to find out how,
as usual.  What's the trick?

	To my mind, the evidence suggests that despite its undoubted
	successes, set theory is not right for mathematical
	foundations, and we should be looking for its replacement.

Whoa, needle went negative there.  But I would have the same reaction to
a set theorist who claimed that categories were nothing but an
alternative language for the mathematics ordinarily and satisfactorily
treated by set theory.

("Alternative language for" is the polite code word some people use for
"weird way of talking about")

Set theory itself will only go away when the natural numbers go away.
Let's get real here.  The natural numbers are the very oxygen of
mathematics, and they are not going away in *any* foreseeable future.
Hence neither is the (internally) bicomplete topos of finite sets.
This topos is a very nice concrete way of working with natural
numbers---it makes numbers *more* categorical, not less, by letting you
transform them.

But sets *do* have to transform via arbitrary functions, there's no way
to wriggle out of *that* one!  Transforming sets with binary relations
neuters them, neutered sets are only good for the side lines.
*Converse* functions on the other hand are fine, if you're not Bill
Thurston, who eloquently expressed his inability to relate to Set\op at
UACT.

I don't care how the infinite sets are organized, just so long as
there's a way of doing it that doesn't make the logic that bears on my
life inconsistent.  I'm not planning on rubbing up against any infinite
sets personally without a sturdy layer of math and logic between me and
them.  You can seriously injure yourself with an infinite set.

Mathematics founded on set theory stays close to the air supply.  Any
religious upstart of a foundations claiming to offer a viable
*replacement* for set theory is going to have to argue real hard about
the disadvantages of breathing!

Whether we should work with sets and categories in exactly equal
proportions is an interesting question.  I tend to be slightly more
settish than cattish in my thinking, if only because I'm lazy and sit
around a lot, on the dime if not on the dot.  But there's not a big
gap.

Categories: can't live with sets, can't live without them.
Sets: can't live with categories, can't live without them.

Vaughan Pratt

PS.  No reactions yet to my ordinal-based definition of Set.  Main
thing I want to know is, is it old hat?  Second thing, is it good for
anything else besides what I made it up for, namely to shorten the
passage from function composition in Set to the membership relation on
ob(Set)?

I don't claim any more *significance* to the membership relation in my
version of Set than Mike Barr et al were claiming for other versions of
Set.  Well, maybe a little more: it is undeniably the membership
relation for ordinals, which is all my Set claims to contain
*explicitly*.  But is pi essentially an ordinal?  Of course not.  Can
pi exist in my Set?  No more or less than in anyone else's Set.  Is pi
made any more real by installing it in a category?  Rubbish.

---

From: categories <[email-masked]>
Date: Fri, 15 Mar 1996 14:43:31 -0400 (AST)

Date: Fri, 15 Mar 1996 08:53:57 -0500
From: Peter Freyd <[email-masked]>

There's certainly a clear distinction between "definition" and 
"semantics". They are -- to echo PeterJ -- in different categories.

But Vaughan's point about the calculus is well taken. I must back down
a bit. Yes, a semantics for the real numbers and for limits and for
continuity and -- hardest these days to believe -- for the very notion
of function were indeed needed by 19th C mathematicians.  So let me
try again. Core mathematics in the 20th C did not provide a problem
for semantics and for that reason the inadequacy of formal set theory
was not noticed. 

Inadequate for what? Well, let's start with the Church polymorphic
notion of number.

---

From: categories <[email-masked]>
Date: Sat, 16 Mar 1996 10:37:56 -0400 (AST)

Date: Fri, 15 Mar 1996 12:37:36 -0800
From: Vaughan Pratt <[email-masked]>

In his evening talk on Post some LICS' ago, Martin Davis told us of his
sense of revelation when he learned he'd been a computer scientist all
these years.

Now I know just how he must have felt.  What a relief to find I have
*not* been a semanticist all these years.

All I ask is a tall ship and a star to steer her by.  Definitions tell
us our position relative to both our destination and the rocks of
inconsistency.

Whatever semantics is, if the navigator says he can't do his job
without it we're lost.  Another round of semantics for the navigator.

	let's start with the Church polymorphic notion of number.

Of course when the navigator's had so much semantics he tells you he's
seeing double, you do worry a bit.  That semantics is heady stuff.

Vaughan Pratt

---

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

Date: Mon, 18 Mar 1996 10:44:32 +1100 (EST)
From: [email-masked]

After seeing the volume of "fluff" that this topic had generated on
Friday, I took a vow not to contribute any more to it. But 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.

Vaughan's definition is fine as long as you are happy, not just to
assume that the axiom of choice holds, but actually to rely on it
to construct codings for you. If AC doesn't hold, the Vaughan's
category fails to be cartesian closed; and even if it does, 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.

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.

By the way, the Cole--Mitchell--Osius equivalence between weak Zermelo
set theory and well-pointed topos theory, which is described in my
book (sorry Vaughan, but Academic Press won't reprint it) and in
Mac Lane--Moerdijk, doesn't assume the axiom of choice; it's an
"optional extra" which you can add to both sides of the equation
if you want to.

Peter Johnstone