FOM: constructive analysis; topos confusion; set theory alienation

[Stephen G Simpson]

I wish to thank Carsten Butz (4 Feb 1998 15:20:28, 16:12:30) for
taking a stab at my questions about real analysis in a topos.
Obviously this is an uncomfortable topic for topos theorists!

If I may summarize what Butz said, many basic theorems of real
analysis don't go through in a topos with natural number object, the
situation being roughly as for intuitionistic or Bishop-style
constructive analysis.  In addition, Butz remarks that the
difficulties can be overcome by making extra assumptions,
e.g. specializing to Boolean topos, or perhaps Boolean topos with the
axiom of choice.

I would remark that (i) the extra assumptions that Butz proposes are
very specialized from the viewpoint of topos theory, (ii) these extra
assumptions seem very difficult to motivate from the viewpoint of pure
topos theory, outside the context of set theory.  So I don't think
there is much left of "topos-theoretic foundations", at least as
regards real analysis.  Of course I do appreciate the applications of
topos theory to algebraic geometry, sheaf theory, etc. that Butz has
pointed out.  I'm only criticizing "topos-theoretic foundations", not
topos theory as a perhaps useful tool in pure mathematics (algebraic
geometry etc).

 > ... what is needed to "build bridges"? Constructive analysis should
 > be enough, I guess, but may be (compared to classical real
 > analysis) one sometimes has to do some more work constructively.

I regard this as an interesting question.  Bishop's book "Foundations
of Constructive Mathematics" (see also Bishop/Bridges) went a
considerable distance toward demonstrating the viability of
constructive analysis for "building bridges" etc.  I've heard it said
that Bishop felt frustrated because his constructive approach was not
widely adopted in university mathematics courses.  On the other hand,
I can understand why it wasn't adopted, because in my opinion Bishop's
treatment of analysis is too cumbersome at some key points, e.g. the
maximum principle.

Butz asks:
 > Would they agree that Brouwer or Bishop would have been able to
 > build a bridge?  

I don't think this is the right question.  A better question is: Would
Brouwer or Bishop have been able to build a bridge using
intuitionistic or constructive mathematics?  There is a big difference
between these two questions, because Brouwer and Bishop (and many
other constructivistically inclined mathematicians) were quite
familiar with classical methods and used them in their own very
significant mathematical research.  For instance, Brouwer's fixed
point theorem is not valid intuitionistically or constructivistically.
(There is a recursive counterexample due to Orevkov.  In reverse
mathematics it is shown that the Brouwer and Schauder fixed point
theorems are equivalent to weak K"onig's lemma.)  Similarly for some
of Bishop's theorems on function algebras, I think.

I have my doubts about whether intuitionistic and/or constructive
mathematics is "enough to build bridges".

Butz wrote:
 > McLarty has given axioms for toposes. I intended once to do this as
 > well, but I would not have pressed myself in the corset of first
 > order logic, but would have used our ordinary language.

I'm not sure what Butz means by "our ordinary language".  McLarty's
first order axioms (FOM posting of 30 Jan 1998 12:46:45) seem
reasonably clear (although Riis and I remain skeptical about some
aspects).  I have my doubts about whether an "ordinary language"
approach or other alternative approach would be equally clear.

 > (6) Unfortunately, I do not have McLarty's book on topos theory,
 > (and the library copy is not available) but remember vaguely that
 > he discusses forms of analysis in a topos. ...

McLarty's book has chapters introducing the Moerdijk/Reyes synthetic
differential geometry topos, and Hyland's effective topos, but leaves
unanswered almost all questions about real analysis in topos theory.
Moreover, the book contains confusing statements such as the following
(page 7):

  "If [a topos] E has a natural number object we can do all of
  classical mathematics, but not always with classical results, ..."

I find this confusing, because what is "all of classical mathematics",
if it is not simply the corpus of "classical results"?

Butz says:
 > (7) On the categories mailing list some people regretted recently
 > that they were ever taught classical set-theory, in particular the
 > cummulative hierarchy. (Without going into details, they had some
 > good reasons for complaining.) ...

Please do go into details.  I'd like to hear why these category people
think they have corrupted their own minds by studying classical set
theory.  Is classical set theory dangerous to everyone's mental
health?  How about intuitionism?  Topos theory?  Algebra?
Differential equations?  Classical philosophy?  Classical music?  :-)

-- Steve