  When introducing versions of ZF based on intuitionistic logic, the first step is to eliminate from the logic the principle of the excluded middle (EM). The next step is to choose a good stock of set-theoretic principles which faithfully represent the desired notion of constructive set. These tasks turn out to be more challenging than one at first might have expected. In fact, as is well known, systems based on a “weaker” logic have the ability to distinguish between statements which are equivalent from the point of view of a “stronger” logic. In the case of set theory, some of the ZF axioms or schemata are often presented by one of many classically equivalent formulations. Classically it is only a matter of convenience which one to use at a specific time. When working on the basis of intuitionistic logic, however, various formulations of a classical axiom may turn out to be distinct (non-equivalent). In fact, one can envisage new statements which are classically equivalent to a ZF axiom but intuitionistically separate from it (for example CZF’s subset collection axiom (Aczel 1978)). 