FOM: topos theory qua f.o.m.

[Stephen G Simpson]

Colin McLarty writes:
 > Steve Simpson writes:
 > > >   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.)
 > ...
 > Not to beat around the bush any longer let me give you a definitive
 > answer:
 > 
 >         You can do real analysis in any topos with a natural number object.
 > ...
 > You can do real analysis in any topos with a natural number object.
 > It opens up a lot of interesting and useful possibilities beyond
 > ZFC (of course ZFC is already terrific itself) plus you can keep
 > building bridges.

Thank you!  Excellent!  At last, a definitive answer to my question!

[ By the way, you keep saying that I am asking for a copy of ZFC.
Maybe Kanovei is asking for a copy of ZFC, but I am not.  Please
believe me.  I have said in other threads that I have no great love
for orthodox ZFC-style set-theoretic foundations. ]

Now, my next question is, what is the foundational picture motivating
the topos axioms plus axiom (a), the existence of a natural number
object?  Is it a picture of a general theory of functions?  Or some
other picture?  Maybe Peter Aczel would care to take a crack at this.
(Hi Peter, welcome to the discussion!)

Just as a footnote to this, I have some technical/bibliographical
questions.  Maybe all this is well known to topos theorists.  If so, I
apologize.  Anyway, here goes.

You have stated definitively that topos theory plus (a) is an
appropriate theory to do enough real analysis to build bridges.  On
the other hand, we know that topos theory plus (a) does not suffice to
imply (i) the Dedekind reals are the same as the Cauchy reals, (ii)
the law of the excluded middle.  Therefore, you are claiming that (i)
and (ii) are not needed to build bridges.  In other words, you seem to
be saying that the standard treatment of o.d.e., p.d.e., power series,
Fourier series, etc either doesn't use (i) or (ii) or can be reworked
to avoid them.  My question is, how much reworking has been found
necessary in the context of topos theory plus (a)?  What are the major
difficulties that come up?  And, where is this in print in reasonable
detail?  I'm looking for an elegant treatment.  Perhaps one can cite
Bishop/Bridges for at least some of this, after specifying an
appropriate translation.  Is that what you have in mind?

-- Steve