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

[Stephen G Simpson]

Colin McLarty writes:
 > >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.
 >     
 >     	No, not at all. The basis of my claim was that you can do
 > real analysis in any topos with a natural number object. In that 
 > generality the results are far weaker than in ZF (even without
 > the axiom of choice)--and allow many variant extensions with 
 > various uses. 

Darn, I thought I had finally pinned you down on this.  It sounded for
all the world as if you were saying that the axiom of choice is useful
for real analysis in a topos.  Now I don't know what the heck you're
saying.  I'm losing patience, but I'll try one more time.

My question is:

  What additional axioms are appropriate to add to topos theory to get
  enough real analysis to build bridges?  (By "enough real analysis to
  build bridges" I mean the standard undergraduate material on
  ordinary and partial differential equations, power series, Fourier
  analysis, etc., complete with applications, examples, etc.)

Since you have claimed that there is no problem about real analysis in
a topos, it should be easy for you to give me a straight answer to
this question.  Once you have done so, we can talk about whether topos
theory and/or the additional axioms have any f.o.m motivation.  But
first we need to get to the bottom of the above simple, but absolutely
basic, question.

I don't know why I am having so much difficulty getting you to give a
straight answer to this question.  Maybe you don't understand the
motivation for the question.  My motivation is actually very simple.
Namely, I want to subject the vague but frequently repeated
foundational claims of topos theory to rational examination.  A key
fact that is essential for the justification of orthodox ZFC-style
foundations is that ZFC suffices for real analysis: enough to build
bridges, and much more.  I want to know whether a similar key fact
holds for (some appropriate variant of) topos theory.

 > >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? ]
 >     
 >     	(a) holds in every category of sheaves (on a topological
 > space or indeed on any Grothendieck site). (b) holds for sheaves
 > on a topological space only for a narrow range of spaces--for
 > Hausdorff spaces it holds only when the space is a a single point.
 > (Even if you look at all Grothendieck sites, you get very few
 > more toposes satisfying (b).)

That's what I thought.  So sheaves may be a good motivation for topos
theory plus (a), but they provide no motivation for topos theory plus
(a) plus (b).

 > I think this is a crucial difference between set theory and
 > categorical foundations. Set theory has ONLY a foundational role in
 > mathematics. Category theory is used in many ways.

Here on the FOM list, the crucial question for topos theorists is
whether topos theory has ANY foundational role in mathematics.  From
the way this dialog with you is proceeding, I'm beginning to think
that it doesn't.  Or if it does, you aren't able or willing to
articulate it.

 > If there is some non-foundational use of topos theory, then topos
 > theory must be per se not foundational.

Not at all.  But it's far from obvious that topos theory has
foundational uses.  If you claim that topos theory has foundational
uses, you need to explain what they are.  You've failed to do that.

 > the example I gave was Abelian categories. Wondering whether they
 > are "important mathematics" would be like wondering whether the
 > compactness theorem is important in logic.

I wasn't wondering whether Abelian categories are "important
mathematics".  I know that Abelian groups and homomorphisms of them
are "important mathematics".  About whether Abelian category theory is
"important mathematics", I don't know or care.  I know enough about
Abelian category theory to know that it isn't important for my field,
f.o.m.  As to whether it's important for algebraic topology or
whatever, that's a matter for the algebraic topologists et al to
judge.  My guess is that it is marginally important for algebraic
topology, but I really don't care.

Similarly for topos theory.  If topos theory is "important
mathematics", the algebraic topologists et al will judge that by their
own standards.  I don't care about that.  What I do care about is
whether topos theory is of importance for f.o.m.  It probably isn't,
but I want to give you a chance to make your case, if you have one.

Topos theorists frequently make far-reaching but vague claims to the
effect that topos theory is important for f.o.m.  I have serious
doubts, but I don't understand topos theory well enough to know for
sure that topos theory *isn't* important for f.o.m.  I'm giving you a
chance to articulate why you think topos theory is important for
f.o.m.  So far, you haven't articulated it.

-- Steve