Kleene realizability in Peano arithmetic

Question

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?

Answer 1

$\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$.