# How can there be explicit polynomial equations for which the existence of integer solutions is unprovable?

This answer suggests that there are explicit polynomial equations for which the existence (or nonexistence) of integer solutions is unprovable. How can this be?

-
Well it's certainly possible to prove existence by finding a solution! :) –  BlueRaja - Danny Pflughoeft Jul 22 '10 at 16:43

Edit: This has been explained better by Joel David Hamkins; cf. this MO thread.

This is because given any first-order formula $\phi(x_1, \dots, x_n)$ with $n$ parameters in the integers, there is a polynomial $P(x_1, \dots, x_n, z_1, \dots, z_m)$ which can be proved to have a root in $z_1, \dots, z_m$ in the integers if and only if $\phi(x_1, \dots, x_n)$---this is a version of Matiyasevich's solution to Hilbert's tenth problem.

Now, it's possible to construct within any formal system explicit first-order formulas which can't be proved or disproved (for instance, the statement "this formal system is consistent"). This is the second incompleteness theorem. These first-order formulas correspond to polynomials by the first paragraph.

In particular, one can show that you can construct a polynomial $P(z_1, \dots, z_m)$ corresponding to the statement "mathematics* is inconsistent" translated to a formula. Thus, if mathematics is consistent, there's no mathematical proof that this polynomial doesn't have a root.

*Mathematics=ZFC here.

For more on these lines, see Ebbinghaus-Frum-Thomas's very accessible book on mathematical logic.

-
@Akhil: Has anyone actually computed such a polynomial? –  user126 Jul 22 '10 at 3:36
Don't know. E-F-T says that it can be computed, and Matiyasevich says that there have been computations for universal Diophantine equations, so I would imagine possibly, but I can't find it. (It might make a decent MO question.) –  Akhil Mathew Jul 22 '10 at 3:45
You should ask it on MO. I don't know the context, so I'll probably screw it up. –  user126 Jul 22 '10 at 3:46
Done - mathoverflow.net/questions/32892/…. I'm waiting for Joel David Hamkins... –  Akhil Mathew Jul 22 '10 at 4:01
I don't know the explicit polynomials myself, but apparently it's a bit of a cottage industry to try to find smaller and smaller ones. For example you can do 9 variables (but degree 10^45) or you can do degree 4 (but 58 variables), see wolframscience.com/reference/notes/1161a –  Noah Snyder Jul 22 '10 at 4:15

The answer to this question depends on how the problem is defined, but the answer is no, at least without defining the problem in a misleading way.

Since my first solution was completely off the mark, I have deleted it and posted this new one.

Consider polynomial p. If it has an integer solution, then the solution will eventually be found by random guessing. So if it is impossible to prove the existential status, there must be no solution.

Now we know from this link that there is a polynomial, q, that is unsolvable in the integers iff ZFC is consistent. It is well known that ZFC cannot prove its own consistency. So if it ZFC is consistent, then q is unsolvable, but we cannot prove this as then we could prove ZFC. So it seems like it is accurate to say that if mathematics is consistent, we have a polynomial with no integer roots, but we can't prove it. However, if we are assuming maths is consistent, we can use this to prove that the equation is unsolvable (indeed that is what we have done). So, it really isn't accurate an accurate statement at all.

To further clarify, when considering mathematical truth, there are two basic ways of viewing it. The first is where we are assuming that are axioms are true, which necessarily means assuming consistency. If we show any problem is equivalent to consistency, then we consider it to be true.

The other is where we are considering a formal set of statements, of which the axioms have been defined to be true and seeing which statements can be derived to be true. From this viewpoint, we don't actually know whether the axioms are consistent or not. In fact, Godel's second incompleteness theorem shows that no "non-trivial" atomic system can prove its own consistency. So showing a problem is equivalent to consistency is actually the same as showing that the problem is unprovable by the atomic system.

The confusion comes from assuming ZFC is consistent to eliminate one possibility in a choice, yet not allowing this assumption to be used as an axiom in the proofs.

-
I meant that the lack of roots cannot be proved formally within ZFC; the statement "mathematics can't prove X" is largely for dramatic effect. If we assume ZFC is consistent, the fact that the polynomial has no roots; the point remains that a formal derivation of the lack of roots of this polynomial from the axioms does not exist. –  Akhil Mathew Jul 24 '10 at 16:58
@Akhil: My point is that if we are assuming ZFC, we should be allowed to use to as an axiom. Obviously if we allow one part of our reasoning to know about ZFC and the other not to, then we will get weird inconsistencies like knowing something has to have no root, but not being able to prove it. –  Casebash Jul 24 '10 at 19:27
The point should be that ZFC doesn't prove the polynomial has no integer solutions, but the strictly stronger theory ZFC+Con(ZFC) does prove that there are no integer solutions. –  JDH Jul 31 '10 at 19:22