Let $\mathsf{HA}$ denote first-order Heyting arithmetic (viꝫ., Peano axioms with unrestricted recursion scheme, in first-order intuitionistic logic). It is known (e.g., Troelstra & van Dalen, *Constructivism in Mathematics* (1988), 3.5.6; Beeson, *Foundations of Constructive Mathematics* (1985), VII.5.3 but concerning a different system; or Troelstra (ed), *Metamathematical Investigations of Intuitionistic Arithmetic and Analysis* (1973), 3.1.5) that $\mathsf{HA}$ has the *number existence property*:

(NEP) If $\mathsf{HA} \vdash \exists n. P(n)$ for some closed formula $\exists n. P(n)$, then in fact there is a natural number $n$ such that $\mathsf{HA} \vdash P(\overline{n})$ (with $\overline{n}$ the obvious term that denotes $n$).

Now this number existence property be formalized as a statement of arithmetic $\forall “P”.((\mathsf{HA} \vdash \exists n. P(n)) \Rightarrow \exists n. (\mathsf{HA} \vdash P(\overline{n})))$, beginning with a universal quantifier ranging over Gödel codes for formulas $P$. So we can ask whether $\mathsf{HA}$ proves this formalized number existence property.

The techniques used to prove NEP in the references above all seem impossible to formalize in $\mathsf{HA}$, because they depend on something (like cut-elimination or formalization of arithmetical truth) that is beyond its power. Yet I also don't see how NEP would imply the consistency of $\mathsf{HA}$. So here are my questions:

**Questions:**

Does $\mathsf{HA}$ prove the (formalized) number existence property, $\forall “P”.((\mathsf{HA} \vdash \exists n. P(n)) \Rightarrow \exists n. (\mathsf{HA} \vdash P(\overline{n})))$, for $\mathsf{HA}$?

If not, does it at least prove $((\mathsf{HA} \vdash \exists n. P(n)) \Rightarrow \exists n. (\mathsf{HA} \vdash P(\overline{n})))$ for each $P$?

If a negative answer to (1), does $\forall “P”.((\mathsf{HA} \vdash \exists n. P(n)) \Rightarrow \exists n. (\mathsf{HA} \vdash P(\overline{n})))$ imply the consistency of $\mathsf{HA}$?

If a negative answer to (2), does $((\mathsf{HA} \vdash \exists n. P(n)) \Rightarrow \exists n. (\mathsf{HA} \vdash P(\overline{n})))$ imply the consistency of $\mathsf{HA}$ for some judiciously chosen $P$?