FOM: comments on Wilson's dual view of foundations.

[Erik Palmgren]

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 [1] 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 [6] 
(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 [2] 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 
corresponding cardinals. 

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 [2]).


References

[1] 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.

[2] 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. 
(see http://www.math.uu.se/~palmgren/publicat.html)

[3] 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. 
[4] M. Rathjen. Interpreting Mahlo set theory in Mahlo type theory.
[5] M. Rathjen. The higher infinite in proof theory.
(see http://www.amsta.leeds.ac.uk/Pure/staff/rathjen/preprints.html)

[6] A. Setzer: Extending Martin-Löf Type Theory by one Mahlo-Universe. 
To appear in Arch. math. log. 
(see http://www.math.uu.se/~setzer/articles/index.html)


Erik Palmgren
Associate Professor of Mathematical Logic
Uppsala University
Homepage: http://www.math.uu.se/~palmgren