Re: Challenge from Harvey Friedman

Re: Challenge from Harvey Friedman

[categories]

Date: Wed, 28 Jan 1998 22:15:27 +0000
From: Carlos Simpson <carlos@picard.ups-tlse.fr>

Being a newcomer to the category list, I have a really naive and stupid question
(concerning H. Friedman's challenge). Namely, I was always under the impression
that you had to know what a set was before you could talk about what a
category was (in particular a topos). Is it possible to talk about toposes
without knowing what a set is?

This seems somewhat related to a question that has been bugging me for some
time, namely how to talk about a ``category''
which is enhanced over itself, but not necessarily having any functor to or
from Sets. The very first part of the structure would be a class of objects
O
together with a function (x,y)\mapsto H(x,y) from O\times O to O, but I
can't get beyond that.

---Carlos Simpson

Re: Challenge from Harvey Friedman

[categories]

Date: Fri, 30 Jan 1998 10:40:55 -0500 (EST)
From: Michael Barr <barr@triples.math.mcgill.ca>



Well the first question has an easy answer.  It is just as possible to
talk about a category without knowing what a set is as it is to talk about
a set without knowing what a set is.  Of course, you cannot talk about
homsets.  It is interesting to read the very first Eilenberg-Mac Lane
paper, which did not talk about homsets.  A set is an undefined notion and
there is a relation, epsilon that may hold between one set and another,
subject to certain axioms, one version of which Friedman listed.  A
category consists of undefined things called arrows and three relations,
two functional and the third partially functional (actually better than
that, but leave that aside).  Friedman's axioms are not coherent, as has
been pointed out, while the categorical axioms are.  On the other hand,
one can state Friedman's axioms, in all their glorious incomprehensibility
(I think I could stare at the 8th one from now until the middle of next
year without understanding what it says, and the 6th, asserted to be the
axiom of infinity is not much clearer) in a couple hundred words, while it
is pretty much necessary to interrupt the topos axioms for some
definitions (at least monic and subobject) to do the topos axioms.  Thus
each one looks simpler to its devotees and there is really no point in
arguing about it.

Michael

On Thu, 29 Jan 1998, categories wrote:

> Date: Wed, 28 Jan 1998 22:15:27 +0000
> From: Carlos Simpson <carlos@picard.ups-tlse.fr>
> 
> Being a newcomer to the category list, I have a really naive and stupid question
> (concerning H. Friedman's challenge). Namely, I was always under the impression
> that you had to know what a set was before you could talk about what a
> category was (in particular a topos). Is it possible to talk about toposes
> without knowing what a set is?
> 
> This seems somewhat related to a question that has been bugging me for some
> time, namely how to talk about a ``category''
> which is enhanced over itself, but not necessarily having any functor to or
> from Sets. The very first part of the structure would be a class of objects
> O
> together with a function (x,y)\mapsto H(x,y) from O\times O to O, but I
> can't get beyond that.
> 
> ---Carlos Simpson
> 
> 
> 

Re: Challenge from Harvey Friedman

[categories]

Date: Tue, 27 Jan 1998 11:26:45 +0000 (GMT)
From: Dusko Pavlovic <D.Pavlovic@doc.ic.ac.uk>

According to Harvey Friedman:

> I challenge anyone to write down their favorite fully formal axioms for
> topoi that are sufficient to do real analysis, so we can compare them side
> by side with the fully formal axioms I write down here.

The papers I announced here the other day do not offer any such
"dramatically simple" or "tremendously powerful" axioms, comparable
with Friedman's, nor indeed anything as politically engaged --- but I
think they may have to do with the issue.

Given a field in any category with enough limits, we implement
analytic functions, solve differential equations --- do quite a bit of
real analysis. It turns out that most of it can be captured as guarded
induction on final coalgebras.

We did not try to use this to embed real analysis in any fully formal
foundational theory, but to provide a uniform way of implementing it
on a computer, together with infinitary constructions and all. The
result may not be as "amazingly simple" as Friedman's axioms, but it
is fairly simple, and conceptually clear. Check it out (the last two
papers at http://www.cogs.susx.ac.uk/users/duskop/).

Sorry for the plug, but I actually want to make a point. I don't think
category theory should spend time trying to beat set theory on its own
territory of fully formal systems. Sets were invented in the time of
doubt about the consistency of mathematics, when foundations were
really sought for. Nowadays people go and prove Fermat Theorem.

Set theory wants to be something like a formal grammar of
mathematics. That is fine, can be very interesting in itself, but
great stories are usually told without thinking of grammar.

Category theory might perhaps do better to try to be some kind of a
programming language or mathematics, a set of object-(or better:
method-)oriented tools, conceptualizing large "software" projects of
the day.

How about that?

-- Dusko Pavlovic


PS On the other hand, us toposophers competing against them
setologists who can do analysis --- aren't we a bit like

        A Frenchman and an Englishman making the bet who can faster
        translate a sentence from German. Little Gretschen comes
        by and says: (fg)' = f'g + fg'...

I mean, didn't analysts tell *everyone* by now: THEY DO NOT CARE FOR
FOUNDATIONS. They do not think of their manifolds neither as sets of
little elements, nor hanging on a bunch of morphisms among other
manifolds. Most of the time, they are quite happy with their manifolds
as manifolds. Next time they need foundations, they'll invent them
again, like they invented sets and sheaves.

Re: Challenge from Harvey Friedman

[categories]

Date: Mon, 26 Jan 1998 17:36:31 -0500 (EST)
From: John R Isbell <ji2@acsu.buffalo.edu>

   P. S. Subramanian's 'A framework for measuring ...
complexity' is by H. Friedman and R. C. Flagg, Adv.
in Appl. Math. 11 (1990), 1-34 [MR91f:03111].
       John Isbell

Re: Challenge from Harvey Friedman

[categories]

Date: Mon, 26 Jan 1998 14:21:40 +0000 (GMT)
From: Ronnie Brown <r.brown@bangor.ac.uk>


How does Harvey Friedman know that the formulation of real analysis as 
carried out in set theory will do all that real analysis *should* do? 

My favourite example is that of partial functions. Most teachers of real 
analysis (calculus) rightly impress on students the importance of the domain 
of a function, 
and the domain of f+g, etc. So a student might think that the algebra and 
analysis of partial functions would occupy a good part of the literature. 
Solutions of ODEs (such as dy/dx=exp(-y) ) are often given by partial 
functions 
with domain involving a parameter, and the solution (including its 
domain) seems to vary smoothly with this parameter. In fact there is very 
little in the literature on such matters. I had a small go with 
29. (with A.M. ABD-ALLAH), ``A compact-open topology on partial maps with 
open domain'', {\em J. London Math Soc.} (2) 21 (1980) 480-486. 

It is not clear that the most general case of 
the functional analysis of partial functions with domain neither open nor 
closed can be successfully handled within classical set theory. There is 
a chance it can be handled within topos theory. (Try functions defined on 
the leaves of foliations. Any answers?) 

Another point of topos theory is to handle categories such as that of 
directed graphs in a similar manner to the category of sets, and to make 
comparisons between such categories. (Bill Lawvere has of course written 
a lot on this.) 

Ronnie Brown

Re: Challenge from Harvey Friedman

[categories]

Date: Mon, 26 Jan 1998 12:10:01 +0000
From: Steven Vickers <s.vickers@doc.ic.ac.uk>

>Topos theory with natural number object is insufficient to develop
>undergraduate real analysis - although many fom postings conceal this fact.
>One has to add to topoi: natural number object, well pointedness, and
>choice. The latter two are nothing more than slavish translations of set
>theory into the topos framework. The "idea" is to take a fatally flawed
>foundational idea and force it to "work" by transporting important ideas
>from set theoretic foundations.

The slavish translation of well pointedness and choice actually arises from
a more subtle slavish translation of point-set topology.

Point-set topology postulates that the points of a topological space can be
comprehended as a set, but this apparently innocuous idea is questionable
(perhaps we should be more sceptical about what sets can comprehend
following our experience with proper classes).

When we formulate our foundations based on the ideas of topos theory, and
interpret "set" as object in an elementary topos, then - given a natural
numbers object - we can ideed construct "sets of reals" but we find that
they misbehave. Normal theorems of analysis, such as Heine-Borel, fail
unless we also impose the additional ideas from set-theoretic foundations.

However, there is a different way of formulating topology, using locales or
"formal spaces", that works in any elementary topos (still need an NNO to
get the reals, of course) and preserves the validity of theorems such as
Heine-Borel. It works by addressing the topology directly, without regard
to what the opens in it might be sets of. It still has a concept of point,
but generalized point with respect to a varying set-theory (stage of
definition) instead in a fixed one. We can't take a single comprehension in
our favourite set-theory as encompassing all the points.

The moral is that a topological space is more than just a set of points
together with a topology of open subsets. If, for any reasons at all, we
are interested in doing mathematics constructively, then we should discard
point-set topology and use locales.

My picture of what is going on is this: when we try to make a set out of a
space by stripping off the topology, we damage the points, and we put the
well-pointedness and choice in as crutches and plasters to try to rectify
the damage we should never have done in the first place.

Steve Vickers.

Re: Challenge from Harvey Friedman

[categories]

Date: Sun, 25 Jan 1998 10:13 +0530
From: CAYLEY@tifrvax.tifr.res.in


	I remember to have seen a paper on frameworks for
	measuring complexity of mathematical concepts by
	two autors earlier. (I don't exactly recall where)
	but I also remeber that one of the authors was
	H.Friedman!

					P.S.Subramanian
					Tata Institute.

Re: Challenge from Harvey Friedman

[categories]

Date: Sat, 24 Jan 1998 15:59:46 +0000 (GMT)
From: Dr. P.T. Johnstone <P.T.Johnstone@dpmms.cam.ac.uk>

> But the axioms of elementary topoi are already incomparably more
> complicated than the axioms for set theory presented here.

What on earth does Friedman mean by complicated? As Peter Freyd
pointed out a long time ago, the axioms for an elementary topos are
essentially algebraic -- that is, they live at a very low level
of logical complexity. The very first axiom in anyone's (including
Friedman's) axiomatization of set theory is the axiom of
extensionality, which is not expressible even in coherent logic
(at least, not unless you take not-membership as a primitive
predicate, on the same level as membership).

Unless Friedman can put forward an objective measure of complexity
(as opposed to "unfamiliarity to H. Friedman") which justifies the
above quote, then his challenge is not worth considering.

Peter Johnstone

Re: Challenge from Harvey Friedman

[categories]

Date: Fri, 23 Jan 1998 21:22:39 -0500 (EST)
From: Michael Barr <barr@triples.math.mcgill.ca>

I guess simplicity is in the eye of the beholder.  For example, I do not
consider the categorical version of either choice (epis split) or
well-pointed (1 is a generator) to be translations of set theory, but
perfectly natural categorical axioms.  The point is that Harvey is a
set-theorist, so he thinks comprehension and all that stuff (which at
least 95% of all mathematicians could not state properly if their lives
depended on it) is perfectly natural and I don't.  

But my actual criticism of ZF(C) is much simpler.  I have taught these
courses in set theory and we spend a lot of time developing these epsilon
trees and then totally ignore the structure.  In other words, the epsilon
tree structure of sets is totally irrelevant to what you do with them.
There are a number of definitions of pairs, but they are irrelevant.  The
only thing we need to know about pairs (and the only thing a categoriest
does know) is when two pairs are equal.  All the defintions of pairs have
that property of course, but they also have irrelevant properties.

Mike

Re: Challenge from Harvey Friedman

[categories]

Date: Fri, 23 Jan 1998 16:32:35 -0600 (CST)
From: David Yetter <dyetter@math.ksu.edu>

Dear Fellow Categorists:

	I am personally not likely to take up Harvey Friedman's challenge, 
having long been doing "category theory as algebra" rather than "category
theory as foundations".

	I would like to point out, though that Friedman has deliberately chosen
as a test case real analysis, a subject which exists only to simulate the
existence of fluxions on the basis of foundations tied to two-valued logic.
How about asking Friedman to give an elegant, elementary foundation for
rings satisfying the Kock-Lawvere axioms?

	The use of an axiom schema in which arbitrarily complex formulae 
may be subsituted also seems a bit of a dodge.  At first glance, elementary
topoi plus  NNO, well-pointed and choice still doesn't need such things
(but I could be wrong, not having thought much about it for years).

Best Thoughts,
David Yetter
   

Challenge from Harvey Friedman

[categories]

Date: Fri, 23 Jan 1998 11:11:28 -0800
From: Vaughan Pratt <pratt@cs.stanford.edu>


I'm taking the liberty of forwarding to the categories mailing list
the following challenge posted by Harvey Friedman to Steve Simpson's
Foundations of Mathematics mailing list.

This is the latest in a long-running engagement about sets vs.
categories on the latter list, recent postings to which can be read at

	http://www.math.psu.edu/simpson/fom/postings/9801.html

Postings with "categor{y,ical}" in their subject lines are the relevant
ones.

Information about the fom list (how to subscribe etc.) can be found at

	http://www.math.psu.edu/simpson/fom/fom-info

As we were fond of saying quarter of a century ago,

Peace
Vaughan Pratt

------- Forwarded Message

Date: Fri, 23 Jan 1998 00:54:20 +0100
To: fom@math.psu.edu
From: Harvey Friedman <friedman@math.ohio-state.edu>
Subject: FOM: Set Theory Axioms

The point of this posting is to give some entirely conventional axioms for
set theory that are a bit simpler than many that are normally given. They
are fully formal. By comparison, look at the axioms of elementary topoi
that are given in MacLane/Moerdijk, Sheaves in Geometry and Logic, A first
Introduction to Topos Theory, Springer-Verlag, 1994, on p. 163. The
difference in complexity is strikingly grotesque.

I challenge anyone to write down their favorite fully formal axioms for
topoi that are sufficient to do real analysis, so we can compare them side
by side with the fully formal axioms I write down here.

Topos theory with natural number object is insufficient to develop
undergraduate real analysis - although many fom postings conceal this fact.
One has to add to topoi: natural number object, well pointedness, and
choice. The latter two are nothing more than slavish translations of set
theory into the topos framework. The "idea" is to take a fatally flawed
foundational idea and force it to "work" by transporting important ideas
from set theoretic foundations.

But the axioms of elementary topoi are already incomparably more
complicated than the axioms for set theory presented here.

Let me start with the dramatically simple axioms of finite set theory.
These amazingly simple axioms are tremendously powerful. We work in the
usual classical predicate calculus with equality and one binary relation
symbol epsilon - which we abbreviate here by "in." It is also useful to use
the constant symbol 0 (for the empty set), the unary function symbol { }
(for singletons), and the binary function symbol U (for pairwise union).
Note that axioms 2-4 amount to the most trivial of definitions.

1. (forall x)(x in a iff x in b) implies a = b.
2. (forall x)(not(x in 0)).
3. x in {a} iff x = a.
4. x in a U b if and only if (x in a or x in b).
5. [phi(0) & (forall x,y)((phi(x) & phi(y)) implies phi(x U {y}))] implies
phi(x).

Here phi(x) is any formula in the language in which y is not free.

That's all! One ***derives*** pairing, union, power set, foundation,
replacement, and choice, from these axioms alone!!! Also, when
appropriately formalized, "every set is finite" and things like "every set
has a transitive closure." These axioms are "practically" complete - an
informal concept that I have alluded to before on the fom.

Now for ZFC. We take a different tack and only use epsilon.

1. (forall x)(x in a iff x in b) implies a = b.
2. (therexists x)(a in x & b in x).
3. (therexists x)(forall y in a)(forall z in y)(z in x).
4. (therexists x)(forall y)((forall z in a)(z in y) implies y in x).
5. (forall x,y)(x in y implies (therexists z in y)(forall w in z)(w notin y)).
6. (therexists x,y)(x in y & (forall z in y)(therexists w in y)(z in w)).
7. (therexists x)(forall y)(y in x iff (y in a & phi)), where phi is any
formula in the language in which x is not free.
8. (forall x in a)(therexists y)(phi) & (forall x,y,z)((phi(x,z) &
phi(y,z)) implies x = y) implies (therexists w)(forall x in a)(therexists
unique y in w)(phi),

A novelty is the axiom of infinity, 6, is simpler than usual; and also
choice and replacement are combined nicely by 8. This allows such a simple
axiomatization in purely primitive notation. Try to right down the axioms
of a topos with natural number object, well pointed, and choice, in simple
primitive notation!! Good luck.

As is well known, ZFC is "practically" complete.

The version in the book on p.163 - which does not even include natural
number object, well pointedness, or choice - requires a very substantial
amount of preliminary abbreviations in order to formalize.



------- End of Forwarded Message