FOM: topos debate; IHOL; Brouwer; model theory; Pratt; Newton

[Stephen G Simpson]

About the recent topos debate: A number of people have tried to cast
this as a "CAT vs. SET" struggle, wherein category theory is allegedly
being presented as a competitor or alternative to set theory.  I think
this is the wrong way to view the matter.  We all need to remember
that category theory has its uses, e.g. in algebraic topology, and set
theory has its uses, e.g. in f.o.m. (= foundations of mathematics).
So let's try to redirect the discussion a little bit.  Serious
questions for the FOM list are: (1) What is the nature of set theory's
contribution to f.o.m.?  (2) What if anything can category theory
contribute to f.o.m.?  These two questions can be considered
independently of each other.

Several people have suggested that the topos debate is somehow
inappropriate or sterile.  I disagree.  I am finding it an excellent
vehicle to make some points about the nature of f.o.m., e.g. the fact
that coherent foundational motivation is crucial.  A byproduct is that
we are subjecting the foundational claims of topos theory to rational
examination.  For instance, the topos theorists are being forced to
clean up their act with respect to wild claims such as (i) topos
theory is a foundational alternative to set theory, (ii) there is no
problem about real analysis in a topos.

Jaap van Oosten writes:
 > If intuitionistic higher order logic is "perfectly respectable
 > f.o.m. research" then so is the study of its models, i.e.  topos
 > theory.

Van Oosten's implicit premise is that topos theory is identical with
the study of models of intuitionistic higher order logic.  That
premise is defective in many ways.  First, the language of topos
theory is very different from that of intuitionistic higher order
logic.  Second, the motivations are very different.  Third, the
methods of model construction are different.  Instead of grossly
oversimplifying by saying that topos theory = models of IHOL, it's
much more accurate to say that there are translations or connections
between topos theory and IHOL.

Topos people seem to think that if there are translations of X into Y
and Y into X, then X and Y are identical, i.e. the same subject.  This
is completely incorrect.  To give a mathematical example, there are
translations of group theory into ring theory (via "group rings") and
vice versa, but this doesn't mean that group theory is identical to
ring theory.  The motivation and the questions considered are very
different.

>From this perspective, I think I'm beginning to understand the false
idea underlying the wild claims about "categorical foundations".  The
idea seems to be that if X is foundationally interesting and X is
translatable into Y then ipso facto Y is foundationally interesting.
>From this point of view, topos theory might be thought to have extreme
foundational interest, because *both* set theory and intuitionism (and
maybe some other foundationally interesting stuff) are translatable
into it.  Never mind that the foundational motivation is lost!

 > One of the most illuminating examples of the usefulness of
 > toposes was, for me, Hyland's "effective topos".  ...

This is an example of how some topos research may contribute to
research in intuitionism, and thereby to f.o.m. research.  But to say
that topos theory = IHOL is not only incorrect, but very misleading.

 > 2. The definition of a topos (I don't bother about "fully formal"

Why don't you bother about "fully formal"?  Don't you see that this is
an important f.o.m. issue?  We need to get a fully formal definition
of topos on the table, in order to subject the foundational claims of
topos theory to rational examination.

 > > There is no way for the logically disinclined to study IHOL (=
 > > intuitionistic higher order logic). 
 > 
 > With all due respect, this is nonsense, as Brouwer himself was
 > certainly "logically disinclined".

Nonsense?  Don't you realize that IHOL is a species of logic?  How can
anyone claim to understand the motivation of IHOL outside of that
context?

Yes, Brouwer was logically disinclined; that's why he disavowed
Heyting's work and all other attempts to "formalize" intuitionism.
But IHOL grew out of and was motivated by Heyting's work.  To ignore
this is to ignore the nature of IHOL.

 > It would also discredit model theory ...

Why?  I hope everybody here knows that I would never seek to discredit
model theory.  In fact, I have published papers on model theory, and I
regard it as one of the important branches of mathematical logic and
one that has contributed mightily to f.o.m. research.  I prefer
model-theoretic (semantical) methods to proof-theoretic (syntactical)
ones whenever possible.  Both approaches are logical in nature.

Incidentally, we need to keep in mind that when the topos theorists
talk about a *model*, they are often referring to something that in
the context of mathematical logic would more appropriately be called a
*theory*.  This usage is also evident in Carsten Butz's posting of 29
Jan 1998 15:09:36.

 > all treatments of category theory (whether they want to be vague
 > about it or not) still depend on some primitive idea of "set".

Amen.

 > I think that a purely categorical foundation is possible (starting
 > with an appropriate axiomatization of CAT as a 2-category ...

OK, this is interesting.  I don't agree with this statement by van
Oosten, but I want to follow up on it.  The reason is, I'm hoping that
van Oosten can help us to understand Vaughan Pratt.  I carefully
studied Pratt's posting of 22 Jan 1998 12:11:44 claiming to explain
this, and I couldn't make head or tail of it.  The reason I think van
Oosten may be able to help is that Pratt also emphasized 2-categories,
indeed n-categories for arbitrary n.  Pratt's basic idea seems to be
that a morphism in a category should be regarded as something like a
directed line segment from the source object (left endpoint) to the
target object (right endpoint).  And decomposition of a morphism is
something like subdivision of a line segment.  But beyond that, I
wasn't able to grasp how Pratt's picture might lead to something that
could be called "a categorical foundation".  Can van Oosten explain
what in the world Pratt is talking about?

 > Soory, but I find "coherent conception of the mathematical
 > universe" highfaluting nonsense.  

Highfaluting nonsense?  Obviously I strongly disagree.  It's extremely
desirable to have a coherent conception of the mathematical universe.
Set theory is based on one such conception, viz. the cumulative
hierarchy.  Topos theory is not based on any such coherent conception.
Are you trying to hide this lack by casting doubt on the whole notion
of "coherent conception"?

 > Soory, but I find "coherent conception of the mathematical
 > universe" highfaluting nonsense.  We're like Newton, gathering
 > pebbles at the beach, with an ocean of knowledge, unexplored,
 > before us. We have no idea!

I'm somewhat shocked by this reference to Newton.  Let me try to
paraphrase it, and then you can tell me whether I understand you.
Here is what you seem to be saying: "The search for a coherent
conception of the mathematical universe (or a coherent conception of
anything) is misguided, because it doesn't take account of Newton's
insight that there a vast unexplored ocean of knowledge.  Standing
before this vast ocean, the appropriate attitude is awe, wonder, and
humility.  To strive intensely to know and understand by means of
coherent conceptions is is arrogant, irreverent, highfaluting, and
nonsensical."  Is that what you are saying?

My interpretation of Newton is very different from the above!

-- Steve