Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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

share|improve this question
The question is equivalent to constructing a polynomial diophantine equation in the Hilbert's 10th. It sounds to me as mathoverflow.net/questions/20430... –  Wadim Zudilin Jul 22 '10 at 4:09
@Wadim: Could you clarify how the answer to that question answers this one? I don't follow. –  Akhil Mathew Jul 22 '10 at 4:12
@Wadim: The question is whether or not such a polynomial has ever been explicitly computed, not whether or not one exists. –  Harry Gindi Jul 22 '10 at 4:15
Akhil and Harry, there is no relation between the question I mention and this one. "Sounds" means that the existence is known (for periods) but nobody can give an explicit (explicitly computed, if you wish) example. –  Wadim Zudilin Jul 22 '10 at 5:54
What is the meaning of "lack of roots can't be proved"? That the existence of roots, and the nonexistence, are both consistent with ZFC? Or that it actually does not have roots, but you cannot prove it? –  Anweshi Jul 22 '10 at 12:15
show 4 more comments

5 Answers

up vote 28 down vote accepted

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 at http://www.math.uni-bonn.de/people/carl/preprint.pdf.

share|improve this answer
You must mean nonsolvable, right? Otherwise we can prove the consistency of ZFC within ZFC... –  Pete L. Clark Jul 22 '10 at 8:24
Pete, you are absolutely right. I edited "consistent" to "inconsistent". –  Stefan Geschke Jul 22 '10 at 8:59
The paper with Moroz is about a different problem, halfway between expressing inconsistency of ZFC and Diophantine coding of the halting problem. They find Diophantine equations expressing "$n$ is the Goedel number of a formula provable in the predicate calculus with one binary predicate (and no function or constant symbols)". To get ZFC from this one has to interpret it using a finite number of axioms in predicate calculus. For that reason the paper mentions only NBG set theory. To Diophantine express its consistency one needs, ad hoc, Goedel number of the formula "NBG axioms imply 0=1". –  T.. Jul 23 '10 at 9:16
The link is now "404 - Not Found." –  Rasmus Bentmann Feb 6 at 20:25
add comment

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.

share|improve this answer
That paper contains the following beautiful theorem: For every axiomatizable theory $T$ and any proposition $P$, if $P$ has a proof in $T$, then $P$ has another proof consisting of 100 additions and multiplications of integers. Amazing :P I wonder if anyone has bothered to find the optimal bound! –  Mariano Suárez-Alvarez Jul 22 '10 at 5:46
add comment

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.

share|improve this answer
Hmm. The way Akhil stated the result was that: if ZFC is consistent, you can write down a polynomial $P \in \mathbb{Z}[x] = \mathbb{Z}[x_1,\ldots,x_n]$ without integer solutions. You seem to be claiming: one may write down a polynomial $P \in \mathbb{Z}[x]$ such that, if ZFC is consistent, then it has no roots, but this cannot be proved from ZFC. That sounds much stronger. Are you sure about this? –  Pete L. Clark Jul 22 '10 at 5:40
The Matijasevich et al proof uses much less than ZFC, so as long as that proof is correct, ZFC's consistency or lack thereof doesn't affect anything. They showed that one can (mechanically) associate to any given implementation of ZFC a Diophantine equation whose solutions correspond to inconsistencies (if any) in ZFC. e.g., "$(n,x_1,\dots,x_{136})$ is a solution if and only if the $n^{\rm th}$ valid proof of this version of ZFC has $0=1$ as its conclusion". –  T.. Jul 22 '10 at 5:52
@T.: thanks; I think that addresses my concern. –  Pete L. Clark Jul 22 '10 at 6:11
Thanks! I am going to add a link from the math.SE question to this answer. –  Akhil Mathew Jul 22 '10 at 12:10
add comment

For every consistent recursively axiomatizable theory $T$ there exists (and one can effectively compute it 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) + \\ &(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 "Universal Diophantine Equation" by James P. Jones.

share|improve this answer
Of course, not all numbers in the set can be effectively computed from the axioms, but an infinite subset of them can be. –  Vladimir Reshetnikov Nov 27 '11 at 5:51
add comment

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 http://www.springerlink.com/content/m5k0281k67r46325/ )

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.

share|improve this answer
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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