FOM: "function" as a basic mathematical concept

[Stephen G Simpson]

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.

I'm not at all interested in applications of topos theory or sheaf
theory to prove new theorems in Fourier analysis.  My question is, is
it possible to develop TRADITIONAL applications of real analysis,
including the TRADITIONAL rudiments of classical Fourier analysis,
within elementary topos theory.

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

I'm not asking these questions in order to embarrass topos theory.
I'm genuinely curious.

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

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

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.

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.

My point here is: How does topos theory stack up against ZFC?  We know
that ZFC is a well-motivated, plausible, natural set of axioms which
arise from a certain picture that we have in mind, namely the
cumulative hierarchy.  Are the elementary topos axioms equally natural
in this sense?  What is the picture giving rise to them, if any?  And
what about the extra axioms needed for real analysis?

 > The parable itself only refutes one purported argument that topos
 > theory depends on 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.

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?

-- Steve