FOM: the exaggerated claims of topos theory qua f.o.m.

[Stephen G Simpson]

Background: McLarty in his posting

  156.  [[ Colin McLarty Jan 16 55/2053 "Re: FOM: topos theory qua f.o.m.; a
      quote from Mac Lane"]]

  http://www.math.psu.edu/simpson/fom/postings/9801.156

claimed that topos theory plus natural number object is an appropriate
foundational scheme for real analysis.  McLarty agreed to my
specification of "real analysis" as the standard undergraduate
material in ordinary and partial differential equations, power series,
Fourier series, etc.  This amount of real analysis was designated as
"enough real analysis to build bridges".

I had asked McLarty to explain the f.o.m. motivation, if any, of the
topos-theoretic treatment of real analysis.  McLarty replied in

  156.  {{ Colin McLarty Jan 16 55/2053 "Re: FOM: topos theory qua f.o.m.; a
     quote from Mac Lane"}}

  http://www.math.psu.edu/simpson/fom/postings/9801.156

and I now want to comment on this reply.

McLarty briefly recapitulates the definition of a topos with natural
number object.  He leaves out numerous details of that definition.
That's OK, but a more serious matter is that he also leaves out the
details of how various specific concepts of real analysis are to be
motivated in this setting.  For a sample of the kind of details that
occur in the orthodox set-theoretic treatment, see Harvey's posting

  FOM: Categorical Foundations
  Sat, 17 Jan 1998 21:06:04 +0100

McLarty leaves out all of the analogous details for his
topos-theoretic treatment.

By way of general motivation, McLarty briefly mentions the following:
(i) a general theory of functions, (ii) product types in computer
languages, and (iii) recursion.  I think this grab-bag would be hard
for undergraduates to swallow.  It's also hard for me to swallow.  For
me, the problem with this is that it's too much of a mixture.  There's
no clear picture of what the topos axioms are supposed to be "about".
In set theory, the picture is, sets.  In topos theory, the picture is
-- what?  There are too many wildly differing models for this to be a
viable educational and/or foundational option.

Let me try to state this contrast better.  The set theory axioms
(let's focus on Zermelo plus choice) specify a remarkably complete
picture, answering *all* of the questions about sets that are likely
to arise in the set-theoretic development of real analysis.  (Harvey
calls this "practical completeness".)  By contrast, the topos axioms
plus natural number object don't do anything like this.  If the topos
axioms plus natural number object are viewed as a description of an
intuitive picture of "collections and functions", then they are way
too vague.  For instance, they don't settle the question of whether,
if A is a collection and B is a subcollection of A, then A-(A-B)=B.
Undergraduates would be shocked if you told them that this is
questionable.

McLarty may view the existence of many different models as a virtue,
In my view, this excessive generality is not only educationally
unsound, but also incompatible with the foundational way of thinking.

Summary: In this first part of McLarty's posting, McLarty has made an
straightforward if inadequate attempt to present a little bit of
f.o.m. motivation for real analysis in topos theory plus a natural
number object.

However, the second part of McLarty's posting is a different story.

The second part of McLarty's posting is concerned with my question
about references/details for McLarty's earlier definitive claim that
"enough real analysis to build bridges" can be done with topos theory
plus a natural number object.  McLarty begins by waffling:

 > When I say "building bridges" I mean "designing and building 
 > bridges" and as you know that math is pretty weak.

In other words, McLarty is simultaneously backing off and not backing
off from the previously agreed-upon specification of "enough real
analysis to build bridges" in terms of standard undergraduate material
in o.d.e., p.d.e., power series, Fourier series, etc.

 > Compare Harvey's surprizing work on math in finite initial segments
 > of the cumulative heirarchy. Every topos (even without natural
 > numbers) includes equivalents to every finite initial segment of
 > the cumulative heirarchy. In any topos with natural numbers these
 > equivalents relate to the real numbers just as they do in sets. So
 > you can see far more than enough math is available for building
 > bridges.

So now it emerges that the basis of McLarty's claim is finite initial
segments of the cumulative hierarchy.  The full set of natural numbers
isn't even needed!
    
 > No reworking at all compared to the standard account in any
 > textbook on real analysis. You just can't prove as many theorems as
 > you could with stronger assumptions.

For instance, can you prove that every continuous real-valued function
on [0,1] has a maximum value?  What if the function is assumed to be
differentiable?  Such theorems are encompassed by the agreed-upon
definition of "enough real analysis to build bridges".  But it's a
wild claim and a gross exaggeration to say that such theorems are
present in a finite setting.  On the other hand, maybe that's not what
McLarty meant, since he's partially backing away from the agreed-upon
specification of "real analysis".  If so, then what did he mean?  Did
he mean that the maximum principle etc are provable in topos plus
natural number object?

By this time, the fog is pretty thick.  I'm reminded of squids that
squirt clouds of ink to evade their pursuers.

McLarty continues:

 > The particulars of real analysis based just on the topos axioms
 > plus natural numbers are not in print anywhere I know of, because
 > the changes from the set theory case are trivial.

"The changes from the set theory case are trivial?"  What replaces the
A-(A-B)=A?  What replaces the idea that sets are made of elements?
Now I'm really losing patience!

I guess by now it's clear to all 280 FOM subscribers that the grossly
exaggerated claims of topos theory qua f.o.m. are bankrupt.  I'm not
sure it's worth continuing this.  Maybe I'll continue it, just to show
everyone the extent of the bankruptcy.

-- Steve