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?

Solution 1:

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.

Solution 2:

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.