  Kripke models for intuitionistic set theories have been used  in (Friedman and Scedrov 1985) to show that IZF does not have the EP (and combining this with the results in (Myhill 1973) we have that IZF\(_{Rep}\) does not prove IZF). Kripke models have more recently been applied to clarify the relation between the constructive substitutes of the power set axiom: Myhill’s exponentiation axiom and Aczel’s subset collection schema. It is clear that the power set axiom implies both of these principles, and that subset collection implies exponentiation. On the other hand, each of the latter two principles  does not imply power set, as the theory CZF with power set in place of subset  collection is much stronger  than CZF and CZF\(_{Exp}\) (Rathjen 2012b). In fact, CZF and CZF\(_{Exp}\) have the same proof theoretic strength (Griffor and Rathjen 1994); therefore to investigate the relation between  subset collection and exponentiation in constructive set theory  one needed to develop tools other then proof theoretic methods.  Lubarsky (2005) used Kripke models to show that Myhill’s exponentiation axiom does not imply Aczel’s subset collection (on the basis of CZF minus subset collection plus full separtion). In (Lubarsky and Rathjen 2007) the authors applied the technique of Kripke models to show that also the consequences of the theories CZF and CZF\(_{Exp}\) are different. Aczel and Rathjen (2001) had shown that the class of Dedekind real numbers forms a set in CZF,  by using subset collection. Lubarsky and Rathjen (2007) showed that CZF\(_{Exp}\) does not suffice to prove the same statement. For further applications of Kripke models to separating crucial constructive  notions, see e.g. (Diener and Lubarsky 2013).