Toposes as constructive set theories

Here’s something that I just learned: a topos, despite the fact it can model intuitionistic logic is not quite the right setting for a constructive set theory. The reason is that in a topos every function has an image. In a constructive set theory, the only sets whose existence you want to assert is those whose membership functions are explicitly computable. The image of a function between two infinite sets may not be explicitly computable.

(I think the correct analogue for constructive set theory is something called a quasitopos, but I don’t know much about them.)

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>