Set existence property for intuitionistic theories with dependent choice (Q793723)

It is known that many intuitionistic theories have the existence property (EP): if a sentence \(\exists x.A(x)\) is provable, then so is A(t) for some closed term t. In the presence of countable choice (CAC) or relativized dependent choice (RDC), however, only fragment of EP regarding the existence of natural numbers (numerical EP) was established [\textit{J. Myhill}, J. Symb. Logic 40, 347-382 (1975; Zbl 0314.02045)]. The authors first show EP for second order intuitionistic arithmetic with CAC. The proof involves Friedman's extension of the Kleene slash, not in the classical metatheory, but in the 1945-realizability model. Numerical EP is then used. The method readily extends to intuitionistic type theory (resp. intuitionistic Zermelo set theory) with RDC. A modification of the argument establishes the following for intuitionistic ZF set theory formulated with replacement, and with RDC \((ZFI_ R\)+RDC). Let TI be the schema of transfinite induction over all (true) primitive recursive well founded binary relations on natural numbers. Let T\(I^-\) be the fragment of TI referring to such relations provably well founded in intuitionistic ZF with collection and RDC. Let a sentence \(\exists x.A(x)\) be provable in ZF\(I_ R\)+RDC (in ZF\(I_ R\)+RDC+TI, resp.). Then there is a formula \(B(y)\) with exactly y free, such that \(\exists x(A(x)\wedge \forall y(y\in x\leftrightarrow B(y)))\) is provable in ZF\(I_ R\)+RDC+T\(I^-\) (in ZF\(I_ R\)+RDC+TI, resp.).