  Constructive and intuitionistic ZF are based on the same first-order language as classical ZF set theory, which has only the binary predicate symbol \(\in\) (membership) as non-logical symbol. That is, they are formulated on the basis of intuitionistic first-order logic with equality, plus the binary predicate symbol \(\in\). We can thus take advantage of the simplicity of the set-theoretic language and of our familiarity with it (Myhill 1975). As with Bishop-style constructive mathematics, Constructive and intuitionistic ZF are compatible with the classical tradition, in the sense that all of their theorems are classically true. In fact, the two formal systems that we shall consider, Constructive Zermelo-Fraenkel (CZF) and Intuitionistic Zermelo-Fraenkel (IZF), give rise to full classical ZF by the simple addition of the principle of the excluded middle.