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$,


1. $\mathsf{HA} + \mathrm{ECT}\_0 \vdash (\varphi \Leftrightarrow \exists n.(n\mathbin{\mathbf{r}}\varphi))$
2. $\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?
> 
> 
> 



Kleene realizability in Peano arithmetic
$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}$Let me first answer a slightly modified question:



> 
> **Proposition:** For any sentence $\phi$, there exists $n\in\mathbb N$ such that $\T{PA}\vdash\overline n\kr\phi$ if and only if $\T{HA+ECT\_0+MP}\vdash\phi$.
> 
> 
> 


The right-to-left direction follows from $\T{HA+MP}\subseteq\T{PA}$ and the fact that we can find explicit realizers in $\T{HA+MP}$ for each consequence of $\T{HA+ECT\_0+MP}$.


On the other hand, assume that $\T{PA}\vdash\overline n\kr\phi$. The formula $x\kr\phi$ is almost negative, hence it is equivalent to a negative formula $\psi(x)$ in $\T{HA+MP}$. Then $\T{PA}\vdash\psi(\overline n)$, hence $\T{HA}$ proves its double negation translation. However, negative formulas are $\T{HA}$-provably equivalent to their double negation translations. Thus, $\T{HA}\vdash\psi(\overline n)$, $\T{HA+MP}\vdash\overline n\kr\phi$, and (by the result you quote) $\T{HA+ECT\_0+MP}\vdash\phi$.


For the actual question you asked:



> 
> **Proposition:** For any sentence $\phi$, $\T{PA}\vdash\exists x\,(x\kr\phi)$ if and only if $\T{HA+ECT\_0+MP+SLEM}\vdash\phi$, where SLEM denotes the *sentential* law of excluded middle: the schema $\chi\lor\neg\chi$ for sentences $\chi$.
> 
> 
> 


Left-to-right: continuing the argument above, $\T{PA}\vdash\exists x\,(x\kr\phi)$ implies that $\T{HA}$ proves the double negation translation of $\exists x\,\psi(x)$, which is equivalent to $\neg\neg\exists x\,\psi(x)$. Thus,
$$\T{HA+MP}\vdash\neg\neg\exists x\,(x\kr\phi).$$
Since $\exists x\,(x\kr\phi)$ is a sentence, this implies
$$\T{HA+MP+SLEM}\vdash\exists x\,(x\kr\phi).$$
By point 1 of your quoted result, this means
$$\T{HA+MP+SLEM+ECT\_0}\vdash\phi.$$


For the right-to-left direction, it suffices to show
$$\T{PA}\vdash\exists x\,\bigl(x\kr(\chi\lor\neg\chi)\bigr).$$
It follows easily from the definition that
$$\T{HA}\vdash\exists x\,(x\kr\neg\chi)\leftrightarrow\neg\exists x\,(x\kr\chi).$$
Thus, using the law of excluded middle, PA proves that either $\chi$ has a realizer, or it does not, in which case anything is a realizer of $\neg\chi$. In both cases, we obtain a realizer of $\chi\lor\neg\chi$.


