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?

notsome standard primitive-recursive bijection. Instead, we should pair two numbers $x_1,x_2$ by the index of some canonical Turing machine which on input $i$ terminates with $x_i$. Else the soundness theorem "if HA proves a formula $\varphi$, there is a number $n \in \mathbb{N}$ such that HA proves $n \mathop{\mathbf{r}}\varphi$" is not provable in PRA (nor in HA or PA), such that we need to resort to the weaker statement (2) with the internal $\exists$. $\endgroup$notbe able to extract a witnessing number, just analgorithmfor computing a witnessing number. $\endgroup$Metamathematical Investigations of Intuitionistic Arithmetic and Analysis(1973) ¶3.2.2 (p. 189) seems to use the same definition as I give (pairing is defined at ¶1.3.9(B) (p. 23)), and soundness is stated for it at ¶3.2.4. Similar definition in van Oosten'sRealizability: a historical essay, ¶2.2–2.3. Where is there a substantially different definition? $\endgroup$6more comments