FOM: Foundational motivation for topos theory
till at Informatik.Uni-Bremen.DE
Fri Feb 13 06:30:35 EST 1998
Steve Simpson has repeatedly asked for a foundational motivation of
topos theory. One motivation of topos theory which in my eyes is
highly relevant for foundations is the following:
With his "Begriffsschrift", Frege created a paradise of classical logic
with unlimited comprehension. Russell destroyed this (illusion of a)
paradise by showing it to be inconsistent.
Zermelo-Fraenkel set theory is one answer to Russell's paradox: it
carefully limits comprehension, while keeping classical logic.
But there also is another answer: keep unlimited comprehension, but not
Now ZFC is a very successful commitment to the first answer, while topos
theory is a more general theory of sets allowing both answers. In fact,
there are not only ZFC-like topoi, but also topoi where you have
(something like) unlimited comprehension, but of course then you don't
have the law of the excluded middle.
The latter topoi are important at all those areas where some form of
unlimited comprehension is more important than the law of excluded middle.
The most prominent such area I know is semantics of polymorphism (i.e.
possibly quantified type variables). Some form of unlimited comprehension
comes in here because
means the product of all types t, and this again has to be a type.
There are two famous papers explaining the situation:
"Polymorphsim is not set-theoretic" by Reynolds* shows that the sets of
ZFC are not suitable as a standard semantics of second-order polymorphic
lambda calculus (where standard semantics means that type forming
operations like product and function types are interpreted in the standard way).
"Polymorphism is set-theoretic, constructively" by Pitts** shows that
using the sets of a suitable topos, there indeed is such a
* Lecture Notes in Computer Science 173, 145-156
** Lecture Notes in Computer Science 283, 12-39
More information about the FOM