FOM: topos theory qua f.o.m.; topos theory qua pure math

[Stephen G Simpson]

Let me try to summarize the current state of the discussion regarding
topos theory qua f.o.m. (= foundations of mathematics).

I started the discussion by asking about real analysis in topos
theory.  McLarty claimed that there is no problem about this.  After a
lot of back and forth, it turned out that the basis of McLarty's claim
is that the topos axioms plus two additional axioms give a theory that
is easily intertranslatable with Zermelo set theory with bounded
comprehension and choice.  The two additional axioms are: (a) "there
exists a natural number object (defined in terms of primitive
recursion)"; (b) "every surjection has a right inverse" (i.e. the
axiom of choice), which implies the law of the excluded middle.

[ Question: Do (a) and (b) hold in categories of sheaves? ]

OK, fair enough; the topos axioms plus (a) and (b) are enough for the
development of real analysis.  But then I raised two further
questions, which seem crucial: (1) Is there any foundational picture
that motivates the topos axioms?  (2) Can this same foundational
picture also be used to motivate the additional axioms (a) and (b)?

McLarty seems to be saying that the answers to (1) and (2) are "yes"
and "yes", but he declines to discuss it here on the FOM list.  OK,
fair enough.  Let's leave it at that, unless somebody else wants to
carry the ball.

To me, the question of foundational motivation is crucial.  For a
while I was wondering whether it might be possible to motivate topos
theory as "a general theory of functions".  But McLarty says that the
real motivation is much more complex.  Indeed, when we look at the
history, topos theory seems to have arisen from a strange mixture of
motivations.  One motivation is "sets without elements" a la Lawvere.
Another is "linear transformations without linearity" a la
Grothendieck/Lawvere.  Another is "logic without formulas" a la
Makkai/Reyes.

The whole thing is very confusing to a humble FOMer such as myself.

On the other hand, maybe I'm barking up the wrong tree.  Maybe topos
theory doesn't really have any f.o.m. motivation or content.  Maybe
topos theory is to be viewed as simply a tool or technique in pure
mathematics.  Maybe this is what McLarty had in mind when he said:

 > To category theorists beginning with Saunders MacLane it was
 > exciting, and it revamped all of homological algebra. Whether it is
 > "foundations" or not it is important mathematics.

In other words, don't judge topos theory from the viewpoint of f.o.m.
Judge it from the viewpoint of applications to pure mathematics:
homological algebra, algebraic geometry, etc.

My perspective is that of a mathematician specializing in f.o.m.  I
know something of homological algebra, algebraic geometry, etc, but I
don't know whether topos theory is "important mathematics" or not.
I'm willing to leave that question up to the intended clients of topos
theory, i.e. the algebraic geometers et al.  I assume they will
evaluate topos theory fairly based on their own standards.

-- Steve

PS.  McLarty mentioned MacLane's book "Mathematics: Form and
Function".  My impression is that, although MacLane in that book tried
to motivate topos theory as an f.o.m.-style general theory of
functions, in subsequent books he has backed off from that view.  This
would seem to confirm my hypothesis that topos theory isn't to be
evaluated as f.o.m.