FOM: comments on Wilson's dual view of foundations.
palmgren at math.uu.se
Sat Mar 18 10:54:03 EST 2000
I have some remarks with relevance to points 2 - 4 of Todd Wilson's
interesting posting on March 15. In fact, Joyal and Moerdijk have
already set up a categorical framework which can interpret
intuitionistic set theory IZF (ZF = IZF+classical logic). Within this
framework one then develops a theory of internal sheaves, following
Johnstone and others, and hence there is in principle no need to refer
to set theory when developing a model-theory of IZF. The main reference
here is A. Joyal and I. Moerdijk: Algebraic Set Theory. Cambridge
University Press 1995. Since ZF can be interpreted into IZF by a
negative interpretation (Friedman 1973), there is thus a categorical
framework of at least the interpretational strength of set theory.
In his development  of constructive set theory (CZF) Peter Aczel
investigated the constructive analogues of regular cardinals
(regular sets) and inaccessibles. For a constructive justification
of these notions Martin-Löf's type-theoretic universes are essential.
More recently constructive analogues of larger cardinals have been
studied by Michael Rathjen [3,4,5] (within CZF) and Anton Setzer 
(within Martin-Löf type theory). CZF is a proof-theoretically much
weaker system than IZF, which belongs to the predicative realm, i.e.
it can be reduced to generalised inductive definitions. Nevertheless
CZF + classical logic = ZF. In a recent paper  with Moerdijk we
develop a categorical structure for interpreting CZF, adapting the
methods from "Algebraic Set Theory". It should be possible to use
the ideas from the extensions of CZF and their type-theoretic
interpretations to find the right categorical notions for the
It seems clear to me that categorical axiom systems, such as toposes,
are not suitable as the ultimate foundation of mathematics. They are
simply algebraic generalisations of mathematical universes which are
closed under certain constructions (products, function spaces, quotients,
etc). As for the motivation of such systems it seems that one should
look to constructive foundations (the logic of toposes is intuitionistic)
rather than classical set-theoretic foundations. Thus, for instance,
one can start out from the notion of "set" in Bishop constructivism,
which is a type (or preset) together with an equivalence relation. It
is possible to formalise this category of sets in various constructive
type theories: intuitionistic versions of Church type theory
(which are impredicative) or Martin-Löf type theory (which is predicative).
The former gives the category of "sets" the properties of a topos,
while the latter yields a weaker categorical structure, which still
admits the construction of internal sheaves (see ).
 P. Aczel. The type-theoretic interpretation of constructive
set theory: inductive definitions. In: R.B. Marcus et al. (eds.)
Logic, Methodology and Philosophy of Science VII. North-Holland 1986.
 I. Moerdijk and E. Palmgren: Type Theories, Toposes and Constructive Set
Theory: Predicative Aspects of AST. U.U.D.M. Report 2000:2, 44 pp.
 M. Rathjen, E.R. Griffor, E. Palmgren.
Inaccessibility in constructive set theory and type theory.
Annals of Pure and Applied Logic, 94(1998), 181-200.
 M. Rathjen. Interpreting Mahlo set theory in Mahlo type theory.
 M. Rathjen. The higher infinite in proof theory.
 A. Setzer: Extending Martin-Löf Type Theory by one Mahlo-Universe.
To appear in Arch. math. log.
Associate Professor of Mathematical Logic
More information about the FOM