FOM: categorical dys-foundations; evading challenges; intuitionism

[Stephen G Simpson]

Steve Awodey writes:
 > This is a response to Steve Simpson's recent "challenge to McLarty".

However, Awodey does not provide any specific information in response
to any of the three specific challenges.  See below.

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

Shouting McLarty down????  On the contrary, I'm providing him with a
wonderful forum in which he can give detailed explanations and
justifications for his wild claims about "categorical foundations", in
front of a large audience of f.o.m. professionals.

 > It seems to me that a less personal, more civil discussion would be
 > more fruitful, for both sides.

My remarks were not personal.  Anybody can take up my three
challenges.  But McLarty is the one who has been making wild claims
about "categorical foundations," and you and McLarty are evading.  As
for your complaint about civility, well, I would say that my three
challenges are rather pointed, but your complaint is only a smoke
screen hiding the fact that you, McLarty, and the other "categorical
foundationalists" have no answers.  It appears that "categorical
foundations" is nothing but bluff and bluster.

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

Note however that Awodey does not provide any specific information in
answer to any of my three points.

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

OK, so you want to divert this into a discussion of a notoriously
difficult and complex question -- what is the precise meaning of
"simple".

I and others think it would be more productive for you to explicitly
state the fully formal axioms for topos theory.  After that, we can
look at them and consider in what sense they are or are not simple.
Don't you think this would be a lot more to the point than embarking
on a discussion of the many possible meanings of "simple"?

If you insist on a precisely defined measure of simplicity, well, OK,
as a first approximation let's take "number of bytes".  We can refine
this later, but note that this crude measure is already interesting.
If it turns out that the fully formal topos axioms have 50 times as
many bytes as the fully formal set theory axioms, don't you think that
would be interesting?

You referred to "wearing McLarty down".  Do you regard Challenge 1 as
an attempt to "wear McLarty down"?  Is this because the fully formal
topos axioms will run to 20 pages of abstract nonsense?  I think
what's really on your mind is that you are afraid to state the fully
formal topos axioms on the FOM list, because f.o.m. professionals will
then see that they are not simple in any sense, by any stretch of the
imagination.

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

Instead of all this hot air, why don't you simply present the fully
formal statement of the topos axioms?  After that, we can talk about
"algebraic simplicity" or whatever else you want to talk about.  I am
going to want to talk about some things that you are probably *not*
going to want to talk about: motivation and general intellectual
interest.

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

Another evasion.  Awodey is simultaneously saying that topos with NNO
suffices, and that if it doesn't suffice, we can add more axioms to
force it to suffice.  Only he doesn't call them axioms.  He calls them
"logical resources" -- another evasion.  And he evades the fact that
these additional axioms are motivated solely by the topos theorists'
desire to, as Harvey says, slavishly translate ZFC into the inferior
topos notation.

 > Which part of this account are you no longer satisfied with?

I was never satisfied with any part of this account.  Right off the
top of my head, I can think of about 10 specific objections to this
account.  I feel like the proverbial mosquito in the nudist camp; I
don't know where to begin.

Here's one specific objection.  Consider the standard undergraduate
calculus theorem saying that every continuous real-valued function on
[0,1] has a maximum value.  This theorem is stated and applied near
the beginning of all freshman calculus books.  It's used in
optimization problems.  I surmise that it's a difficulty for
"categorical foundations", because it's probably not provable in topos
plus NNO.  That's because it's not provable in what you call IHOL,
because IHOL is consistent with "all functions from N to N are
recursive" and there is a well known recursive counterexample going
back to Specker.  (I am familiar with this kind of thing, because I'm
an f.o.m. professional.)

This one specific objection may be enough to topple McLarty's wild
claim that there is no problem about real analysis in topos plus NNO.
This is just one specific objection.  I can think of many more.

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

Understanding your point of view is only one objective here.  Another
is to subject the wild claims of "categorical foundations" to rational
examination.

I urge you to stop hiding behind accusations of incivility.  If you
think that there is a coherent conception of the mathematical universe
underlying your claims of "categorical foundations", please state that
conception.  Otherwise, please concede that there is no such
conception.

 > Let's try another tack, away from ZFC:

Again Awodey is evading.  All of my challenges concerned topos theory.
None of them concerned ZFC, except as a basis for comparison.

 > Now, presumably your objections against topos theory hold equally
 > against IHOL?

No.  Absolutely not.  IHOL makes excellent foundational sense, as a
logical analysis or working out of the consequences of Brouwer's
objections to nonconstructive existence proofs, his intuitionistic
philosophy of mathematics, etc.  In other words, IHOL has a serious
foundational motivation.

Topos theory has no foundational motivation.  Topos theory makes no
foundational sense.  This is one difference between IHOL and topos
theory.  There are other significant differences.

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

As explained above, it's not merely a matter of style, it's also a
matter of motivation.  Do the words "coherent motivation" mean
anything to you?

 > If so, think of it as a way for those mathematicians who are not
 > logically inclined to study IHOL.

There is no way for the logically disinclined to study IHOL (=
intuitionistic higher order logic).  If you leave out logic, you leave
out all of the motivation for IHOL, as well as much of the technique
and substance of it.

 > Case 2: If so, what is your objection to IHOL?

None.  It's perfectly respectable f.o.m. research.  Unlike topos
theory.

-- Steve