For completeness of MathOverflow and for clarity of the question, I will first recall a few things, including the the definition of Kleene realizability: experts can jump directly to the question below.
For natural numbers $n$ and first-order formulae $\varphi$ of Heyting arithmetic, the formula “$n$ realizes $\varphi$” is defined by induction on the complexity of $\varphi$ by:
for atomic $\varphi$, “$n$ realizes $\varphi$” simply means $\varphi$ [is true],
$n$ realizes $\varphi\land\psi$ iff $n=\langle p,q\rangle$ (some fixed primitive recursive bijective pairing function $\mathbb{N}^2\to\mathbb{N}$) where $p$ realizes $\varphi$ and $q$ realizes $\psi$,
$n$ realizes $\varphi\lor\psi$ iff $n=\langle 0,p\rangle$ where $p$ realizes $\varphi$ or $n=\langle 1,q\rangle$ where $q$ realizes $\psi$,
$n$ realizes $\varphi\Rightarrow\psi$ iff for each $p$ which realizes $\varphi$, the value $\{n\}(p)$ (of the $n$-th partial recursive function applied to $p$) is defined and realizes $\psi$,
$n$ realizes $\exists x.\psi(x)$ iff $n=\langle k,q\rangle$ where $q$ realizes $\psi(k)$ (meaning the substitution for $x$ in $\psi$ of the explicit term representing the integer $k$),
$n$ realizes $\forall x.\psi(x)$ iff for each $k$, the value $\{n\}(k)$ is defined and realizes $\psi(k)$.
This in turn defines a new first-order formula of Heyting arithmetic which we can denote, say, $n\mathbin{\mathbf{r}}\varphi$.
Now I understand that (Dragalin and Troelstra independently proved that) for all $\varphi$,
$\mathsf{HA} + \mathrm{ECT}_0 \vdash (\varphi \Leftrightarrow \exists n.(n\mathbin{\mathbf{r}}\varphi))$
$\mathsf{HA} + \mathrm{ECT}_0 \vdash \varphi$ if and only if $\mathsf{HA} \vdash \exists n.(n\mathbin{\mathbf{r}}\varphi)$
where $\mathsf{HA}$ denotes Heyting arithmetic and $\mathrm{ECT}_0$ some statement (the “extended Church thesis”) which I won't copy because it's not really germane to my question but which says informally that every relation on an almost negatively defined domain contains a partial recursive function defined on that domain; note that $\mathrm{ECT}_0$ is classically refutable.
Furthermore, in (2) (well, trivially in (1) also), $\mathsf{HA}$ can be replaced by $\mathsf{HA} + \mathrm{MP}$, where $\mathrm{MP}$ (“Markov's principle”) is the (classically tautological) $(\forall x.(\psi(x)\lor\neg\psi(x))) \Rightarrow ((\neg\neg\exists x.\psi(x))\Rightarrow \exists x.\psi(x))$.
To paraphrase, $\mathsf{HA} + \mathrm{ECT}_0$ axiomatizes the set of formulae provably realizable in $\mathsf{HA}$, and $\mathsf{HA} + \mathrm{MP} + \mathrm{ECT}_0$ axiomatizes the set of formulae provably realizable in $\mathsf{HA} + \mathrm{MP}$.
This leads me to ask:
Question: what can be said about the set of formulae $\varphi$ such that $\mathsf{PA} \vdash \exists n.(n\mathbin{\mathbf{r}}\varphi)$, where $\mathsf{PA}$ denotes Peano arithmetic (i.e., Heyting arithmetic plus the excluded middle)? In other words, what are the set of formulae provably realizable in Peano arithmetic? Can they be axiomatized?
