 In \(\mathbf{HA}\) \(+\) MP \(+\) ECT, which Troelstra considers to be a formalization of Russian recursive mathematics (cf. section 3.2 of the entry on  constructive mathematics),  every formula of the form \((y \realizesrel A)\) has an equivalent “classical” prenex form \(A'(y)\) consisting of a quantifier-free subformula preceded by alternating “classical” quantifiers of the forms \(\neg \neg \exists x \) and \(\forall z \neg \neg ,\) and so \(\exists y A'(y)\) is a kind of prenex form of \(A.\)