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

[Colin Mclarty]

Reply to message from simpson at math.psu.edu of Thu, 15 Jan
>
>Let me try to summarize the current state of the discussion regarding
>topos theory qua f.o.m. (= foundations of mathematics).
>
>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. 
    
    	If you want to copy the ZFC case pretty nearly (so closely 
that only a logican could tell the difference) then you will want 
a topos with numbers and choice. To copy the ZFC case exactly you 
want a topos with numbers, choice, and replacement.
    
    	Now some people will say "See, topos foundations just copy
set theory!". A more apt conclusion would be "If you ask for copies
of set theory, then yes--topos foundations can give them".    
    
>  The two additional axioms are: (a) "there
>exists a natural number object (defined in terms of primitive
>recursion)"; (b) "every surjection has a right inverse" (i.e. the
>axiom of choice), which implies the law of the excluded middle.
>
>[ Question: Do (a) and (b) hold in categories of sheaves? ]
    
    	(a) holds in every category of sheaves (on a topological
space or indeed on any Grothendieck site). (b) holds for sheaves
on a topological space only for a narrow range of spaces--for
Hausdorff spaces it holds only when the space is a a single point.
(Even if you look at all Grothendieck sites, you get very few
more toposes satisfying (b).)
   
>OK, fair enough; the topos axioms plus (a) and (b) are enough for the
>development of real analysis.
    
    	I.e. they are enough to copy real analysis in ZFC rather well.
They are much more than you need for other variants.
    
> But then I raised two further
>questions, which seem crucial: (1) Is there any foundational picture
>that motivates the topos axioms?  (2) Can this same foundational
>picture also be used to motivate the additional axioms (a) and (b)?

	I'm working on an answer to this--that is, an answer shorter
than my book plus all my philosophic articles. A salient point: my
goal is not to motive "the topos axioms" by themselves. There is a large
and branching family of axiom systems, all extensions of the category
axioms. So there is a large and branching family of motivations for
various ones of them as fom--not all of the axioms systems, of course,
have interesting fom motivations.

	Set theorists, I think, already find this kind of thing odd.
To them, we have one mathematics, it needs one foundation, and that 
should be one theory. Of course set theory actually embraces many
variants--ZF, NF, Feferman's collections and operations, numerous
extensions of ZF, numerous restrictions of 2nd order Peano arithmetic.
But these are not at all so vastly disparate as extensions of category 
theory nor so organically related to each other as those extensions.
So it leaves a different mind set.
    

>Indeed, when we look at the
>history, topos theory seems to have arisen from a strange mixture of
>motivations.  One motivation is "sets without elements" a la Lawvere.
>Another is "linear transformations without linearity" a la
>Grothendieck/Lawvere.  Another is "logic without formulas" a la
>Makkai/Reyes.

	This list made me think! When I saw "set theory without elements"
I thought, okay, but that's an obvious enough idea isn't it? But don't
worry about my sanity, I quickly recalled it seems odd to a lot of people
here. As to "linear transformations without linearity" I thought
well of course there's linearity, he himself said "linear transformations"
--but then understood that by "linearity" Steve means "linear spaces".
As to "logic without formulas", that's not so much my domain and I guess
my feeling about it is closer to Steve's than on the other issues. But
it does make sense--I wonder if older logicians were bothered when Tarski
and others began talking about "theories without axioms" (i.e. theories
as deductively closed sets of formulas, but with no subset of those
formulas selected as the axioms)?


>On the other hand, maybe I'm barking up the wrong tree.  Maybe topos
>theory doesn't really have any f.o.m. motivation or content.  Maybe
>topos theory is to be viewed as simply a tool or technique in pure
>mathematics.  Maybe this is what McLarty had in mind when he said:
>
> > To category theorists beginning with Saunders MacLane it was
> > exciting, and it revamped all of homological algebra. Whether it is
> > "foundations" or not it is important mathematics.
    
    	I think this is a crucial difference between set theory and
categorical foundations. Set theory has ONLY a foundational role in
mathematics. Category theory is used in many ways.
    
    	So set theorists tend to think of each given theory (ZF, group 
theory, Feferman's theory of collections and operations, topos theory
....) as either BEING foundational or NOT BEING. If there is some
non-foundational use of topos theory, then topos theory must be per
se not foundational. So when Steve sees me say that Abelian categories
are important even if you do not take them as a foundation, he thinks
I might mean they are not a foundation. To me this is a complete
nonsequitur.
    
    
>My perspective is that of a mathematician specializing in f.o.m.  I
>know something of homological algebra, algebraic geometry, etc, but I
>don't know whether topos theory is "important mathematics" or not.
>I'm willing to leave that question up to the intended clients of topos
>theory, i.e. the algebraic geometers et al.  I assume they will
>evaluate topos theory fairly based on their own standards.
    
    	Yes, and they do argue it still. But the example I gave was
Abelian categories. Wondering whether they are "important mathematics"
would be like wondering whether the compactness theorem is important 
in logic.
    
>PS.  McLarty mentioned MacLane's book "Mathematics: Form and
>Function".  My impression is that, although MacLane in that book tried
>to motivate topos theory as an f.o.m.-style general theory of
>functions, in subsequent books he has backed off from that view.  This
>would seem to confirm my hypothesis that topos theory isn't to be
>evaluated as f.o.m.
    
    	He certainly discusses non-foundational uses of topos theory
in his book with Moerdijk. To conclude that he has backed off
from their foundational role would be the "set theorist's nonsequitur"
I discussed above about myself and Abelian categories. He has not in 
fact--but recall he thinks all
foundations are provisional, good for a lot of things, but no one
of them is actually necessary for people who want to do math.

Colin