Question related to Hilbert's 10th problem

Question

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?

Answer 1

As pointed by Yuval and cody there are easy solutions to get infinitely many Diophantine equations that are not provable nor refutable (let's say in PA).

However these syntactic solution result in provably equivalent sets, i.e. sets that the theory can prove they are equivalent. You can consider these as padding arguments. Another way is adding a variable which is not used at all.

You can also play with adding or removing some strings explicitly (finite variations of the set).

If you want to get Diophantine equations that are "essentially" different (e.g. the sets are not Turing equivalent) then that is more challenging and I think knowing that there is an independent Diophantine equation is not enough, you will need the fact that every r.e. set can be encoded as a Diophantine equation (or something similar).

ps: since you only care independence it is more natural to represent these formulas as Diophantine equations not their negations.