A first answer to Beeson’s question came with (Rathjen 2012), where the author introduced the notion of weak existence property: the focus here is finding a provably definable set of witnesses for every existential theorem. He then introduced a form of realizability based on general set recursive functions, where a realizer for an existential statement provides a set of witnesses for the existential quantifier, rather than a single witness. Rathjen combined this notion of realizability with truth to yield that a number of theories with collection do enjoy the weak existence property (while IZF does not). Among them, in particular, the theory CZF without subset collection plus Myhill’s exponentiation axiom, CZF\(_{Exp}\). In fact, Rathjen claimed that by combining these results with further work he had carried out, he could show that CZF\(_{Exp}\) (and a number of other theories) do have the existence property. A striking observation is that these theories are formulated with collection; consequently the failure of the existence property in the case of IZF can not be attributed only to collection, but to the interplay between this scheme and unrestricted separation.