  Although CZF and IZF are the most widely studied systems, numerous other systems for constructive and intuitionistic set theory have been considered in the literature so far. The proof-theoretic strength of a number of constructive and intuitionistic set theories has been established by a variety of tools, like, for example, an extension to set theory of the double negation interpretation (originated in (Friedman 1973a)), and a variety of other proof-theoretic interpretations, often resulting from a careful combination of semantic and proof theoretic techniques. In many cases the proof theoretic strength of a system has been determined by a chain of interpretations between constructive and classical systems, and by using a variety of tools, from relisability to more "traditional" proof theoretic techniques, as ordinal analysis (see, for example, Beeson 1985; Griffor and Rathjen 1994; Rathjen 2012b). In particular, realisability has turned out to be very useful, due to its flexibility. As to the outcomes of these investigations, some of the systems analysed turn out to be as weak as arithmetic, as, for example, Friedman’s system B (Friedman 1977); other systems are as strong as full classical ZF, as IZF (Friedman 1973a). There are also systems of intermediate strength, as CZF. The strength of the latter theory, in fact, equals that of a theory of one inductive definition known as ID\(_1\). The fact that CZF has the same strength as ID\(_1\) is taken to confirm the (generalised) predicativity of the set theory, and to prove that it exceeds the limit of predicativity given  the natural numbers, since ID\(_1\)’s proof theoretic ordinal is well above  \(\Gamma_0\).