FOM: Foundational motivation for topos theory

[Till Mossakowski]

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
classical logic.

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

         \Pi t.t

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 
standard semantics.

Till Mossakowski


* Lecture Notes in Computer Science 173, 145-156
** Lecture Notes in Computer Science 283, 12-39