Axiom ``collection'' independence of ``DC'' principle in intuitionistic set theory (Q1902734)

Let \(\text{ZFI}_2\) be the set theory with intuitionistic logic, with two sorts of variables (natural numbers and sets), and including a complete family of set-theoretic axioms (exact formulation is given by the author in Dokl. Akad. Nauk SSSR 252, 1070-1074 (1980; Zbl 0482.03026)). In that paper we obtained a model where ``collection'' and ``DC'' (double complement) are true. Let us cite the precise formulation of ``DC'' in the language of \(\text{ZFI}_2\): \[ \forall a \exists x \bigl[ \forall n (\neg \neg n \in a \leftrightarrow n \in x) \wedge \forall u( \neg \neg u \in a \leftrightarrow u \in x) \bigr] \] (here \(n\) is a variable on the natural numbers, and the other ones on sets). It is clear that \(\text{ZF} \vdash \text{DC}\). Let us make an effort to weaken \(\text{ZFI}_2\) by means of replacement of the axiom ``collection'' by the axiom of substitution. From the intuitionistic standpoint, the deducibility \(\text{ZFI}_2\) -- ``collection'' + substitution \(\vdash\) ``collection'' is no longer valid [see \textit{H. M. Friedman} and \textit{A. Ščedrov}, Adv. Math. 57, 1-13 (1985; Zbl 0585.03025)]. It is also clear that \(\text{ZFI}_2\) -- ``collection'' + substitution + ``DC'' is consistent with respect to ZF. There arises the question: whether the scheme ``collection'' remains not deducible in this theory? Here we give the answer and prove the following result concerning the one-sorted theory: if we add ``DC'' to the theory from \textit{J. Myhill}'s paper in Lect. Notes Math. 337, 206-231 (1973; Zbl 0272.02039), then the obtained theory is completely existential. This fact yields (by virtue of the result of Friedman and Ščedrov [loc. cit.]) a positive answer to the formulated question.