  Constructive and intuitionistic Zermelo-Fraenkel set theories are  axiomatic theories of sets  in the style of  Zermelo-Fraenkel set theory (ZF)  which are based on  intuitionistic logic.  They were introduced in the 1970’s and they represent a formal context  within which to codify mathematics based on intuitionistic logic (see the entry on  constructive mathematics). They are formulated on the standard first order language of  Zermelo-Fraenkel set theory and make no direct use of inherently  constructive ideas. In working in constructive and intuitionistic  ZF we can thus to some extent rely on our familiarity with ZF and  its heuristics.