 Combining Markov’s Rule with the negative translation gives the result that classical and intuitionistic arithmetic prove the same formulas of the form \(\forall x \exists y A(x, y)\) where \(A(x, y)\) is quantifier-free. In general, if \(A(x, y)\) is provably decidable in \(\mathbf{HA}\) and if \(\forall x \exists y A(x, y)\) is a closed theorem of classical arithmetic \(\mathbf{PA},\) the conclusion of the Church-Kleene Rule holds even in intuitionistic arithmetic. For if \(\mathbf{HA}\) proves \(\forall x \forall y (A(x,y) \vee \neg A(x,y))\) then by the Church-Kleene Rule the characteristic function of \(A(x,y)\) has a Gödel number \(m,\) provably in \(\mathbf{HA};\) so \(\mathbf{HA}\) proves \(\forall x \exists y A(x,y) \leftrightarrow \forall x \exists y \exists z B(\mathbf{m},x,y,z)\) where \(B\) is quantifier-free, and the adjacent existential quantifiers can be contracted in \(\mathbf{HA}.\) It follows that \(\mathbf{HA}\) and \(\mathbf{PA}\) have the same provably recursive functions.