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

[Colin McLarty]

Stephen G Simpson writes:

>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.

        It is "useful" for your goal of copying ZFC. It is incompatible with
other goals I mentioned. It is not *necessary* to real analysis in toposes. 

        Here are the relevant passages, showing I have said exactly this all
along:

        From my post of Tue, 13 Jan 1998 21:03:05

>>>       Anyone who likes to, may "doubt" that the elementary topos
>>>axioms can have any foundational role. But if you accept those
>>>axioms themselves, real analysis proceeds from there by exactly
>>>the same definitions as from the ZF axioms. Of course the results
>>>differ from the ZF results in the ways I mentioned before. If you
>>>require your topos to meet suitable further conditions you can
>>>get exactly the same analysis as in ZF or ZFC or whatever you like.

        Of course ZF does not use choice. You pursued the ZFC thread, saying
in your post of Wed, 14 Jan 1998

>>>>My question is, is it possible to develop real analysis in the general
>>>>topos setting, sufficiently to obtain these traditional applications?
>>>>Can we envision teaching and doing foundations of math in this way,
>>>>based on functions and topos theory, as opposed to or an alternative
>>>>to the orthodox way based on sets and ZFC?

        I answered in Wed, 14 Jan 1998

>>>       You can do real analysis in any topos with natural numbers. In
>>>general then the Cauchy and Dedekind reals will disagree. That disagreement
>>>has foundational interest (at least as much as any other study of
>>>constructive analysis) and applications to other mathematics (though, as I
>>>say, I don't know if it yet helps build bridges). 

        Still no mention of choice. But later in that post I mention
numerous kinds of real analysis in toposes, including kinds naively
intertranslatable with some set theories with choice:

>>>       In fact, you get a huge amount of classical analysis by taking the
>>>topos axioms, with natural numbers (i.e. an axiom of infinity) plus the
>>>axiom of choice (every onto function has a right inverse). This implies
>>>excluded middle. These axioms are equivalent (not only in consistency
>>>strength but via a rather naive translation) to some set theory--I think it
>>>is Zermelo set theory with bounded comprehension and choice. I should point
>>>out that another equally naive translation ties this same extension of the
>>>topos axioms to Aczel's Anti-foundational Axiom plus bounded comprehension
>>>and choice. 

        So, choice is used IF you want to copy set theories with choice.

        You declare your interest explicitly in your post of Wed, 14 Jan
1998 15:11:21

>>>>My point here is: How does topos theory stack up against ZFC?  

        That is a fine question, but please stop confusing my answers to
this question with my answer to "can you do real analysis in a topos?"

        When you ask me explicitly to compare toposes to ZFC my answer will
involve the axiom of choice in toposes. 

Colin