The Existence Property in Constructive Set Theory

Abstract

This chapter is primarily of technical interest, in the sense that nothing in the rest of the book depends upon it, and in the sense that the proofs are rather complicated. Nevertheless, the existence property has attracted considerable attention, since many people feel a constructive theory “ought to” have the existence property. It has turned out to be difficult to establish the existence property for constructive set theories, and new techniques have been developed for the purpose. From this perspective, the methods of this chapter are of more than “mere” technical interest, in that they represent the frontier of knowledge in the subject of constructive set theory.