# Essential incompleteness via diophantine formulas?

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

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

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

• 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$. – Emil Jeřábek May 28 '14 at 13:20
• 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$? – Dave Albert May 28 '14 at 21:46
• $\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. – Emil Jeřábek May 28 '14 at 22:12
• 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.) – Dave Albert May 29 '14 at 9:18
• 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. – Emil Jeřábek May 29 '14 at 13:41