FOM: IHOL vs topos; Boolean algebra vs Boolean ring; topos challenges

[Stephen G Simpson]

Steve Awodey 31 Jan 1998 10:40:55 writes:

 > ... Steve Simpson's evident misunderstanding of the notion of
 > isomorphism ...

Awodey has shifted the terms of the discussion.  Until now, Awodey and
I weren't talking about "isomorphism".  We were talking about alleged
translations of IHOL (= intuitionistic higher order logic) into topos
theory and vice versa.

 > ... the two translations must compose to give the respective
 > identity operations ...

This is incorrect; see below. 

 > ... do we need to recall the definition of isomorphism?

What does "isomorphism" have to do with it?  Is Awodey now saying that
IHOL is "isomorphic" to topos theory (in some unspecified sense)?

Awodey is relying on Carsten Butz's posting of 29 Jan 1998 15:09:36,
in which Butz partially explained the nature of some alleged
translations between IHOL and topos.  Note however that Butz and
Awodey haven't explained exactly what they mean by IHOL.  I expect
that, if pressed, they would define IHOL in a way that would be in
some sense equivalent to topos.  However, I'm not at all sure that it
would be compatible with Heyting's foundational ideas.  For example,
Butz's sketch of IHOL doesn't mention propositional connectives and
quantifiers, which would be essential in any Heyting-style
intuitionistic system.

Furthermore, the alleged "equivalence" or "isomorphism" between topos
and IHOL is rather loose.  According to Butz, If you start with IHOL
and translate to topos and then back to IHOL via the translations
considered by Butz, you don't get the same IHOL.  What you get is some
sort of maximal extension by definitions.  Evidently a lot of
structure has been lost.

 > An accurate example of the situation that in fact obtains would be
 > the translations between (the theories of) boolean algebras and
 > boolean rings. 

Note first that Boolean algebras are not isomorphic to Boolean rings.
Now, if Awodey were to claim that the theory of Boolean algebras is
isomorphic to the theory of Boolean rings, I *might* agree.  But I'd
have to be cautious, because when a category theorist says "two
theories are isomorphic" he may mean various things, depending on what
category of theories is under discussion.  Since Awodey hasn't
specified the category that he is talking about, it's hard to tell
what he means by "isomorphic".  Note also that "theory" has an unusual
meaning for topos people; see Makkai/Reyes.

 > Do you really want to insist that these theories are different in
 > some significant way?

Well, I concede that any proposition about Boolean algebras has a
counterpart for Boolean rings, and vice versa, so there is a close
relationship.  However, these two subjects have very different
motivations.  I regard motivation as significant.

Actually, I can use this to make a point about the motivation of
topos theory.

Historically, where did "Boolean algebra" and "Boolean ring" come
from?  Boolean algebra was invented by George Boole in order to
analyze logical reasoning, what we now call propositional logic.  The
notion of Boolean ring was invented much later, by nameless ring
theorists, for their own purposes.  One of their purposes was to
subsume Boolean algebra under ring theory, in order to be able to say
that "logic is just a branch of ring theory", as one prominent
algebraist told me.  This is incredibly crass, because it ignores
Boole's original motivation.

Similarly, topos theory was invented by algebraists for their own
purposes.  One of the purposes was to subsume set theory under
category theory, via a slavish translation.  The translation
accomplishes nothing, except to enable algebraists to talk about
"categorical foundations", while obliterating the f.o.m. motivation
that underlies set theory.

Butz 29 Jan 1998 15:09:36 writes:
 > we write very often for simplicity Sets for this base-topos.

I think Butz is saying that a base-topos is called "Sets" even if it
doesn't consist of sets and functions.  Doesn't this cause endless
confusion?  Remarkable!  It strikes me as a perfect illustration of
the true nature of the relationship between topos theory and set
theory.

Incidentally, I answered some of Butz's and Awodey's questions in
private e-mail to Butz, which Butz quoted in his posting.  In that
exchange, I said that IHOL is motivated by an analysis of Brouwer's
intuitionistic ideas for f.o.m.  Butz replied:

 > Well, I don't care too much about the "original" motivation, ...

A revealing remark.

-- Steve

PS on topos challenges:

I'm glad that McLarty (30 Jan 1998 12:46:45) has answered the first of
my three topos challenges (24 Jan 1998 20:16:05), by posting a fully
formal definition of topos.  It's 1868 bytes long and uses 13
primitives, compared to 299 bytes and three primitives for finite set
theory.  I'm pleasantly surprised!  Another comparison: 2437 bytes and
13 primitives for topos with extra axioms, versus 646 bytes and one
primitive for ZFC.  Does Awodey want to discuss other measures of
simplicity?

My second and third topos challenges haven't yet been answered.  They
concern real analysis and motivation, respectively.