FOM: some answers to Simpson

[Carsten Butz]

This post tries to answer some questions posted by Stephen Simpson in
connection with real analysis in a topos (Tue, 3 Feb 1998 14:24:10, 
FOM: categorical mis-foundations: real analysis; IHOL; simplicity;
schemes).

Real analysis:
=============
For real analysis the question was:

   > Consider the standard undergraduate calculus theorem saying that
   > every continuous real-valued function on [0,1] has a maximum
   > value. ....  I surmise that it's a difficulty for "categorical
   > foundations", because it's probably not provable in topos plus
   > NNO.

Before I try to answer this question, I should note that I was never
really interested in doing analysis in a topos, and unfortunately I do
not have access to McLarty's book, in particular, I do not remember
what he does. 

The first subtle thing to remember is that there are potentially
different kind of reals, Cauchy reals, Dedekind reals, etc, which in a
classical set-up (for example in a boolean topos) coincide, but not in
general. The reason being, that intuitionistically these different
notions are distinct. So one has to distinguish which reals one means.

I looked up in [vanDalen/Troelstra: Constructivism in Mathematics],
chap 6, where they treat some analysis of Cauchy reals. 
They have
- a counterexample to the intermediate-value theorem in its strong
form (1.2);
- a weaker form of the intermediate-value theorem (1.4);
- and, concretely to your question: for any uniformly continuous function
defined on a closed interval both sup(f) and inf(f) exist (1.8), but
they give a counterexample to the existence of a maximum (1.10).

This was the negative part, the poor positive part is that the result
holds in a boolean topos. I am convinced that the result is true in
many toposes not being boolean, but cannot state any sharper
answer. Sorry.

Another remark: I once spoke to a computer scientist about the
intermediate-value theorem and he said: "Of course, I do not believe in
this theorem, why should I?" As far as I remember, the
person had a good mathematical background, so you cannot just say that
he was too stupid to get the result.
So there could be a debate (that we should not start here) what
real analysis really is, and as well, 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. 

IHOL:
=====
I am happy you understood it, and as well, you rightly mention some of
the short-comes: Starting with a theory T (formulated in some fixed
higher order language) we construct the topos E(T), and then get out
of it its internal theory T(E(T)), which is formulated in a much
larger language (for example, the types are the objects of E(T)).
As you observed correctly, T(E(T)) is something like a maximal
extension by definitions of T.
  Of course, if we want to axiomatize something, we choose an
appropriate language, and we choose the 'right' axioms. No doubt, we
all agree.
  On the other side, we very often study the deductive closure of a
set of axioms (then speaking of a theory, so my use of the word theory
above is a little misleading), and in some sense (very liberal, of
course), T(E(T)) is the deductive closure of T, containing as well
many more definable types, ..., well, as you said, it is the maximal
extension by definitions.
  Of course, things like finite set of axioms, finite signature (basic
sorts, function and relation symbols) are lost. 
  
  I guess, mathematically (logically) we should be happy,
philosophically we should at least be suspicious, I agree.

  I read again through your questions, and I feel, I should say
something more: 
(1) So we might agree on some axioms T (mathematically and
philosophically), but we will agree only mathematically on T(E(T)).
(2) We should remember that T and T(E(T)) have the same models (really
the same): any T(E(T)) model is a T model qua restriction, and any T
model extends canonically to a T(E(T)) model. That's good, at least. 
(Where do these models live? In any intuitionistic universe of
mathematics, for example, they could live in some topos....).

You say that topos-theorists do not appreciate the foundational
importance of intuitionistic logic etc. ..
 Maybe, we didn't express ourselves correctly and clearly: Yes, we are
algebraists and we love being so. Yes, we are categorists and this is
at least the toolbox we use every day.
  And, yes, we are logicians, we appreciate in particular
intuitionistic logic, and not just because it is the logic that holds
in the objects we study (toposes), also because we find the logic and
the ideas of constructive/intuitionistic mathematics appealing.
  If you complain about the fact that we do not analysis: Do so, I
can't give you a satisfying answer for that. As far as I am concerned
the reason is that I am interested in algebra, and not in analysis. I
should say as well that it is slightly easier to do algebra in a topos
than doing analysis in a topos, but may be this is just my very
personal impression, and others might disagree. 

Simplicity:
===========
We had an unfortunate discussion about simplicity. I have my doubts
whether everybody on this list would really sign everything they
wrote. Let me summarize:

(1) There is no doubt that we have some intuition about simplicity,
but this can differ from person to person.
(2) There is as well no doubt, that the basic things we want to
describe (say collections) should be simple, of low complexity, etc.
I guess we all agree that the notion of "set" (capturing collection)
is simple and basic (although we category theorists think there is
something more).
(3) Again, the axioms of Harvey Friedman are nice, well-stated etc,
although we can/could argue a little whether this or that property
does really hold for collections, or whether we can really perform this
or that construction on collections, but this is more about
philosophy, not about simplicity. 
(4) One should at least mention that one of the 'axioms' is an axiom
scheme, with all its pro's and con's. Friedman argued nicely in favour
of it (really well-done), although I still think (as a philosopher,
not as a mathematician) that one should be careful with axiom schemes,
but that's not the point here.

(5) We toposophers claim that the axioms for a topos are simple. We
once tried to convince you that one can axiomatize toposes as models
of an algebraic theory (axiomatized by a language containing only
function symbols, and having as axioms only equations, i.e., axioms of
the form
\forall x ( t(x) = s(x) )
where x is a finite string of variables).

This is certainly true (it was observed by Peter Freyd quite some time
ago), but I personally dislike this statement a little, since this
axiomatization is not the "philosophically correct one", still, it is
a good result in "logic", and algebraic theories are certainly the
simplest we can think of qua logical complexity.
But, what does simple mean then if we need 50 axioms? (I have never
really looked at the proof, I do not know how many axioms one needs.)

(6) Still, I would sign immediately that the axioms of a topos are
simple! Cartesian closed categories are one of the most simplest
structures one can think of, and they are one of the first categories we
teach our students after introducing the concept of a category.
The only additional 'axiom' is that of the subobject
classifier. Difficult? May be yes if you see it for the first time,
but in one form it just says that the functor sending an object to its
subobjects is representable, a perfectly natural condition in category
theory. And, after all, our set-theory students struggle as well when
they see the axioms of set-theory for the first time, isn't this
correct?

(7) 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 am not
convinced that first-order logic is always appropriate to formulate
things, it is well-known to everyone who has used it for some time
that some perfectly natural notions can become clumsy if written up in
first order logic (please, be honest). 
  I personally do find McLarty's axioms clumsy (sorry, Colin), I do
not find the definition of a topos clumsy. 
 
(8) One of the 'advantages' of an axiomatization of toposes is that a
finite set of axioms is enough, no axiom scheme. Again, this means
'some' sort of simplicity, still it is debatable. 

  Regards,

  Carsten Butz

Carsten Butz
Research Associate
Department of Computer Science, University of Aarhus (Denmark)
Research interests: Categorical logic, topos theory, homological algebra
WWW: http://www.brics.dk/~butz/