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?
Question related to Hilbert's 10th problem
computability;logic;undecidability