FOM: "function" as a basic mathematical concept

[Colin McLarty]

>Colin McLarty writes:
> > Applications of sheaf theory are traditional by now. They've been
> > around half a century, and they are used for all the things you
> > name--except possibly Fourier series. I don't know applications
> > there but I wouldn't expect to since I don't know much about
> > Fourier analysis.
>
>I guess my question still isn't clear.  I'll try once more.

        Yes, I was confusing the question "can you do this" with "are there
known research benefits to doing this". Certainly you can do it.

> > Now if you ask "How far are foundational presentations of real
> > analysis in a topos used to build bridges" I'd guess not very far.
>
>I'm not asking whether they ARE so used.  I'm asking whether it's
>POSSIBLE IN PRINCIPLE to so use them.

        Well, I mentioned that these techniques apply to things like solving
differential equations. So I intend that as a Yes. 

>  In other words, I'm asking
>about the project of using topos theory as an alternative foundational
>setup for mathematics, replacing the orthodox setup, ZFC.  I'm
>wondering what will happen when you try to set up the rudiments of
>real analysis, in the elementary topos setup.  Will you get enough
>real analysis to build bridges?  Or will you get a horrible,
>ill-motivated mess that nobody can make sense out of?

        If you do it in a topos with natural numbers and choice, no one but
a logician will be able to distinguish the result from real analysis in ZFC.

        Of course if you take another version, modelling one of Brouwer's
notions of free choice sequence--then Brouwer might think the result lovely
but I guess most people would call it a mess. Brouwer's theory is a mess to
most people. 


> > >I think you already said that this requires special assumptions on the
> > >topos, e.g. the existence of a natural number object.
> > 
> > That is no very special assumption. And ZF has to use its axiom of
> > infinity for the same purpose.
>
>Well, I wonder.  How special is it, given the original motivation for
>topos, especially if we are talking about topos theory qua general
>theory of functions?

        It is precisely as natural as the claim: There is an object whose
functions to other objects are defined by primitive recursion. You might
like to do topos theory without it (as you might like ZF without an axiom of
infinity) but it is also natural enough to include it.  

> > It is an interesting question which assumptions are needed for which
> > results. I'm not expert on that but there are results.
>
>OK.  So this means there is a lot more work to do before you can say
>that there are no doubts or problems about real analysis in topos
>theory.  Right?

        No. We know a lot of topos axiomatizations for various kinds of real
analysis, including full classical real analysis. And I don't know much
about fragments of those axioms.

        Did you doubt the possibility of doing real analysis in ZF before
you learned of reverse mathematics?  

>By "something like ZFC" I simply meant something intertranslatable
>with some reasonably rich fragment of ZFC, e.g. Zermelo set theory, or
>maybe Zermelo set theory with comprehension only for bounded formulas.

        Tbat is exactly what I went on to discuss in the post you are
replying to. I also mentioned Axcel's Anti-foundational axiom with bounded
comprehension.
 
>
>But you didn't address my key question, about whether the additional
>axioms that are needed for real analysis are well-motivated in terms
>of the original motivation for the topos axioms.

        I thought I did. I also answered your question about whether the
axioms needed to get exactly the same analysis as ZFC are as well motivated
as the basic topos axioms. To the "key question", yes. To the other
question, I say no. But you don't have to take my word for it. I think the
axiom scheme of replacement is less natural than either Zermelo set theory
or topos theory--
anyway its motivation is just about the same in topos theory as in Zermelo
set theory. 

>Historically I think a lot of topos theory developed as a sort of
>"category theorist's reaction of set theory".  One of the motivating
>examples was the category of sheaves of sets over a topological space.
>But I grant it's hard to unravel these historical motivations.

        You can find books and articles supporting your view of the history.
The thing is, the people who did this are still living and you can talk to
them. You can also read their publications. You get a very different picture.

        The "category theorist's reaction to set theory" was Lavwere's 1963
theory of the category of sets--before he knew of toposes. It led to only a
little activity, and it was no major project of his either (he did it as a
handout in freshman calculus at Reed College, where calculus is supposed to
include foundations). Most category theorists were uninterested in it since
it just seemed like a reaction to set theory.

        Grothendieck's 1957 theory of linearity, the Abelian categories I
have written of before, provoked more action. Lots of category theorists
were trying to generalize them around 1960 in various ways. This stuff can
all be codified in set theory if you like, but that won't show you what it
is about. In particular, a key idea here is duality: If you have an Abelian
category *A* you can form its opposite *Aop*. An *Aop* arrow f:A-->B is
simply an *A* arrow the other way B-->A. Then *Aop* is also Abelian.

        To a set theorist this probably does not look very exciting. Who
cares if you look at functions from a set A to a set B, or from B to A? You
can look at both. So what? That is why set theorists are not category
theorists (with some few exceptions? Dana Scott? Andreas Blass? Vaughan
Pratt?). To category theorists beginning with Saunders MacLane it was
exciting, and it revamped all of homological algebra. Whether it is
"foundations" or not it is important mathematics.

        Lawvere's goal in particular was to start with something like the
Abelian category axioms and get away from the linearity--only as a secondary
goal to start with sets and get away from the constancy.

        Grothendieck's topos theory was a categorically minded geometer's
reaction to local homeomorphisms--including the fact that they can be
represented by sheaves but also their geometric character.

        Now, sheaves of sets on a topological space may have suggested
Boolean valued models of set theory. (Did they? I don't know about that.)
And Boolean valued models encouraged Lawvere around the time he began
looking at Grothendieck's topos theory. But Lawvere himself felt his earlier
categorization of set theory suffered from being too close to set theory. So
it was only years later, after he and Tierney had axiomatized topos theory,
that they went back and saw how their theory incorporated BVMs and Lawvere's
early category of sets.  

>My real question is about the foundational motivation, here and now.
>Is topos theory backed up by a motivating story as a general theory of
>functions which is supposed to be adequate for all of mathematics?
>The paradigm here is ZFC, which does have a well-known
>f.o.m. motivation as a general theory of sets which is adequate for
>all of mathematics.  How does topos theory stack up to ZFC?

        I am not going into the whole thing now. But I will give a fragment
you might or might not want to think about. Can you understand the
motivation of someone who defines the product BxC of two sets B and C this
way: "It has as many elements as there are pairs <b,c> with b an element of
B and c an element of C"? I mean that is the definition, there is nothing
more to say. We do not say the elements of AxB "are" the pairs or anything
else. We just know how many there are.

Colin