There are two obvious approaches to constructive set theory: (i) Carefully add some set variables to a simpler theory, cautiously add some axioms about them, and try to explain the constructive meaning of the theory, (ii) Start with classical set theory, throw out the law of the excluded middle and any axioms which imply it, and see what is left over. We shall begin with the second approach; the first approach will be followed in Chap. X.