No Subject

However, if one wants to arrive at a formal system which allows one to derive 
(in principle) "all current mathematics" then I think one has to accept that
HAH is not satisfactory simply because it is too weak. On the other hand it
still is the case that traditional syntax of ZF is not very convenient as a 
formalisation of mathematical practice. Therefore, it might be worthwhile to
look for formal systems of a type-theoretic character equiconsistent to ZF(C)
and including ZF(C) via translation. Well, such a language is available, namely
the so-called "Calculus of Inductive Constructions" an impredicative type
theory with an infinite hierarchy of universes. This is described in

   Werner, Benjamin
   Sets in types, types in sets. 
   Theoretical aspects of computer software (Sendai, 1997), 530--546, 
   Lecture Notes in Comput. Sci., 1281, 
   Springer, Berlin, 1997.  
   ftp://ftp.inria.fr/INRIA/Projects/coq/Benjamin.Werner/zfc.ps.gz

where one also can find (sketches of) proofs of the meta-theoretic properties 
mentioned above.
The reason why systems like the "Calculus of Inductive Constructions" are as
strong as ZF(C) is that they allow one to 

     define FAMILIES of TYPES by structural recursion.

which is precisely what the set theoretic axiom of replacement is good for.
However, type theoretic language does bring this to the point more clearly
than the set-theoretic axiom of replacement which is often used in mathematical
practice to formulate the image of a function  f : A -> B namely as 
{ f(a) | a \in A} which certainly has to be considered as sort of an overkill
because this can be formulated in HAH as well. The real strength of the axiom
of replacement is used when defining `images of functions without a codomain'
as e.g. families of sets indexed by some inductive type (e.g. an ordinal).
The very purpose of type-theoretic universes is to provide a codomain for
such `functions without codomain'.
According to these observations I get the impression that what topos logic
is missing is a concept of universe which allows one to define by recursion
not only families of objects but also families of types.

I want to conclude my remarks with a pointer to a recent paper by Alex Simpson
on 

    Solving Domain Equations in Models of Intuitionistic Set Theory

(to be found at http://www.dcs.ed.ac.uk/home/als/Research/rde.ps.gz) where in
the last paragraph of section 5 (p.12) he gives a counterexample to the claim 
that 

     in a topos satisfying the usual axioms of SDT (Synthetic Domain Theory) 
     one always can solve domain equations.

The reason is that the topos considered there doesn't allow one to construct
certain N-indexed families. (This is a style of argument well-known from the
usual proofs in set theory showing that Z(C) is weaker than ZF(C)!)


I hope that it has got clear from my formulations that I am not at all 
``anti-category''. However, I always found it most confusing when in some
texts on toposes I read the statement that the logic of toposes coincides
with intuitionistic set theory. I think that most classically trained 
logicians get immediately puzzled by such statements because they know very
well that set theory is stronger than type theory and, therefore, feel sort
of repelled by such oversimplifying statements.
Moreover, during the 90ies there have been developed fascinating categorical
accounts of constructive set theory by Joyal, Moerdijk, Simpson, Butz and 
Palmgren. I think it would be an interesting question to clarify the relation
between this account and the one by universes.

Thomas Streicher