FOM: "function" as a basic mathematical concept

[Colin McLarty]

>Colin Mclarty writes:
> > 	A given sheaf in one of the articles will be called
> > the "sheaf of real numbers" or "the sheaf of real-valued functions
> > on the reals"; precisely because it is constructed within its sheaf 
> > category the way the "real numbers" or "real-valued functions on the 
> > reals" are constructed within any topos. 
>
>Yes, I take the point.  For instance, the sheaf of real-valued
>functions on a topological space X is just the "real numbers" as
>interpreted in an appropriate topos, namely the topos of all sheaves
>on X.  In this sense, results about sheaves of real-valued functions
>can be viewed as applications of results about "reals" in a topos.

        More than that, they are so viewed by everyone I know of in the
field. The general theory leads the particular applications.

> > >I have my doubts as to whether general topos theory as
> > >a general theory of functions (if that's what it is) could provide a
> > >reasonably well-motivated foundation for real analysis, good enough
> > >for applications etc.  I'm not saying it can't be done, I'm only
> > >saying that I have my doubts.
> > 
> > 	Following my last paragraph, the motivation for real analysis
> > in general topos theory is not only as good as the motivations in
> > particular cases in SLNM 753: It IS the motivation for all of them,
> > and for many newer specific applications.
>
>I'm afraid there has been a misunderstanding, because I didn't express
>myself clearly enough.
>
>When I said "good enough for applications", I didn't mean applications
>to sheaf theory.  What I meant was, traditional applications of real
>analysis: ordinary differential equations, partial differential
>equations, Fourier series, building bridges, things like that.

        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.

        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. People
like Martin Hyland and others around Dana Scott have worked on getting
practical uses in computer science for this approach to recursive reals
(more generally to data types as "modest sets") but I don't know how
practical it is yet. 

 
> > The elementary topos definition of "Dedekind cut on the 
> > rational numbers" or "Cauchy sequence of rational numbers" is exactly 
> > the same as the ZF set theory definition.
>
>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.

>All right, so I
>guess my question becomes, what further assumptions on the topos are
>needed for a fuller development of real analysis?  I think you also
>said that further assumptions are needed to obtain equivalence of the
>Dedekind and Cauchy reals.

        You can do real analysis in any topos with natural numbers. In
general then the Cauchy and Dedekind reals will disagree. That disagreement
has foundational interest (at least as much as any other study of
constructive analysis) and applications to other mathematics (though, as I
say, I don't know if it yet helps build bridges). 

>  And more assumptions on the topos may be
>needed to obtain even something like intuitionistic real analysis

        Here it depends very much on which intuitionistic analysis you mean.
You can get models of numerous variants on free choice sequences, if you
want. Ieke Moerdijk has done that. Other versions are closer to Bishop's
constructive analysis, others to Markov's recursive analysis.

        It is not just a matter of accumulating stronger and stronger
assumptions. There are actually many incompatible assumptions you can study
separately. (Or they may be jointly trivializing, in the sense that two
assumptions can both be rather subtle while their conjunction is equivalent
to a much simpler assumption.) 


>even then I'm not sure that applications such as Fourier series are
>obtained.  Finally, may we not need even more assumptions on the topos
>to get something like the law of the excluded middle, so that we can
>apply our Fourier series to differential equations?

        It is an interesting question which assumptions are needed for which
results. I'm not expert on that but there are results.

>By this time, haven't we made so many assumptions that it's pretty
>much deja vu all over again, i.e. ZFC?  

        In fact, you get a huge amount of classical analysis by taking the
topos axioms, with natural numbers (i.e. an axiom of infinity) plus the
axiom of choice (every onto function has a right inverse). This implies
excluded middle. These axioms are equivalent (not only in consistency
strength but via a rather naive translation) to some set theory--I think it
is Zermelo set theory with bounded comprehension and choice. I should point
out that another equally naive translation ties this same extension of the
topos axioms to Aczel's Anti-foundational Axiom plus bounded comprehension
and choice.     

>I'm well aware that you can get something like ZFC by piling more and
>more axioms onto the elementary topos axioms.  But, there is a key
>question here: Are these additional axioms well-motivated in terms of
>the original motivation for the topos axioms?

        Well, "something like" is a pregnant phrase and we could argue all
day what is like what. As to the further axioms needed to make the topos
axioms naively intertranslatable with ZFC, these are known but to my mind
not as natural as either ZFC or the topos axioms. The project of relating
topos theory to ZFC is by definition derivative from both topos theory and
ZFC. I think it is a nice point in foundations, but not as immediate as
either of its two poles.
 
>I assume you are claiming that the original motivation for the topos
>axioms is to have a general theory of functions, since that was the
>context of this discussion.  That is your claim, isn't it?

        You had expressed doubts about the possibility of doing real
analysis in a topos. You did that in the context of discussing a general
theory of functions as a foundation. I think that is a fair connection to
make. Mac Lane even presents toposes that way in his book MATHEMATICS: FORM
AND FUNCTION. The "original motivation" for the topos axioms is a bit richer
than that, though. It seems like a bigger topic than we need to get into
here. I've written on it in "The use and abuse of the history of topos
theory" BRIT. JOUR. FOR PHIL. OF SCIENCE 1990, pp.351-75.

>
> > As Feferman has noted, if you want to extend the topos axioms to
> > copy some particular fragment or extension of the ZF axioms, then
> > you necessarily have that fragment or extension of ZF in mind. I
> > hope Pratt's Star Trek parable has convinced people that this does
> > not mean topos theory secretly depends on set theory.
>
>I forgot the Star Trek parable.  Could you please remind me, and
>explain why topos theory doesn't secretly depend on set theory?


        I don't know Star Trek so well, but Pratt's story involved
mathematicians from two different parts of the Galaxy who could not
understand each other's ideas at all. Finally one finds a way to express
itself so that the other can understand--and the other immediately concludes
"so, you did think like me all along but you tried to conceal it!" 

        The point is, that finding a translation between topos theory and
set theory does not make topos theory depend on set theory--any more than it
makes set theory depend on topos theory.

        The parable itself only refutes one purported argument that topos
theory depends on set theory. The general argument that category theory does
not so depend, has been done to exhaustion last fall on fom. (And the
special case of toposes makes little difference.) As far as I can see it
left partisans of each side exactly where they stood at the start--convinced
they were obviously right. I'll be talking about it at the Center for
Philosophy of Science in Pittsburgh, Feb.3. I'll post any new ideas that
come out of that.

best, Colin