Suppose $A(x)$ is a $\Delta_0$ formula defining a non-empty set of natural numbers. It's an easy theorem that there is a primitive recursive function $f:\mathbb{N} \rightarrow \mathbb{N}$ such that $Range(f) = \{n \in \mathbb{N} \mid A(n)\}$. I'm wondering if it's known whether either of the following strengthenings of this theorem are true:

Strengthening 1: Suppose $A(x)$ is a $\Delta_0$ formula defining a non-empty set of natural numbers. Can we find a $c \in \mathbb{N}$ such that $\varphi_c$ is primitive recursive, $\mathbb{N} \models \forall x (A(x) \rightarrow \exists y \varphi_c(y) {\downarrow} = x)$, and $PA \vdash \forall y \exists x (\varphi_c(y) {\downarrow} = x \wedge A(x))$?

Strengthening 2: Suppose $A(x)$ is a $\Delta_0$ formula defining a non-empty set of natural numbers. Can we find a $c \in \mathbb{N}$ such that $\varphi_c$ is primitive recursive, $PA \vdash \forall x (A(x) \rightarrow \exists y \varphi_c(y) {\downarrow} = x)$, and $PA \vdash \forall y \exists x (\varphi_c(y) {\downarrow} = x \wedge A(x))$?

(In the above, "$\varphi_c$" refers to the (partial) recursive function defined by the Turing machine whose Gödel code is c. "$\varphi_c(y) {\downarrow} = x$" is shorthand for a $\Sigma_1$ formula which says that with input y, the Turing machine with Gödel code c eventually halts and outputs x.)

Pedantic Clarification: Typically "$\phi_c(x){\downarrow} = y$" is an abbreviation for "$\exists t M(c,x,y,t)$", where (i) $M(c,x,y,t)$ is a $\Delta_0$ formula and (ii) $\mathbb{N} \models M(c,x,y,t)$ if and only if the Turing machine with Gödel code c halts after t steps on input x and produces output y. Let's call any formula $M$ satisying (i) and (ii) a "computation predicate". By this paper by H.B. Enderton, Strengthening 2 is false for certain choices of computation predicate.

It follows that any argument for Strengthening 2 which assumes that our choice of $\Delta_0$ computation predicate is arbitrary cannot suffice. We also need that PA proves certain facts about our chosen computation predicate. I suspect that any reasonable construction of a computation predicate will work (e.g., whatever construction is used in your favorite recursion theory book), so my question should be phrased more precisely as: is there a computation predicate such that Strengthenings 1 and 2 hold?


I think both strengthening 1 and 2 are true and it is a sketch for proof:

You can construct an effective procedure to find an index $c$ (of a primitive recursive function) for any $\Delta_0$ formula $A(x)$ such that $\mathbb{N}\models \forall x (A(x)\leftrightarrow \exists y \varphi_c(y)\downarrow =x)$ (because for writing a computer program to simulate $A(x)$ we do not need an unrestricted search loop, and all programs in which all search loops are restricted by a primitive recursive bound, computes a primitive recursive function). If we drop the part $\wedge A(x)$ from the condition $PA\vdash \forall y \exists x (\varphi_c(y)\downarrow =x \wedge A(x))$, it becomes the assertion that $\varphi_c$ is a total function and we know that all primitive recursive functions are provably total in $PA$ (in fact $I\Sigma_1$). I think that with a suitable choose of $c$ it would be provable in $PA$ that $\forall x (A(x)\leftrightarrow \exists y \varphi_c(y)\downarrow =x)$ (of course it need an exact proof by induction on complexity of $A(x)$) and if it can be proved, srengthening1 and 2 both hold.


I believe even strengthening 2 is a true statement, that can be proven by "simply" internalizing the proof of the original statement into $PA$.

Proof: Suppose $A(n_0)$ holds for some number $n_0\in\mathbb{N}$. In particular this is provable in $PA$: $$ PA\vdash A(\overline{n_0})$$ where $\overline{n}$ is the numeral representing $n$. This is a simple consequence of completeness of $PA$ (and indeed, much much weaker systems) for $\Delta_0$ sentences.

One can then build the following recursive function $f$:

  • $f(0)=n_0$

  • $f(n+1)= \begin{cases} n \mbox{ if $A(n)$ holds}\\ n_0 \mbox{ otherwise}\end{cases}$

The first case in the definition of $f(n+1)$ is easily decidable even for a p.r. function. This function is easy to define in $PA$, and it is easy to prove, again in $PA$, that $A(m)$ holds for every $f(n)=m$, and conversely that for every $m$ such that $A(m)$ hold, there is a corresponding $n$ with $f(n)=m$ (take $n=0$ if $m=n_0$ and $m+1$ otherwise).

The rule of thumb is:

$PA$ can prove everything you can prove in an informal argument that doesn't specifically involve consistency of $PA$ (or something stronger).

This has a few exceptions (e.g. the Paris-Harrington argument).

  • $\begingroup$ Is there a more precise way of stating this rule of thumb (or a good reference for such theorems)? Your argument is exactly the argument I had in mind, but I'd like to be certain it actually can be carried out in PA. To give you an example of the kind of thing I am worried about, consider part (a) of the sole theorem of this paper: "On Provable Recursive Functions" - H.B. Enderton $\endgroup$ – James Aug 19 '15 at 20:26
  • 1
    $\begingroup$ The first remark is that there is nothing special about $PA$ here: in general you can assume ZFC or whatever you need to carry out your argument. The second remark is that I'm somewhat mistaken: the argument crucially relies on 1. That $PA$ is complete on $\Delta_0$ sentences, and 2. $A(x)$ is provably decidable by a recursive function. This is because we are working from a restricted language, namely $\Delta_0$. Enderton's theorem crucially uses some total function of unknown complexity, i.e. a total function in the abstract. $\endgroup$ – cody Aug 19 '15 at 22:26
  • $\begingroup$ Regarding PA being complete on $\Delta_0$ sentences, this FOM message seems to suggest that this is indeed PA-provable: cs.nyu.edu/pipermail/fom/2007-August/011793.html In Enderton's paper, if $M_0(x,y,z,w)$ is $\Delta_0$, then the $M(x,y,z,w)$ in part (a) of his theorem may be chosen to be $\Delta_0$ as well. This is because it's possible to find a $\Delta_0$ formula A(x) such that $\mathbb{N} \models \forall n PA \vdash A(n)$ but $\mathbb{N} \not\models PA \vdash A(n)$ (specifically, take A(x) to say that x does not code a proof of ``0=1"). The reason for bringing up Enderton's $\endgroup$ – James Aug 19 '15 at 22:55
  • $\begingroup$ ...paper is that it suggests that the strenthening 2 cannot be proven by general considerations about recursive functions and Turing machines. It depends on the way computation is encoded. $M(x,y,z,w)$ being $\Delta_0$ is not enough. $\endgroup$ – James Aug 19 '15 at 23:00
  • 1
    $\begingroup$ Your comment is correct, some pathological choices of $\varphi$ won't work. Any reasonable choice allows proving points 1. and 2. of my comments though, which I believe are indeed the crucial steps. For pathological $\varphi$ it is unprovable that $\varphi_c$ indeed behaves as the described $f$. But a broad statement to that effect can be made: no "interesting" property of $\varphi_c$ can be proven (in $PA$) for a sufficiently pathological $\varphi$. $\endgroup$ – cody Aug 20 '15 at 2:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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