FOM: topos = IHOL

[Steve Awodey]

In reply to:
>
>Date: Fri, 30 Jan 1998 12:33:21 -0500 (EST)
>From: Stephen G Simpson <simpson at math.psu.edu>
>Subject: FOM: topos debate; IHOL; Brouwer; model theory; Pratt; Newton
...
>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.
...
>So let's try to redirect the discussion a little bit.
...
>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.

Some redirection!

        But my real comment is with regard to Steve Simpson's evident
misunderstanding of the notion of isomorphism:

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

You've missed the point:  the two translations must compose to give the
respective identity operations - do we need to recall the definition of
isomorphism?
        "Topos people" - and indeed most other mathematicians - do indeed
think that if two things are isomorphic, then there's not much point in
distinguishing between them.  The fact that you've missed this point is
clear from the subsequent example you give:

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

Not to mention the fact that not every ring occurs as a group ring!  An
accurate example of the situation that in fact obtains would be the
translations between (the theories of) boolean algebras and boolean rings.
Do you really want to insist that these theories are different in some
significant way?

The connection between topos theory and IHOL is of this kind.  It is as
tight as the connection between analysis conducted in English and analysis
conducted in German.  Carsten Butz spelled this out very clearly in his
posting from Thu, 29 Jan 1998.

Now, given that much of the debate of the last few days has turned on this
important point (i.e. the close connection between topos theory and IHOL)
which you apparently missed, perhaps you will want to at least reconsider
some of your strongly-held opinions, and qualify such claims as:

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

The inference you mention seems unproblematic to me, given the stronger
sense of "translatable" (not my choice of words) that we now see is at
issue.

Steve Awodey