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})$)?

  • 1
    $\begingroup$ Could the downvoter please explain what the downvote was about? $\endgroup$ – Andrej Bauer May 28 '14 at 9:34

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


[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

  • $\begingroup$ It might be woth pointing out that the counterexample can be made finitely axiomatizable: an inspection of the proof of the lemma reveals that it is enough to take $Q$ + commutative semirings + $\exists x\,\forall y\,x+y=x$. $\endgroup$ – Emil Jeřábek May 28 '14 at 13:20
  • $\begingroup$ Thanks Emil! I will summarize your main counterexample as a separate answer, at least for my own benefit. A question on your finitely axiomatizable counterexample: $Q$ $+$ commutative semirings $+$ $\exists x \forall y (x+y=x)$. Let $D_0=$ the set of diophantine sentences of the form $\exists \vec{y}(f(\vec{y}) = g(\vec{y}))$ in which one of the polynomials $f$ and $g$ is a constant, and $D_1=$ the set of such sentences in which both $f$ and $g$ are non-constant. I see how this theory proves all sentences of $D_1$, but how does it prove all the $\neg\sigma$ for false $\sigma \in D_0$? $\endgroup$ – Dave Albert May 28 '14 at 21:46
  • $\begingroup$ $\let\ol\overline$Let $\ol n:=S^n(0)$ for $n\in\mathbb N$. You need to show in $Q$ that $x+y=\ol n$ implies $x=\ol m$ and $y=\ol{n-m}$ for some $m\le n$, that $xy=0$ implies $x=0$ or $y=0$, and if $n\ne 0$, that $xy=\ol n$ implies $x=\ol m$ and $y=\ol{n/m}$ for some $m\mid n$. Then you can simulate the argument in the proof of the lemma. $\endgroup$ – Emil Jeřábek May 28 '14 at 22:12
  • $\begingroup$ Yes, I think I see it now, thanks again! One more question: Does your counterexample for diophantine formulas generalize to $\exists$-formulas? Or is there a $\exists$-formula witnessing the essential incompleteness of $Q$? (A $\exists$-formula is one of the form $\exists \vec{y} \psi(\vec{x},\vec{y})$ with $\psi$ quantifier free.) $\endgroup$ – Dave Albert May 29 '14 at 9:18
  • $\begingroup$ I am confident the answer is the same, but my example does not work: $\mathbb N$ is definable in $M$ by an $\exists$ (negated atomic) formula, hence the $\exists$-theory of $M$ is $\Sigma^0_1$-complete. One would need a more complicated model, and it’s not clear to me ATM how to construct it. It would suffice to have an example with $T\supseteq\mathit{PA}^-$ (= the theory of nonnegative parts of discretely ordered rings) as every $\exists$ formula is equivalent to a Diophantine one over $\mathit{PA}^-$, however, I believe the existence of DOR with decidable $\exists$-theory is an open problem. $\endgroup$ – Emil Jeřábek May 29 '14 at 13:41

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.