The lack of definable witnesses and provably recursive functions in intuitionistic set theories (Q1071017)

Let \(ZFI_ R\), \(ZFI_ C\) be intuitionistic Zermelo-Fraenkel set theory formulated with Replacement, resp. Collection. It is known that \(ZFI_ R\) has the existence property. It is shown that \(ZFI_ C\) does not have the existence property. This remains true if one adds Dependent Choice and all true \(\Sigma_ 1\)-sentences of ZF. It is known that ZF and \(ZFI_ C\) have the same provably recursive functions. It is shown that this is not true for \(ZFI_ C\) and \(ZFI_ R\). (From the authors' summary).