FOM: Re: three challenges for McLarty

[Steve Awodey]

This is a response to Steve Simpson's recent "challenge to McLarty".

        First of all, let me remind you that McLarty is not alone among
category theorists who believe the discipline is relevant to the
foundations of mathematics.  Shouting him down, or wearing him down, will
not make the issue go away.  It seems to me that a less personal, more
civil discussion would be more fruitful, for both sides.

        Be that as it may, let me try to briefly answer your points, in
order to help "depersonalize" this discussion:

>Challenge 1. McLarty needs to explicitly state fully formal axioms of
>topos theory plus natural number object etc.  These axioms are to be
>compared side-by-side with the very concise yet fully formal axioms of
>set theory which were posted by Harvey in 23 Jan 1998 00:54:20.  (The
>purpose of the comparison is to see that the set theory axioms are
>much, much simpler than the topos axioms.)

There's an obvious question of what is meant by "simple" here - perhaps
"familiar-looking to set theorists"?  Moreover, there is the question, what
the point of such a comparison is supposed to be.  That is, what is shown
by determining certain axioms to be more "simple", in one sense or another?
For example, the topos axioms are essentially algebraic, a condition that
can arguably be interpreted as a kind of logical simplicity (and is so
regarded by category theorists).  By contrast, ZFC does not have this
property (not even close).  Now what is this supposed to show?

>Challenge 2. McLarty needs to forthrightly concede that topos with
>natural number object is not sufficient for undergraduate real
>analysis, specifically the standard undergraduate material on
>calculus, ordinary differential equations, partial differential
>equations, power series, and Fourier series.

Are we going in circles here?  It was said very clearly by several
contributers that topos with NNO in fact does suffice.  Indeed, it does so
exactly as well as does intuitionistic, higher-order logic (IHOL).  If more
logical resources (e.g. excluded middle or choice) are required to give the
theorems included in your notion of "undergraduate real analysis", then
these resources can be added in a natural way, just as in IHOL.  This
seemed like a useful way of looking at the situation, for both sides.
Which part of this account are you no longer satisfied with?

>Challenge 3. McLarty needs to forthrightly concede that, as Harvey put it,
> > there is no coherent conception of the mathematical universe that
> > underlies categorical foundations in your sense.

This seems a strange way of trying to understand the categorists' point of view.

>Why doesn't McLarty come clean on these points?  McLarty's refusal to
>come clean on these points is hampering the discussion.  Several FOM
>subscribers have shown that they understand the nature and importance
>of these points.

What is this kind of bullying supposed to achieve?

        Let's try another tack, away from ZFC: We agreed (or at least you
didn't object to the fact) that general topos theory is - in a sense that
we can make more precise if need be - essentially the same as IHOL.  At
least it has the same expressive and deductive strengths.  Of course, the
usual style of presentation is rather different, but that's more a matter
of style and personal taste, and perhaps utility with respect to certain
kinds of questions.
        Now, presumably your objections against topos theory hold equally
against IHOL?
        Case 1: If not, please say what you consider the difference between
the two approaches to be. Is it merely the style of topos theory that you
object to?  If so, think of it as a way for those mathematicians who are
not logically inclined to study IHOL.
        Case 2: If so, what is your objection to IHOL?
        Case 2a: Lack of excluded middle (or axiom of choice). Then just
add them - to IHOL and to topos theory in essentially the same way.
Although I would argue that it's better to leave them out for foundations,
since there are interesting and useful theories that become inconsistent if
they are added.
        Case 2b: Maybe you find something objectionable in type theory.  I
guess a sets vs. types discussion could be useful.
        Case 2c: Something else?

        If you can say where this scheme breaks down, maybe we'll be able
to get a more useful discussion going.

Steve Awodey