# Question related to Hilbert's 10th problem

Given $n \in \mathbb{N}$ and $p,q \in \mathbb{N}[x_1,\ldots,x_n]$ one can define the following formula in the language of formal arithmetics

$$\varphi(n,p,q) = \forall x_1 \cdots \forall x_n : \neg (p(x_1,\ldots,x_n) = q(x_1,\ldots,x_n))$$

I would like to show that there are infinitely many triples $(n,p,q)$ such that neither $\varphi(n,p,q)$ nor $\neg \varphi(n,p,q)$ is a theorem of formal arithmetic.

In showing this I can use the fact that the problem of deciding if a polynomial $r \in \mathbb{Z}[x_1,\ldots,x_n]$ has a natural zero is undecidable.

Knowing the above fact we know that there is a polynomial $r \in \mathbb{Z}[x_1,\ldots,x_n]$ such that neither $$\varphi' = \forall x_1 \cdots \forall x_n : \neg (r(x) = 0)$$ nor $\neg \varphi'$ is a theorem. (Here the quantifiers are over the naturals which I am not sure if I can use deliberately?)

Once we have such $r$ we can write it as $$r(x_1,\ldots,x_n) = p(x_1,\ldots,x_r) - q(x_1,\ldots,x_n)$$ for $p,q \in \mathbb{N}[x_1,\ldots,x_n]$ and hence $\varphi(n,p,q)$ and $\neg \varphi(n,p,q)$ are also not theorems since $\varphi$ is logically equivalent to $\varphi'$ and we have shown that this is not a theorem.

Once we have one such triple $(n,p,q)$ we have infinitely many of them since we can just take $(n,p+k,q+k)$ for $k \in \mathbb{N}.$

Since I never did such things before I am wondering if the above reasoning is correct?

-
You can also multiply both sides by a constant factor... –  cody Nov 28 '12 at 16:18
It would be more interesting to find infinite pairs of (p,q) that are not related by "affine transformations". I suspect there is a relatively simple argument to show this as well. –  cody Nov 28 '12 at 16:58
You can substitute $a+b$ or $a^2+b^2+c^2+d^2$ for a variable $x_i$ to get a "different" pair $(p,q)$. –  Yuval Filmus Nov 28 '12 at 19:12