FOM: "function" as a basic mathematical concept

[Stephen G Simpson]

A day or two ago I raised the question of whether "function" could be
considered as a basic mathematical concept, on a par with "set".  I
expressed skepticism about this, partly because I don't see how to do
real analysis in any foundational scheme based on functions,
comparable to real analysis in ZFC set theory.  In particular, I
expressed skepticism about the claims of topos theory.

Colin McLarty replies:
 > There is a large literature on real analysis in toposes, with
 > applications to classical analysis, Brouwer's analysis, and recursively
 > realizable analysis, among other topics. 
 >  
 > The best single reference would be Springer Lecture Notes in
 > Mathematics no.753, with many articles on real analysis. This was 
 > published in 1979. 

Ah yes, I remember this conference proceedings volume from the 70's.
Its title is "Applications of Sheaves".  The editors express
disappointment that analysis was not better represented at the
conference; nevertheless, the volume contains many interesting
articles about sheaves of real-valued functions on topological spaces.
At a quick glance I don't see any articles about real analysis in a
topos.  In fact, the volume doesn't seem to contain many articles
about topos theory at all.

Categories of sheaves are toposes, but the notion of topos is much
more general.  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.

Henk Barendregt writes:
 > I think one can defend that a system like lambda-PRED-omega is a
 > good candidate for a FOM based on functions.  See my paper in
 > vol. II Handbook of Logic in Computer Science, OUP for a definition
 > of that system. (Paper also available from
 > http://www.cs.kun.nl/~henk/papers.html)

Interesting.  I know that the idea of foundations of math based on
functions rather than sets was one of the original motivating ideas
for lambda calculus in the hands of Church, Curry, ....  I guess
Church et al didn't have much success with this idea, but now it has
apparently been revived.

 > What is your argument, Steve, that one cannot do analysis in a
 > topos?

I don't say that one cannot.  It's just that I don't know how to do
it in a satisfactory way.

-- Steve Simpson