Work in the first order language of number theory, consisting of the symbols $\mathbf{0}$, $\mathbf{S}$, $\boldsymbol{+}$, and $\boldsymbol{\cdot}$, and let $Q$ denote Robinson's arithmetic.


By a *diophantine formula* we mean a formula in this language having the form $\exists y\_1 \dots \exists y\_m(f(x\_1, \dots, x\_n, y\_1,\dots, y\_m) = g(x\_1, \dots, x\_n, y\_1,\dots, y\_m))$, where each of $f(x\_1, \dots, x\_n, y\_1,\dots, y\_m)$ and $g(x\_1, \dots, x\_n, y\_1,\dots, y\_m)$ is a term in this language having the form of a polynomial whose variables are among $x\_1, \dots, x\_n, y\_1, \dots, y\_m$, and whose coefficients are terms of the form $\mathbf{S}\mathbf{S} \dots \mathbf{S}\mathbf{0}$.


We of course know (Rosser-Kleene-Mostowski) that there is a $\Sigma\_1$-formula $\phi(x)$ with one free variable $x$ such that for every consistent recursively axiomatizable theory $T$ extending $Q$, there is some $n$ such that the sentence $\phi(\mathbf{S}^n\mathbf{0})$ is undecidable in $T$.


Question: Is there a diophantine formula $\phi(x)$ for which the above will be true (i.e. for every consistent recursively axiomatizable theory $T$ extending $Q$, there is some $n$ such that the sentence $\phi(\mathbf{S}^n\mathbf{0})$ is undecidable in $T$)?


Note that we are only requiring that $T$ be a consistent recursively axiomatizable theory extending $Q$, and so are allowing $T$ to be $\omega$-inconsistent.


An alternative way of asking the same question: Can some recursively inseparable pair of r.e. sets $A$ and $B$ be "represented" in $Q$ by some diophantine formula $\phi(x)$ (so that if $n \in A$ then $Q \vdash \phi(\mathbf{S}^n\mathbf{0})$ and if $n \in B$ then $Q \vdash \neg\phi(\mathbf{S}^n\mathbf{0})$)?



Essential incompleteness via diophantine formulas?
The answer is negative.


Consider the model $M=\langle\mathbb N\cup\{\infty\},0,S,+,\cdot\rangle$, where we put $S(\infty)=\infty$, $\infty+x=x+\infty=\infty$ for all $x\in M$, $\infty\cdot0=0\cdot\infty=0$, and $\infty\cdot x=x\cdot\infty=\infty$ for $x\ne0$. It is easy to check that $M\models Q$. In fact, $M$ satisfies the axioms of commutative semirings, hence any term is in $M$ equal to a polynomial with nonnegative integer coefficients, and these polynomials can be manipulated in the expected way.



> 
> **Lemma:** The set of sentences $\phi$ of the form $\exists y\_1,\dots,y\_m\,f(\vec y)=g(\vec y)$ valid in $M$ is decidable.
> 
> 
> 


**Proof:** By the remark above, we can write $f,g$ as polynomials in $\mathbb N[\vec y]$. Notice that if $h\in\mathbb N[\vec y]$ is non-constant, we have $h(\vec\infty)=\infty$.


Case 1: If $f$ and $g$ are nonconstant, then $M\models\phi$, as witnessed by $\vec y=\vec\infty$.


Case 2: Let (wlog) $g$ be constant, say $g=c\in\mathbb N$. I claim that if $f(\vec a)=c$ for some $\vec a\in M$, then also $f(\vec b)=c$, where $b\_i=\min\{a\_i,c\}$. Indeed, if $h(\vec y)=\prod\_{i\in I}y\_i$ is a monomial that appears in $f$ with a nonzero coefficient, and $a\_i>c$ for some $i\in I$, then $a\_j=0$ for some $j\in I$, lest $f(\vec a)\ge h(\vec a)>c$. Thus, $h(\vec a)=h(\vec b)=0$. Consequently, $M\models\phi$ iff there are $a\_1,\dots,a\_m\in\{0,\dots,c\}$ such that $f(\vec a)=c$, and this can be algorithmically checked.$\qquad\Box$


Now, let $T$ be the theory axiomatized by $Q$, the axioms of commutative semirings, and $\{\phi:M\models\phi\}\cup\{\neg\phi:M\nvDash\phi\}$ for Diophantine sentences $\phi$. Then $T$ is consistent (being true in $M$), and recursively axiomatized (by the lemma), but for every Diophantine formula $\phi(x)$ and $n\in\mathbb N$, the sentence $\phi(S^n(0))$ is decidable in $T$.
(One can check that the finite theory $T=Q$ + commutative semirings + $\exists x\,\forall y\,(x+y=x)$ also works.)


As a related result, the set of Dophantine sentences consistent with $Q$ is decidable, see <https://mathoverflow.net/a/194502> .


Let me remark that while the answer above exploits the weakness of $Q$ which allows for quite pathological models, reasonable stronger base theories can still make a trouble. In particular, it is a long-standing open problem whether the universal fragment of the theory of quantifier-free induction ($\mathit{IOpen}$) is decidable; ~~if it is, then one can construct a counterexample $T$ as above with $T\supseteq\mathit{IOpen}$.~~ [EDIT: While I’m pretty sure the existence of models of $\mathit{IOpen}$ with decidable existential theory is also an open problem, it’s stronger than decidability of its universal fragment: we would need decidability of Boolean combinations of $\exists$ sentences, or some kind of amalgamation property.]


EDIT: I found that the Lemma above, using the same model $M$, was proved by Dyson, Jones and Shepherdson [2]. Better yet, they also found a model $M\_1\models Q$ that embeds in the non-negative part of an ordered domain such that the validity of existential sentences of the language $\langle0,S,+,{\cdot},{\le}\rangle$ in $M\_1$ is decidable. (The order is not discrete, though. It also does not agree with the usual order defined in $Q$ via $\exists z\,x+z=y$.)




---


On the other hand, the answer is positive for theories $T$ extending $I\Delta\_0+\mathit{EXP}$, as this theory proves the MRDP theorem.


EDIT: In fact, the positive answer does not need anything as strong as exponentiation for the base theory, because we do not need full MRDP theorem for Diophantine definability on *standard* integers. Let $IE\_1,IU\_1\subseteq I\Delta\_0$ be the fragments of PA with induction only for bounded existential formulas and bounded universal formulas, respectively, and $IU\_1^-$ a further restriction of $IU\_1$ where induction formulas are not allowed parameters. (Actually, $IE\_1$ and $IU\_1$ *with* parameters coincide.) I will write just $n$ for $S^n(0)$ below.



> 
> **Theorem:** Every partial recursive function $f(\vec x)$ has a Diophantine representation $\phi(\vec x,y)$ in $IU\_1^-$, in the sense that
> 
> 
> 1. $IU\_1^-\vdash\forall x,y,y'\,(\phi(\vec x,y)\land\phi(\vec x,y')\to y=y')$.
> 2. If $f(\vec n)=m$, $IU\_1^-\vdash\phi(\vec n,m)$.
> 
> 
> Consequently, for every pair of disjoint r.e. sets $A,B$, there is a Diophantine formula $\phi(x)$ such that $n\in A$ implies $IU\_1^-\vdash\phi(n)$, and $n\in B$ implies $IU\_1^-\vdash\neg\phi(n)$.
> 
> 
> 


The argument is mostly a rehashing of results of Kaye [1]. First, $IE\_1$ is $\forall\_1$-conservative over $IU\_1^-$, hence we may work in $IE\_1$, and every existential formula is easily seen to be equivalent to a Diophantine formula over $IE\_1$, hence it suffices to find an existential representation.


Let $\exists\vec z\,\theta(\vec x,y,\vec z)$ be an existential definition of the graph of $f$ in $\mathbb N$, and put
$$\phi\_0(\vec x,y)=\exists w,\vec z\,\bigl(\vec x,y,\vec z\le w\land\theta(\vec x,y,\vec z)\land\forall y',\vec z'\le w\,(\theta(\vec x,y',\vec z')\to y=y')\bigr).$$
A standard argument shows that $\phi\_0$ represents $f$ in $IE\_1$, but it’s only $\exists U\_1$.


Kaye defines a $\forall\exists$ axiom $E$, and shows that $IE\_1+E=I\Delta\_0+\mathit{EXP}$, and that it proves the MRDP theorem. Thus, there is an existential formula $\exists\vec u\,\eta(\vec x,y,w,\vec u)$ such that
$$IE\_1+E\vdash\exists\vec u\,\eta(\vec x,y,w,\vec u)\leftrightarrow\forall y',\vec z'\le w\,(\theta(\vec x,y',\vec z')\to y=y').$$
Applying [1, Lemma 5.8 (ii)] to the left-to-right implication, there is an existential formula $\exists\vec v\,\xi(r,\vec v)$ such that
\begin{align\*}
IE\_1+E&\vdash\forall r\,\exists\vec v\,\xi(r,\vec v),\\
IE\_1&\vdash\xi(r,\vec v)\land \vec x,y,w,\vec u\le r\land\eta(\vec x,y,w,\vec u)\to\forall y',\vec z'\le w\,(\theta(\vec x,y',\vec z')\to y=y').
\end{align\*}
Define $\phi(\vec x,y)$ as
$$\exists w,\vec z,\vec u,r,\vec v\,\bigl(\vec x,y,\vec z\le w\land w,\vec u\le r\land\theta(\vec x,y,\vec z)\land\eta(\vec x,y,w,\vec u)\land\xi(r,\vec v)\bigr).$$
Clearly, $\phi(\vec x,y)$ is an existential formula, and it is easy to see that it satisfies condition 1. If $f(\vec n)=m$, then $IE\_1+E\vdash\phi(\vec n,m)$, as it proves $\phi$ equivalent to $\phi\_0$. Since $IE\_1+E$ is sound, the existential sentence $\phi(\vec n,m)$ is true in $\mathbb N$, and consequently provable in $Q\subseteq IE\_1$. Thus, $\phi$ represents $f$ in $IE\_1$.


**References:**


[1] Richard Kaye, *Diophantine induction*, Annals of Pure and Applied Logic 46 (1990), no. 1, pp. 1–40. <http://dx.doi.org/10.1016/0168-0072(90)90076-E>


[2] Verena H. Dyson, James P. Jones, and John C. Shepherdson, *Some diophantine forms of Gödel’s theorem*, Archiv für mathematische Logik und Grundlagenforschung 22 (1982), pp. 51–60. <https://eudml.org/doc/137991>


