FOM: topos theory qua f.o.m.; talk radio style

[Stephen G Simpson]

Steve Awodey writes:
 > The further questions Steve is asking, regarding the use of
 > excluded middle and choice in developing analysis in a topos, are
 > not essentially different in topos theory than in the context of
 > higher-order logic.  In particular, there's nothing new to be said.

Huh?  McLarty said that excluded middle and choice are not needed for
analysis in a topos.  According to McLarty, all that is needed is the
natural number object.  Are you backtracking on this?  Is McLarty?
I'm sure you can find something new to say.

[ Technical question: I'm confused about the mismatch between Cauchy
and Dedekind reals.  McLarty said this can happen in a topos with
natural number object.  Can it happen in higher-order logic? ]

 > Regarding the "motivation" for topos theory:

Why the quotes around "motivation"?  Don't you regard motivation as an
important issue?

 > this is also where the "general theory of functions" interpretation
 > that Steve alludes to comes in - say, as developed in Mac Lane's
 > "form & function" book.  Yet another motivation is the "variable
 > sets" interpretation developed by Lawvere; and following
 > Grothendieck's original lead, there's the geometric interpretation.
 >         Of course, these kind of remarks are terribly vague -
 > almost useless.  But there's plenty of good literature around 

Yes, your remarks are vague.  And yes, I'm sure there is plenty of
good topos literature around -- good by the standards of topos
literature.

You are ducking the motivation question.  The motivation question is:
Can you comprehensibly state the f.o.m. motivation for topos theory,
plus natural number object, plus whatever additional axioms are
appropriate to get enough real analysis to build airplanes?

It's very important to state this motivation right here, on the FOM
list.  The reason it's important is that here, on the FOM list, the
standards for stating f.o.m. motivation are much higher than they are
in the topos theory literature.  Here on the FOM list, you will be
under pressure to explain yourself in terms of general intellectual
interest.  That's not a requirement in the topos theory literature.

 > There's no disagreement between McLarty's statements and mine: he
 > was talking about sheaves on topological spaces and I mentioned
 > sheaves on (complete) boolean algebras.

McLarty wasn't talking only about sheaves on topological spaces.  He
was also talking about sheaves on posets and Grothendieck sites.
Complete Boolean algebras are posets.  I still say that you guys
need to communicate with each other and get your story straight.

 > The talk-radio style, inflammatory moderation on this list
 > (presumably intentional?) may elicit more postings, ...

Talk radio?  That's an interesting analogy.  I hadn't thought of it.

Sure, I'm trying to provoke thought and elicit good postings.  But I
also mean everything I say.  What you may not have understood before
is that some of us are passionately interested in f.o.m.

-- Steve Simpson