Intuitionistic proof of equiconsistency of the Church thesis with set theory (Q1901901)

The present note contains an answer to a question of \textit{H. M. Friedman} and \textit{A. Ščedrov} [Adv. Math. 57, 1-13 (1985; Zbl 0585.03025)] (quotation from p.2: ``... it is not known whether \(\text{ZFI}_R\) is equiconsistent with \(\text{ZFI}_R\) + ``Every \(f \in \omega^\omega\) is recursive'' ''). The answer is positive, and it was for the first time announced by the author in ``Intuitionistic set theory'' (Russian) [Theses of the VIIIth Vsesoyuz. Konf. ``Logika i metodologiya nauki'', Palanga 1982, 91-94 (1982)] and later in ``Set theory with intuitionistic logic and a method of recursive realizability'' [Pap. Sov. Sci. submitted to the Sov. Natl. Org. Com. for the VIIth Int. Congr. Logic, Methodol. Philos. Sci., Salzburg 1983, pp. 71-74]. In the same papers there were given the reasons which cause the answer to be possible if we use models of realizability type, and which do not enable it in pseudo-Boolean models. Here we give the proof for a two-sorted set theory. But it can be further extended to a one-sorted version.