FOM: "function" as a basic mathematical concept

[Stephen G Simpson]

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.

 > >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.

My question is, is it possible to develop real analysis in the general
topos setting, sufficiently to obtain these traditional applications?
Can we envision teaching and doing foundations of math in this way,
based on functions and topos theory, as opposed to or an alternative
to the orthodox way based on sets and ZFC?  I'm not saying this can't
be done; I'm just asking questions, expressing doubts, etc.

 > 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.  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.  And more assumptions on the topos may be
needed to obtain even something like intuitionistic real analysis, and
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?

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

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?

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?

 > As Feferman has noted, if you want to extend the topos axioms to
 > copy some particular fragment of 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?

-- Steve