FOM: topos theory qua f.o.m.

[Stephen G Simpson]

I wrote on January 14:
 > I'm wondering what will happen when you try to set up the rudiments
 > of real analysis, in the elementary topos setup.  Will you get
 > enough real analysis to build bridges?  Or will you get a horrible,
 > ill-motivated mess that nobody can make sense out of?

Vaughan Pratt immediately replied:
 > I would expect a mess, but one no less horrible than what you get
 > by setting up real analysis in the ZFC setup.  It is one thing to
 > claim that it can be done, but it is all too easy to underestimate
 > the complexity of the passage from such an in-principle claim to
 > its actual realization.

Pratt is being cryptic, but I guess he is referring to the well-known
difficulty and enormous length of completely formalized proofs in
almost any formal system based on first-order logic.  This is a valid
point, and there are a lot of interesting questions at this level of
completely formalized proofs.  I'll defer to others who know more
about this than I.  

However, my question was at a different level.  I was referring to
what Pratt is calling the "in-principle" level.  "In-principle", we
all know how to set up real analysis in ZFC.  But to me at least, it's
not so clear how to set it up in elementary topos theory, even
"in-principle".  Recall that some developments of intuitionistic
analysis are horribly messy and seem to leave us with no way to obtain
even the standard rudiments of engineering mathematics.

In the meantime, McLarty has stated definitively that elementary topos
with a natural number object is the correct setting for this kind of
real analysis.  I'm not sure of the details, but McLarty claims to
have them.

-- Steve