categories: toposes vs. sets - another aspect

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

I want to take up the discussion on ``toposes vs. sets'' from another point
of view. Over the years a few questions have accumulated and I'd be interested 
in the opinion of the experts.

As Bill Lawvere has pointed out in his reply to the original question there 
are several meanings in which one can understand the relation  

               ``toposes vs. set theory''.

One such distinction is static sets vs. variable sets and one can hardly deny
that the latter are of enormous importance for understanding modern mathematics
from a conceptual point of view. That's probably what most categorists have in
mind when they defend categories as superior to traditional set theory. 
Another argument probably is that the official language of axiomatic set 
theory is most inconvenient for actual formalisation of mathematics. One
knows that in principle one always can eliminate function symbols in favour
of relation symbols but that leads to an explosion of length of formulas and
ends in something fairly uncomprehensible.Thus, categorists and also quite a
few logicians are in favour of formal systems based function application and 
predication instead of using just one single relation  \epsilon  besides 
equality because function application and predication are the basic 
constitutents of actual mathematical statements and, moreover, appear most 
naturally from the categorical notion of topos. In the end this amounts to 
the point of view that HAH (Higher Order Arithmetic), the internal language 
of the free topos with NNO, is the formal system which is most suitable for 
formalizing mathematics (if one wants to embark on such an endeavour at all).

Well, but there are some reasons why HAH may be considered as non-sufficient 
at least from a logical point of view. As Zermelo-Fraenkel set theory ZF(C) 
and, actually, already Zermelo's Set Theory Z(C) prove the consistency of HAH 
and accordingly they are non-conservative extensions of HAH. Well, one might 
argue that this lack of conservativity only affects "meta-statements" and not 
``real mathematical statements''. Even hard boiled set theorists would admit 
that "99% of modern mathematics can be formalised in HAH" (such a statement 
for Zermelo's Z(C) instead of HAH can be found e.g. in Kunen's monograph on 
set theory). However, there  do exists natural mathematical statements which 
can be formulated in the language of HAH but proved only in ZF though they are
fairly different in character from ``meta-statements''. 
A typical such example is Borel Determinacy (BD) saying that for every Borel
set X in Baire space either player or opponent has a winning strategy for the 
game G_X where in each step each player plays a natural number and in the end 
(after \omega steps) player has won if and only if the resulting sequence of 
numbers lies in X.