FOM: no foundations, but real analysis

[Carsten Butz]

Yes, one can do real (intuitionistic) analysis in any topos 
with a natural number object.


Dear all,

this message tries to clarify some aspects of topos theory, related to the
question whether or not one can develop real analysis inside a topos, and
if yes, how far it can be done. In particular, this message does not
discuss foundational aspects of the sort 
"what is more basic, the notion of set or the notion of function".
In my opinion all of the stuff below has been said on this list
already,
both by Colin Mclarty and by Steve Awodey. Unfortunately, this has not
been recognised by some on this list, so that I feel the need to make
the statements as precise as possible, in particular, I give
references to two standard texts in topos theory.

(1) I guess, most of real analysis can be formalised in ZF, some results might 
need the axiom of choice, so that we certainly can agree on the standard
axiomatisation of ZFC. On the basis of ZFC you can open any textbook
on real analysis to see how the theory develops.

(2) In general, a topos is not a categorical model of ZFC (this was never 
claimed on this list). Mainly, this fails for three reasons:
(a) The logic supported by a topos is in general only intuitionistic. 
    It is classical in so-called Boolean toposes.
(b) The topos may fail to have a so-called natural number object (nno). 
    This roughly means that the topos does not support the axiom of infinity. 
    I should mention that some texts include the existence of a natural 
    number object in the definition of a topos.
(c) The topos may fail to support the axiom of choice, either internally (IAC)
    or externally ("any epi has a section").

(3) In general, a topos is a categorical model of an intuitionistic higher
order type theory. A detailed account of this, including a calculus is given
in [Lambek-Scott, II.1]. (Note: they include the natural number object in the
definition of a topos.) The type theory valid in a topos is not as strong as 
the intuitionistic version of ZF ([MacLane-Moerdijk] discuss the situation for
well-pointed toposes in VI.10).

(4) The topos is boolean iff the supported type theory is classical. 

(5) Anyway, if the topos has enough structure (nno + boolean + IAC), then its
internal logic is a classical higher order type-theory with choice.
Within this type-theory you can do all real analysis you want. There will 
be no difference between the statements that you can prove in such a topos,
and those statements you find in a textbook about analysis you give to your
students. Even the proofs are exactly the same. There is nothing more
to say about this point. 
  Well, maybe, there is something more to say: What if in particular 
booleanness is missing? Then your analysis is intuitionistic. Of
course, you cannot prove such statements as the mean-value theorem or
results using step functions. But this is just natural:
Intuitionistically you even cannot define step functions (just to give
an example), at least not in the straightforward way you do in
classical analysis. 
  There was as well the question whether this kind of real analysis
has been developed in print: For the classical case, there are
literally hundreds of references, for the intuitionistic variants I am
not so sure: There is may be just not too much interest in developing
intuitionistic analysis for its own sake. The only source I know
where this topic is touched is [Troelstra-VanDalen], Section I.5 and I.6.
However, particular results appear throughout the topos-theory 
literature, although they are not always (immediately) recognisable as such. 
  It is however true that analysis in some specific toposes has been
developed to some extend: Some toposes model very closely the
philosophical ideas of some intuitionistic philosophers like Brouwer or
Bishop. And these people developed their ideas up to quite some 
sophisticated level. As an example one might quote
Bishop's Constructive Analysis. (Although I have to admit that I do
not have a topos model right here to present you.)

(6) Related to (5) the question was raised how artificial these extra 
assumptions are: Let me give two answers to that question.
  First of all, writing down what it means to have a nno or to be boolean
is a very simple statement qua structure. You would never say that these
definitions are complicated to state. The same applies to IAC.
References: nno [Lambek-Scott], p. 140.
            boolean [Lambek-Scott], p. 131.
            IAC [Lambek-Scott], p. 161
                [MacLane-Moerdijk], p. 344 (exercises 5-16).
  The second answer is the following: Adding these assumptions to the axioms
of a topos is as artificial as it is to require for your base for doing 
mathematics the following principles:
  the axiom of infinity
  the underlying logic is classical
  the axiom of choice
I mean this statement as it stands: In the *categorical* set-up,
adding nno, boolean or IAC are natural assumptions you may consider to
add. For most on this list there is certainly no doubt that these
assumptions are natural in the classical set-theory set-up.
(I leave aside the questions about choice, and may be the question of
intuitionistic logic, which are not too much our purpose here.)

(7) I would like to emphasise the historical development of topos theory: 
First, there were the categories of sheaves on some (small) site
(nowadays called Grothendieck toposes) . They were invented by
Grothendieck and his school to have the right set-up to do cohomology 
theory (the category of sheaves of abelian groups of a Grothendieck
topos is an abelian category satisfying AB5*). Grothendieck et al. were
in particular interested in etale cohomology. This started in the early 60th
I guess, and culminated in the seminar notes SGA4 (LNM 269, 270 etc). 
Lawvere and Tierney tried to give an axiomatic treatment of Grothendieck 
toposes, i.e., tried to prove a statement like "a category is a Grothendieck
topos iff ....". It might have been quite a surprise to them that the
axiomatisation is closely related the earlier attempts to write down all the
properties of SETS, our base-category of sets. They coined the notion of
an elementary topos, which was simplified during the years. 
The definition you find nowadays is that an elementary topos is a 
cartesian closed category with a subobject classifier. (Above, topos referred
to elementary topos.) Any Grothendieck topos is an elementary topos.
Giraud's theorem may be seen as a way to distinguish elementary toposes from
Grothendieck toposes.

(8) The statements made in this mail should clarify and give evidence to 
the following precise mathematical statements:

 Any topos supports an internal higher order intuitionistic type theory.

 In a topos with natural number object, you can develop intuitionistic
 analysis, with all its pro's and con's, for example, Dedekind reals and
 Cauchy reals may differ in such a set-up.

 Requiring that your topos is boolean puts you pretty close to ZF.
 (If I remember correctly, Mathias has a paper related to it? "On Mac Lane
  set theory" or something like this. This should contain a detailed account
 of how close to ZF you get.) 

(9) In my opinion, the statements made in (8) do not at all touch the
foundational question, whether or whether not functions may serve as a 
(better) foundation of mathematics or not. I will come back to this in a 
second posting. 

  Regards,

  Carsten Butz

References: 
[Lambek-Scott] Introduction to higher order categorical logic. CUP.
[MacLane-Moerdijk] Sheaves in geometry and logic. Springer.
[Troelstra-VanDalen] Constructivism in Mathematics. North-Holland.

PS I am a Research Associate at the Department of Computer Science in Aarhus,
Denmark. I studied Mathematics and Computer Science (but realized recently 
that I did quite some Philosophy as well) in Germany, and got
my Ph.D. from the Mathematics Department of Utrecht University 
(The Netherlands) in 1996. 

Research Interests: Categorical logic, topos theory, homological algebra.
Other interests certainly include analytical philosophy and foundations in the
broadest sense. 
-------------------------------------------------
Carsten Butz (Ph.D.)
BRICS
Basic Research in Computer Science
Centre of the Danish National Research Foundation
Department of Computer Science
University of Aarhus
Ny Munkegade, Building 540
8000 Århus C
Denmark

butz at brics.dk
http://www.brics.dk/~butz
-------------------------------------------------