  Although there are many systems of sets based on intuitionistic logic, we can distinguish two main trends within the literature. According to the first one, we take all of what is available in classical ZF set theory and only modify those principles, such as foundation, which have a clear incompatibility with intuitionistic logic. This gives rise to set theories such as Intuitionistic Zermelo-Fraenkel,  IZF, a variant of which was introduced as early as in (Friedman 1973a). (See Beeson 1985, Chapters 8 and 9 and Scedrov 1985 for two surveys on IZF.) The rationale behind these theories appears to be that of granting the mathematician the most powerful tools possible, as long as compatibility with intuitionistic logic is preserved. According to the second approach, in addition to the adherence to intuitionistic logic we also introduce restrictions on the set-theoretic principles admitted, as far as the resulting system complies with the constructive mathematical practice. Theories of this second kind can thus be seen as the outcome of a double process of restriction with respect to classical ZF. First there is a restriction to intuitionistic logic, then a restriction is imposed on the set-theoretic constructions allowed. The latter is motivated by (1) the observation that weaker principles appear to suffice for the constructive mathematical practice and (2) the desire to adhere to a form of predicativity (see the next section for a clarification of this notion of predicativity). Paradigmatic examples of the latter kind of systems are Myhill’s Constructive Set Theory (Myhill 1975), Friedman’s system B (Friedman 1977) and Aczel’s Constructive Zermelo-Fraenkel set theory  CZF  (Aczel 1978; 1982; 1986, Aczel &amp; Rathjen 2001; Aczel &amp; Rathjen 2010, Other Internet Resources). We can also say that in this second approach the foundational motivation influences the practice to a higher degree.