 It is not surprising that investigations on the proof-theoretic strength of constructive and intutionistic set theories have been a crucial meta-theoretical tool for understanding these theories and their relations with each other. Investigations on the proof-theoretic strength of a theory are rich and informative. In particular, Feferman (1993) has argued that a proof-theoretic analysis may help us establish whether a certain theory complies with a given philosophical framework: for example, the analysis may reveal that a theory is predicative or finitistic etc. Furthermore, as a by-product of the proof-theoretic analysis we sometimes obtain simple independence proofs. In fact, we can show that a theory cannot prove a specific principle because adding it to the theory would increase the theory’s proof-theoretic strength. For example, CZF does not prove the powerset axiom, as the addition of powerset to CZF gives rise to a much stronger theory. Proof-theoretic interpretations have also been employed to compare constructive and intuitionistic ZF set theories among each others, as well as with their classical counterparts, and also with other foundational systems for constructive mathematics, such as constructive type theory and explicit mathematics (see e.g., Griffor and Rathjen 1994, Tupailo 2003). For a definition of the notion of proof-theoretic strength and for surveys on proof theory see, for example, (Rathjen 1999, 2006b). 