Does anyone know a polynomial whose lack of roots can't be proved?

Question

In Ebbinghaus-Flum-Thomas's Introduction to Mathematical Logic, the following assertion is made:

If ZFC is consistent, then one can obtain a polynomial $P(x_1, ..., x_n)$ which has no roots in the integers. However, this cannot be proved (within ZFC).

So if $P$ has no roots, then mathematics (=ZFC, for now) cannot prove it.

The justification is that Matiyasevich's solution to Hilbert's tenth problem allows one to turn statements about provable truths in a formal system to the existence of integer roots to polynomial equations. The statement is "ZFC is consistent," which cannot be proved within ZFC thanks to Gödel's theorem.

Question: Has such a polynomial ever been computed?

(This arose in a comment thread on the beta site math.SE.)

Answer 1

In his Master's Thesis, Merlin Carl has computed a polynomial that is solvable in the integers iff ZFC is inconsistent. A joint paper with his advisor Boris Moroz on this subject can be found here.

Answer 2

For every consistent recursively axiomatizable theory $T$ there exists (and can be effectively computed from the axioms of $T$) an integer number $K$ such that the following Diophantine equation (where all letters except $K$ are variables) has no solutions over non-negative integers, but this fact cannot be proved in $T$: \begin{align}&(elg^2 + \alpha - bq^2)^2 + (q - b^{5^{60}})^2 + (\lambda + q^4 - 1 - \lambda b^5)^2 + \\ &(\theta + 2z - b^5)^2 + (u + t \theta - l)^2 + (y + m \theta - e)^2 + (n - q^{16})^2 + \\ &[(g + eq^3 + lq^5 + (2(e - z \lambda)(1 + g)^4 + \lambda b^5 + \lambda b^5 q^4)q^4)(n^2 - n) + \\ &\quad\quad(q^3 - bl + l + \theta \lambda q^3 + (b^5-2)q^5)(n^2 - 1) - r]^2 + \\ &(p - 2w s^2 r^2 n^2)^2 + (p^2 k^2 - k^2 + 1 - \tau^2)^2 + \\ &(4(c - ksn^2)^2 + \eta - k^2)^2 + (r + 1 + hp - h - k)^2 + \\ &(a - (wn^2 + 1)rsn^2)^2 + (2r + 1 + \phi - c)^2 + \\ &(bw + ca - 2c + 4\alpha \gamma - 5\gamma - d)^2 + \\ &((a^2 - 1)c^2 + 1 - d^2)^2 + ((a^2 - 1)i^2c^4 + 1 - f^2)^2 + \\ &(((a + f^2(d^2 - a))^2 - 1) (2r + 1 + jc)^2 + 1 - (d + of)^2)^2 + \\ &(((z+u+y)^2+u)^2 + y-K)^2 = 0. \end{align} Moreover, for every such theory, the set of numbers with this property is infinite and not recursively enumerable.

The equation is derived from Undecidable Diophantine Equations, James P. Jones, Bull. Amer. Math. Soc. (N.S.), Vol. 3(2), Sep. 1980, pp. 859–862, DOI: 10.1090/S0273-0979-1980-14832-6.

Answer 3

Something close to what you want is in the paper "Universal Diophantine Equation" by James P. Jones in the Journal of Symbolic Logic 47 (1982), pp. 549--571. Jones produces an explicit list of 37 equations in 53 unknowns whose simultaneous satisfiability is equivalent to a general membership statement for computably enumerable sets.

These 37 equations are equivalent to a single equation (sum of their squares = 0) and, since it is universal, you can find an instance equivalent to an unprovable but true sentence of ZFC by substituting values for a couple of the variables. It remains to compute these numerical values, which are probably huge ...

If you have access to JSTOR you can see the paper here.

Answer 4

The MRDP solution of Hilbert's 10th problem establishes that the integer solution sets $\{\, n\, |\, \exists\vec n\, p(n,\vec n)=0\}$ of diophantine equations $p(n,\vec n)=0$ are exactly the computably enumerable sets.

In particular, for any consistent theory $T$, such as PA or ZFC or whatever your favorite theory is, we can write down a particular polynomial $p(n,\vec n)$ such that $p(n,\vec n)=0$ exactly when $n$ is the Goedel code of the proof of a contradiction from $T$, since this is certainly a c.e. set. Thus, if $T$ is consistent, then $p(n,\vec n)=0$ will have no integer solutions, but by the incompleteness theorem, $T$ will be unable to prove this. This issue is discussed in this MO answer.

It is possible in principle to extract from the proofs the actual polynomials involved, and I believe that for the standard theories, these polynomials have been written down. Although some might find it not particularly illuminating to do so, I would admire anyone who put in the effort to actually produce the polynomial. Perhaps others will answer with the actual polynomials.

Answer 5

This question is frequently asked, usually in relation to the Riemann hypothesis or the consistency of set theory. I suppose this is as good a place as any to collect references to explicit arithmetizations of initially non-Diophantine problems, as (systems of) Diophantine equations.

In one of his earlier papers, Matijasevich gives an example of a Diophantine equation expressing a number-theoretic statement, different from the ones on the path to Hilbert's 10th problem. The ones on the path were his breakthrough "$m = F_{2n}$" and the universal Diophantine predicate, "machine $m$ halts in time $t$ on input $n$". The illustrative example was something like "is a prime number", not anything as complicated as consistency of ZFC. The universal equation can be specialized by a choice of $m$ and $n$ to an equation expressing inconsistency of ZFC, but actually writing down specific values accomplishing that translation would be a formidable task. (ADDED: the paper is online at Link )

J.P. Jones has several papers, some with Matijasevich, providing Diophantine encodings of other number theoretic statements. Website: http://math.ucalgary.ca/~jpjones/papers.htm

The long paper by Davis, Robinson and Matijasevich gives Diophantine representations of the Riemann Hypothesis and of "$p$ is a prime number" from which one can write down the Goldbach conjecture, or near-equivalents of the Twin Primes conjecture. Most of it is online at: http://books.google.com/books?id=4lT3M6F745sC&pg=PA323

I don't know if (in)consistency of ZFC has been displayed in print as a Diophantine equation. There may be computer programs available to perform the transformations from ZFC parser to Turing machine to Diophantine representation, and if so, their possibly very large output would answer the question. If you are willing to allow exponentiation as a primitive, as Goedel did in his paper, Gregory Chaitin made software available to construct a huge exponential Diophantine equation, similar to the one printed in his book, whose solution set is algorithmically random when projected onto one of its variables. The Matijasevich-Robinson encoding of $a=b^c$ could then be applied, to produce an ordinary, but even larger, Diophantine statement.