[cxm7@po.CWRU.Edu: Re: FOM: topos theory qua f.o.m.]

[Colin Mclarty]

Reply to message from simpson at math.psu.edu of Fri, 16 Jan
    
    
>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!)
    
    	You can see it as a general theory of functions if you like.
These functions come with pairing, like product types in computer
languages. We also require subtypes defined by equations, and subtypes 
can be defined in terms of functions: we require a specific type called 
Omega with a selected value 'true', such that ever subtype of any 
given type A has a characteristic function X (for upper case Greek chi)
such that the subtype is defined by the equation X='true'. And we
require function types.

	Are computer langauges too sophisticated to motivate a 
foundation? Current set theoretic foundations were motivated by 
arithmetized analysis, which seems no less sophisticated to me.

	Now for natural number objects: The picture is there should
be a type N whose functions to other types are defined by recursion.
Specifically N has a distinguished value 0, and a function s:N-->N,
and given any type B and a value x of B, and a function f:B-->B
there is a unique function u:N-->B defined by the recursion

			u(0) = x
			u.s  =  f.u

writing dots for composition, so u.s is the composite of u with s.

	I think you count recursion as a suitably foundational idea.


>
>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.
    
    	When I say "building bridges" I mean "designing and building 
bridges" and as you know that math is pretty weak. Compare Harvey's
surprizing work on math in finite initial segments of the cumulative
heirarchy. Every topos (even without natural numbers) includes 
equivalents to every finite initial segment of the cumulative 
heirarchy. In any topos with natural numbers these equivalents 
relate to the real numbers just as they do in sets. So you can see 
far more than enough math is available for building bridges.
    
>  My question is, how much reworking has been found
>necessary in the context of topos theory plus (a)?  
    
    	No reworking at all compared to the standard account in any
textbook on real analysis. You just can't prove as many theorems as
you could with stronger assumptions.
    
>And, where is this in print in reasonable
>detail?
    
    	The particulars of real analysis based just on the topos 
axioms plus natural numbers are not in print anywhere I know of, 
because the changes from the set theory case are trivial.
    
    	What is in print are the particulars of various non-classical
extensions, the ones with new un-ZF like features. You saw several
in the Springer Lecture Notes volume 753, but not knowing any topos
theory you will have trouble recognizing what they are doing. For
recursive analysis see chapter 24 of my book and references to
Hyland, Pitts, and Freyd in the bibliography.
    
    Colin