# Kleene realizability in Peano arithmetic

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

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?

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

• Wow, I did not expect such a clean characterization! And I also had never realized that SLEM is so different from LEM, and I am amazed that it does not contradict ECT₀. Do you know if HA+SLEM (with or without MP and/or ECT₀) has appeared in the literature before? – Gro-Tsen Feb 24 '19 at 13:28
• Yes, I’m sure these are well known. I’m not sure though what is a standard abbreviation for SLEM. Concerning consistency, note that if $T$ is any consistent theory in predicate intuitionistic logic, then $T+\mathrm{SLEM}$ is consistent by simple propositional reasoning (in fact, $T+\mathrm{SLEM}\vdash\phi$ iff $T\vdash\neg\neg\phi$). – Emil Jeřábek Feb 24 '19 at 13:57