  As a final remark: while the strength of CZF is well below that of  second-order arithmetic, the simple addition of excluded middle to CZF gives us (full) ZF. This should be contrasted with IZF, which already has the strength of ZF (Friedman 1973a). The limited  proof theoretic strength of CZF compared with IZF has often been considered one of  the main advantages of constructive over intuitionistic set theory. In a sense, it would seem that CZF makes the most of  its use of intuitionistic logic, as it characterises a notion of  (generalised) predicative set which is sufficiently strong for  the development of much of constructive mathematics but also  weak enough to avoid impredicativity. Interestingly, when some large set axioms have been added to constructive set theory, a similar pattern has emerged, as the strength of the resulting theory is well below that of the corresponding classical theory.