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?


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

  • $\begingroup$ 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? $\endgroup$
    – Gro-Tsen
    Feb 24, 2019 at 13:28
  • 2
    $\begingroup$ 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$). $\endgroup$ Feb 24, 2019 at 13:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.