FOM: Real analysis in a topos

[Colin Mclarty]

Reply to message from simpson at math.psu.edu of Mon, 12 Jan
>
>Has there ever been a decent
>foundational scheme based on functions rather than sets?  I know that
>some category theorists want to claim that topos theory does this, but
>that seems pretty indefensible.  For one thing, there doesn't seem to
>be any way to do real analysis in a topos.
>
	There is a large literature on real analysis in toposes, with
applications to classical analysis, Brouwer's analysis, and recursively
realizable analysis, among other topics. 

	The best single reference would be Springer Lecture Notes in
Mathematics no.753, with many articles on real analysis. This was 
published in 1979. 

	The definitions are exactly like real analysis in ZF. The
difference is that, because excluded middle and the axiom of choice 
fail in most toposes, the set of Dedekind reals is in general much
larger than the set of Cauchy reals. On the other hand, in the 
realizable case, even though choice and excluded middle fail, the 
Cauchy and Dedekind reals coincide because of the effective nature 
of the natural numbers.

	Interpreted in various particular toposes, the Dedekind and 
Cauchy reals get various meanings: in the topos of sheaves over a 
topological space they become continuous real-valued functions on 
the space and locally constant real-valued functions, respectively.
So the difference between them has a natural geometric sense.

--Colin McLarty