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?

  • $\begingroup$ You can also multiply both sides by a constant factor... $\endgroup$
    – cody
    Nov 28, 2012 at 16:18
  • $\begingroup$ 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. $\endgroup$
    – cody
    Nov 28, 2012 at 16:58
  • 2
    $\begingroup$ 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)$. $\endgroup$ Nov 28, 2012 at 19:12

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.